17 Sep
2007
17 Sep
'07
10:46 p.m.
On 9/17/07, Roberto Zunino
I thought this was possible with GADTs (is it?):
data Z data S n data List a len where Nil :: List a Z Cons:: a -> List a len -> List a (S len)
Slightly related: The other day I was playing with exactly this GADT. See: http://hpaste.org/2707 My aim was to define a function like 'concat' in terms of 'foldr' but I was unable to do so. Can this be done? Also I was unable to define the function 'fromList :: [a] -> ListN a n'. This makes sense of course because statically the size of the list is unknown. However maybe existential quantification can help but I'm not sure how. regards, Bas P.S. I also asked this on #haskell but I had to go away; Maybe I missed the answer...