On 10/12/07, Andrew Coppin
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