Hacker News Reader

> Haskell is too limiting—the compiler cannot deduce constraints I can solve in my head in seconds

Alex, if you could do a post with concrete examples of these that would be really helpful!

I haven't had too many problems of this kind, but it does start becoming very painful if you work with GHC.TypeLits. It becomes very annoying using unsafeCoerce to "prove" to GHC that (a-1)+1 ~ a and other such trivialites. I realise solving these in the general case require the type checker to be equipped with a fully fledged SMT solver, but what I find really annoying is when GHC.TypeLits lacks the mechanism to solve simple contraints that you can get for free by lifting a simple inductive Nat type.

For instance GHC doesn't know that + is injective, so can't deduce that given a ~ m+1 and a ~ n+1, m ~ n.

*Alexis, not Alex

Thanks. Can't edit any more though.

Reply on news.ycombinator.com