Problems in Haskell's Type-System

Question

Ive come across some answers (here in SO) saying that Haskell has many "dark corners" in its type system, and also some messy holes. Could someone elaborate on this?

Thanks in advance

Answer 1

I guess I should answer this, especially since two people so far have misinterpreted my remarks...

Regarding non-termination, the remark in question was slight hyperbole for dramatic effect, and referred to non-termination at the value level. This was in context of comparing Haskell to theorem provers, in an answer to someone who mentioned type-enforced correctness properties as something they particularly appreciated. In that sense, the presence of ⊥ inhabiting otherwise empty types is a "flaw", because it changes the meaning of a type like A -> B from "given an A, produces a B" into "given an A, either produces a B or crashes the program" which is, for obvious reasons, somewhat less satisfying from a proof-of-correctness standpoint.

It's also completely irrelevant to almost all day-to-day programming and no worse than any other general-purpose language because, of course, the possibility of non-termination is required for Turing-completeness.

I don't have any problem with UndecidableInstances. Actually, it bothers me less than ⊥ at the value level does because it only crashes GHC when compiling, not the finished program. OverlappingInstances is another matter, though, and the ad hoc mishmash of GHC extensions to provide little bits of things that would most naturally require dependent types certainly qualifies as "messy".

But keep in mind that most of the things I'm complaining about in Haskell are only a problem because of the otherwise very solid foundation. Most type systems in other statically typed languages aren't even coherent enough to be called "wrong" in comparison, and cleaning up the stuff I'm calling "messy" is an active and ongoing area of research.

Answer 2

Haskell's type system has no problems or messy holes, actually. Haskell 98 can be fully type-inferred. It possesses what is known as the "principal type" property, which is to say that any given expression has at most a single most general type. There are, however, a range of expressions which are good and useful and valid but do not type under Haskell 98. Most important of these are higher-ranked types. forall a b. (a -> b) -> a -> b is an (uninteresting) example of a rank-one type, which is to say that the forall is only at the very outside. forall b. -> (forall a. a -> a) -> b -> b is an example of a useless but possible type which is not rank-one, and cannot be expressed in Haskell98. Higher ranked types are one of many things which break the principal type property.

As one adds more and more extensions to the basic Haskell98 system, there begin to be tradeoffs introduced between the ability to write really powerful types which express both different types of polymorphism and different types of constraints and the ability to have as much code as possible completely type-inferred. At the very edges of what's possible, types can get messy and complicated, and occasionally you can run into things that seem like they should work but don't. But at that point, you're generally doing what's known as "type-level programming" where a great deal of your application logic has been embedded in the types themselves, and through a combination of typeclass tricks you've conned the compiler into, essentially, running the types as a program at compile time.

I disagree, by the way, with camccann's assertion that potential nontermination is a messy compromise in the type-checker. I think it's a perfectly useful feature, in fact a prerequisite for turning-completeness at the type level, and you only risk it if you explicitly ask the compiler to start allowing lots of dodgy stuff.