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... ;-)
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
