Climbing the infinite ladder of abstraction

Re:Climbing the infinite ladder of abstraction by tome on Sunday August 14, 2016 @07:12AM (#12285146)

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

[ Parent | on HN ]

Re:Climbing the infinite ladder of abstraction by wz1000 on Sunday August 14, 2016 @10:37AM (#12285728)

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.

[ Parent | on HN ]

Re:Climbing the infinite ladder of abstraction by notjack on Tuesday August 16, 2016 @04:50PM (#12300543)

*Alexis, not Alex

[ Parent | on HN ]

Re:Climbing the infinite ladder of abstraction by tome on Wednesday August 17, 2016 @04:17AM (#12303152)

Thanks. Can't edit any more though.

[ Parent | on HN ]