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

http://mlton.org/ValueRestriction

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.

http://www.haskell.org/pipermail/haskell-cafe/2007-July/0292...


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

Search: