Bas van Dijk wrote:
Roberto Zunino wrote:
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'
On 9/18/07, apfelmus [EMAIL PROTECTED] wrote:
...in reality, foldr is (almost) the induction principle for natural numbers!
Oh yes, nice observation!
Afpelmus, thanks for your thorough answers!
regards,
Bas
___
Haskell-Cafe mailing list
Roberto Zunino wrote:
apfelmus wrote:
cons:: a - List e f a - List Nonempty f a
But unfortunately, finiteness is a special property that the type
system cannot guarantee. The above type signature for cons doesn't
work since the following would type check
bad :: a - List Nonempty
On 9/17/07, Roberto Zunino [EMAIL PROTECTED] 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:
David Menendez wrote:
Joachim Breitner wrote:
today while mowing the lawn, I thought how to statically prevent some
problems with infinte lists. I was wondering if it is possible to
somehow mark a list as one of finite/infinite/unknown and to mark
list-processing functions as whether they can
On 9/16/07, apfelmus [EMAIL PROTECTED] wrote:
But unfortunately, finiteness is a special property that the type system
cannot guarantee. The above type signature for cons doesn't work since
the following would type check
bad :: a - List Nonempty Finite a
bad x = let xs = cons x xs in
