Re: [Haskell-cafe] Re: Type-Marking finite/infinte lists?
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-Marking finite/infinte lists?
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: 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... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Type-Marking finite/infinte lists?
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 xs In other words, Haskell's type system doesn't detect infinite recursion. Exactly. Haskell allows free unrestrained recursion, and this is the source of the problem. Instead we could limit ourselves to structural recursion and then we can guarantee that even if we write recursive code, the results will always be finite. For details there's Turner's paper on Total Functional Programming: http://www.cs.mdx.ac.uk/staffpages/dat/sblp1.pdf -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
