First class polymorphism + refined types?

[FrankBro]

First of all, I would like to say thank you for your great project on type systems. I've been interested in the concept for a while without never really touching or implementing them and your project really helps me to better understand them.

I've always thought that a perfect type system would be something along two of your sub-projects, first class polymorphism + refined types. I've been playing around with those two a little bit with the hope of merging them but I wanted to ask you first if it made sense since you seem to be well versed on the subject. Is there anything that would prevent them both from co-existing within the same type system?

[tomprimozic]

Hi! In theory, I don't see a problem, as the type inference/(ML) type-checking phase, which transforms the AST into a typed expression tree, and the refined type-checking (which makes sure that contracts are satisfied) are strictly separated. The problem, however, is that in the current implementation of the refined type system, functions as parameters are not implemented, and functions as return types are not fully implemented (hence, a lot of first-class polymorphism wouldn't pass the refined type checker because it would raise NotImplemented errors). I don't think it would be particularly hard to implement that, and it's completely orthogonal to first-class polymorphism, I'll probably implement it sometime soon.

But yes, I completely agree, a perfect type system would definitely support both refined types and first-class polymorphism (and hopefully other things as well, like a good record system).

[FrankBro]

Nice. I will continue playing with these two then and compare my version with yours if you decide to do it.

I agree, records and variants would be in indeed. Out of curiosity, is there any other specific features or properties your perfect type system would have? To me, a mix of ocaml/F# + type classes of haskell + easy to use dependent types sounds pretty perfect yea.

[tomprimozic]

Uh, that's a hard question... I'm still conflicted about it, as I haven't discovered yet how to even make some of the "perfect" parts of the "perfect" type system, let alone combine them. Some ideas:

• linear/unique types that would enable (1) RIAA and safe I/O (i.e. you have to close every file) (2) mutable updates of linear immutable structures (3) compiler optimizations (since linear parameters can't alias) and (4) no GC (linear objects can be safely deallocated). Ideally also (5) safe region memory allocation. Rust is a great experiment, as is Cyclone, but I don't agree with some of their design choices (and goals).
• subtyping seems unavoidable for programming in the large; you need interfaces (Go) / abstract types (Julia) / traits (Scala) / classes (C++, Java). Also, "real math" has subtyping (i.e. an integer is a rational is a real is a complex). I hope to avoid it, but I haven't yet figured out how, especially since subtyping also gives you ...
• union types, such as int | none or array[int | float]. They just seem so convenient. Of course, type inference becomes almost impossible (or at least nobody has figured it out yet, though I think it's implemented in Stardust).
• effect system sounds like a great idea, but I'm not sure yet what kinds of effects. Is logging/metrics an effect? Is it enough to denote that a function could throw an exception, or should you also say which exceptions it can throw? The latter seems like a good idea for library functions (why write documentation if you can write code) but like hell for higher-order functions. Should functions be impure or pure (or total) by default? Only total functions (like length) can be used in contracts. Is writing to memory an effect, or is writting to a specific location (i.e. global variable) an effect? Effects could enable automatic paralelism, STM, easier static verification. Koka is a nice attempt.
• records and first-class modules, ideally one system that can combine both. Type classes are nice, but seem to "magicky" - to make them really useful, you basically have to make it Turing-complete, which means a language within a language. I hope that modules + a kind of implicit arguments can make a simpler system for overloading/abstraction. But AFAIK no-one has done that so far.
• dynamic types for when you just don't give a fuck

[FrankBro]

linear/unique types that would enable (1) RIAA and safe I/O (i.e. you have to close every file)

Something like the indexed monad is really interesting here. Logic is type checked. https://gist.github.com/gelisam/9845116

(2) mutable updates of linear immutable structures

Something like functionally reactive?

(3) compiler optimizations
(4) no GC (linear objects can be safely deallocated)

I was surprised F# didn't have something like list fusion in haskell. A typical functional pattern like folding creates new objects instead of modifying them, lifetime and usage isn't tracked. https://www.haskell.org/ghc/docs/7.0.1/html/users_guide/rewrite-rules.html

subtyping seems unavoidable for programming in the large; you need interfaces (Go) / abstract types (Julia) / traits (Scala) / classes (C++, Java). Also, "real math" has subtyping (i.e. an integer is a rational is a real is a complex). I hope to avoid it, but I haven't yet figured out how, especially since subtyping also gives you ...

Yea subtyping seems unavoidable.

records and first-class modules, ideally one system that can combine both. Type classes are nice, but seem to "magicky" - to make them really useful, you basically have to make it Touring-complete, which means a language within a language. I hope that modules + a kind of implicit arguments can make a simpler system for overloading/abstraction. But AFAIK no-one has done that so far.

I've had a problem for which type classes would've been nice not too long at work. It's just basically attaching interfaces but after a type definition. F# doesn't allow that, which forces you to write a bunch of boilerplate to contain types supported by the language (int, bool, string, etc).

dynamic types for when you just don't give a fuck

pls no

[Apanatshka]

Hi,
just found this project through HN. Very cool!

I noticed this part of the discussion here:

I hope that modules + a kind of implicit arguments can make a simpler system for overloading/abstraction. But AFAIK no-one has done that so far.

I just wanted to share that long-term plans for Elm involve type-classy functionality which will likely be done with the already available (extensible) records and implicit arguments. I think one of the first mentions of this plan is here, and there are more references to records+Agda style implicit arguments on the mailing list.
I know it's not quite the same as parametrised modules with implicit arguments, but I figured I'd share :)

[tomprimozic]

Hi Jeff!

Thanks for the pointer. I have a similar plan; combine combine records and implicit arguments to make type-classes. This is an interesting paper that I read on that topic: http://homepages.inf.ed.ac.uk/wadler/papers/implicits/implicits.pdf. I'm not sure it would work when combined with records or extensible records, but I think it's worth trying.

[toroidal-code]

Daan Leijen has an excellent paper that introduces an effect-based type system called LambdaK. The effect system is row-polymorphic, so multiple effects can be attributed to a single expression. There's an example implementation in Haskell for his language Koka.

[toroidal-code]

And I just saw your comment about Koka. Sorry!

[arseniiv]

union types, such as int | none or array[int | float]. They just seem so convenient. Of course, type inference becomes almost impossible (or at least nobody has figured it out yet, though I think it's implemented in Stardust).

Sorry, had stumbled on this thread by accident, I see there’s no recent activity here, but maybe you also would be interested in what was done about them in Ceylon. I haven’t read papers about its type system, but for example, they play nice there with contra/covariant type parameters. They also help there in encoding nonemptiness of streams and sequences and in typing tuples treated as heterogeneous lists (if I represent it correctly) and for representing types of argument lists containing optionals.