Hacker News new | comments | show | ask | jobs | submit login

>I've heard of a language being called expressive, but not a type system.

Haskell's type system is practically a language itself. It has many powerful features that aid with expression:

    * sum, product and generalized algebraic data types (GADTs)
    * higher-kinded types
    * universally & existentially quantified types
    * scoped type variables
    * impredicative types
    * associated types
    * type families
    * kind polymorphism (a new feature)
    * type holes (also new)
>By the way, does Haskell's type system have the "value restriction" that you run into in ML?

I'm not sure what you mean by "value restriction". Haskell, like ML, is not a dependently typed programming language. For that you'll want to use something like Agda. As for why you'd want a language to not have dependent types? Well, having them introduces all kinds of considerations with regards to decidability and type inference.

The value restriction is a rule that governs when type inference is allowed to polymorphically generalize a value declaration. In short, the value restriction says that generalization can only occur if the right-hand side of an expression is syntactically a value. [...] The value restriction prevents a ref cell (or an array) from holding values of different types, which would allow a value of one type to be cast to another and hence would break type safety


It can be annoying to work around this, because there are potentially ML programs that would be type-safe and would otherwise compile if they were not hindered by the value restriction.

I got my answer, though:

Ii is interesting that in ML, the presence of mutable ref cells and parametric polymorphism requires the whole language to be dominated by a "value restriction" [1] to ensure that the type system remains sound, whereas in Haskell, because IORef's can only be created (and used) in the IO monad, no such restriction is necessary.


Ahh, thank you. This was very informative. I have no experience with ML. I thought you might have been referring to the mixing of values and types which occurs in dependently typed programming.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | DMCA | Apply to YC | Contact