[Haskell-cafe] Re: Type-level arithmetic

[Andrew Coppin]

I was actually thinking more along the lines of a programming language 
where you can just write

  head :: (n > 1) => List n x -> x

  tail :: List n x -> List (n-1) x

  (++) :: List n x -> List m x -> List (n+m) x

and so forth. You know, instead of the elaborate simulations crafted out 
of systems that weren't meant to do this stuff.

Of course, the integer case is probably fairly easy. I suspect the issue 
is that as soon as you try to do this kind of thing, you develop a 
terminal case of wanting to hyper-generalise everything which then 
directly results in an incomprehensible mess... ;-)