New extension to Haskell -- data types and polymorphism at the type level | Hacker News Reader

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

research.microsoft.com

73 pointsdons13 comments

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.

Could you give a specific example?

Sure.

The paper mentions HList, the "heterogeneous list" package, which often gets used for extensible records and static duck typing; HList uses type-level numbers and lists, and extensive type-level computation. I've wanted to use HList in the past, but the sheer pain of the types involved made it not worth the trouble. It also includes several (incompatible) variations of internal implementations with different tradeoffs.

Several packages exist for "session typing", which allows specification of a communication protocol between functions by using complementary types. Those involve heavy type-level computation on families of related types; this extension would help greatly.

I've personally encountered multiple cases where I'd like to operate on an arbitrary function or type regardless of its arity (how many arguments it takes), but doing so typically requires writing a family of handlers for various argument lengths. This extension would allow handling all of the cases generically.

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.

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)

I think that "second-order lambda-calculus" usually refers to system F, which doesn't even have dependent types.

What I'm getting at is that there are plenty of parts of GHC's flavor of Haskell that you can't depend on type inference for. You have to give type signatures for polymorphic recursion, for instance.

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

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

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?

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.

I'd say it's more like struggling to understand pointers: there's plenty of evidence that beginners struggle with it (e.g. all the monad tutorials), and if you're surprised by that then I'd guess you haven't done much teaching or interviewing. (One of my favorite interview questions requires people to understand escape sequences in a slightly more abstract way than usual, and you'd be surprised.)

In general I find that people do better with concrete examples and struggle with abstract rules. It's not at all obvious to a JavaScript programmer (for example) that asynchronous calls have anything to do with monads, and the designers of mainstream languages have to be very aware of their audience.

So, my question is how extending the type system might be turned into a concrete feature in a "mainstream" language. It's not too often that we need to prove things about red-black trees.

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

I'd say it's like only knowing what an array is instead of being able to generalize to an Enumerable/Iterable thing.

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

Reply on news.ycombinator.com