[Haskell-cafe] Re: Type-level arithmetic

Tim Chevalier catamorphism at gmail.com
Fri Oct 12 13:37:32 EDT 2007

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:
The paper at:
has an example like your head/tail example (in section 3, "Vectors and
finite sets").


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

More information about the Haskell-Cafe mailing list