3 ms·
> 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
by tome 10y ago
> 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!
- wz1000 10y agoI 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.
- notjack 10y ago*Alexis, not Alex
- tome 10y agoThanks. Can't edit any more though.