[Haskell-cafe] Re: Type-level arithmetic

[Tim Chevalier]

On 10/12/07, Andrew Coppin <andrewcoppin at btinternet.com> wrote:
> 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.
>

You might be interested in Epigram:
http://e-pig.org/
The paper at:
http://www.e-pig.org/downloads/epigram-notes.pdf
has an example like your head/tail example (in section 3, "Vectors and
finite sets").

Cheers,
Tim

-- 
Tim Chevalier * catamorphism.org * Often in error, never in doubt
"I always feel I have to take a stand and there's always someone on
hand to hate me for standing there / I always feel i have to open my
mouth and every time I do I offend someone somewhere" -- Ani DiFranco