3 ms·

Why makes you say that Ruby's type system is not expressive? I'm not exactly sure what that means. I've heard of a language being called expressive, but not a t

by kyllo 13y ago

Why makes you say that Ruby's type system is not expressive? I'm not exactly sure what that means. I've heard of a language being called expressive, but not a type system. By the way, does Haskell's type system have the "value restriction" that you run into in ML?

chongli 13y ago
>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.
- kyllo 13y ago
  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 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/029261.html http://www.haskell.org/pipermail/haskell-cafe/2007-July/0292...
  - chongli 13y ago
    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.

by kyllo 13y ago

chongli 13y ago

>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.

kyllo 13y ago
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 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/029261.html http://www.haskell.org/pipermail/haskell-cafe/2007-July/0292...
- chongli 13y ago
  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.