[Haskell-cafe] Re: Type-Marking finite/infinte lists?
Bas van Dijk
v.dijk.bas at gmail.com
Mon Sep 17 18:46:06 EDT 2007
On 9/17/07, Roberto Zunino <zunino at di.unipi.it> wrote:
> 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)
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.
P.S. I also asked this on #haskell but I had to go away; Maybe I
missed the answer...
More information about the Haskell-Cafe