[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)

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.



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 mailing list