New extension to Haskell -- data types and polymorphism at the type level

[JoshTriplett]

This extension (together with the type-level built-in literals, described in section 8.3 of the paper) looks like it will address the major remaining wart I've observed in Haskell: the widespread use of complex type-level programming to make up for deficiencies in the type system. Many packages on Hackage have deep type-level hackery under the surface, and that hackery often creates subtle differences and incompatibilities.

[jrockway]

Could you give a specific example?

[lubutu]

So if we have polymorphic types, and now polymorphic kinds, if we call those first- and second-order polymorphism, why can't we extend this to higher orders? For instance, third-order would be when our kinds' types are also polymorphic.

[ac]

Type inference for higher-order dependent types is undecidable[1]. Going higher up the ladder of "polymorphism orders" one would eventually have to sacrifice Haskell's type inference -- which, I'm sure, few want to: otherwise, a lot more people would have programmed in Coq already.

[1] J. B. Wells. "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable." In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176–185, 1994. (Shamelessly copied from Wikipedia)

[bremac]

Interesting. The extensions to the type system remind me of Ωmega (http://code.google.com/p/omega/), though without higher-order kinds.

EDIT: Turns out "Programming in Omega" is cited by the section on related work. No wonder the mention of proving red-black trees using type-level computation seemed familiar...

[thesz]

Omega became what called now "type families".

Types at the kind level and kind polymorphism is much more close to dependent type system.

Honestly, I cannot wait. ;)

[skybrian]

It sounds pretty neat, but how could all this intimidating-looking type theory this be made useful for ordinary programmers who don't know what a monad is?

[fleitz]

I'm also not sure what these type extensions have to do with monads, monads just describe side effects as a type.

Read about the async keyword in C# if you want to know why monads are useful. I'm not sure why MSFT decided to take a great thing like monads and only allow one type of monad instead of building in support for the general case, it seems so typical in imperative languages that the forest is missed for the trees. They'll take a great thing like generics and then screw it up by only allowing methods on classes which ruins type inference.

  for example:
  var a = new Array<int>(1,2,3,4);
  instead of
  var a = Array.new(1,2,3,4);

I'm not sure why ordinary programmers shouldn't know what a monad is, it's an extremely useful pattern that makes code much easier to read. It's like not knowing what an array is.

[dramaticus3]

You dawg!, I hear you like type systems ...