[Haskell-cafe] Re: Type-level arithmetic

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... ;-)