[Haskell-cafe] Re: Type-Marking finite/infinte lists?

[Bas van Dijk]

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.

regards,

Bas

P.S. I also asked this on #haskell but I had to go away; Maybe I
missed the answer...