On 10/12/07, Andrew Coppin <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe