[Haskell-beginners] foldr for Nats

[kane96 at gmx.de]

@Stephan thanks for the code so far.
@Daniel it should look like foldrNat a b S(S(S(S(Z)))) gives a(a(a(a(b))))


The thing is the definition have to be
-------- Original-Nachricht --------
> Datum: Mon, 1 Feb 2010 21:56:14 +0000
> Von: Stephen Tetley <stephen.tetley at gmail.com>
> An: kane96 at gmx.de
> CC: Beginners at haskell.org
> Betreff: Re: [Haskell-beginners] foldr for Nats

> Hello
> 
> I'm suspecting this isn't homework as you've waited a week so would
> presumably have missed a deadline.
> 
> As Daniel Fischer wrote, one view of folds is that they replace the
> constructors of a data type, code follows...
> 
> 
> data Nat = Z | S Nat   deriving (Eq,Ord,Show)
> 
> 
> -- Look at the type of foldr...
> 
> -- *GHCi> :t foldr
> -- foldr :: (a -> b -> b) -> b -> [a] -> b
> 
> -- It has 2 'constructor replacements':
> -- (a -> b -> b) & b
> 
> -- Replacing Z is easy, we can get some code to compile
> -- by avoiding the hard bit with a wildcard pattern "_"...
> 
> foldrNat1 :: unknown -> b -> Nat -> b
> foldrNat1 _ b Z = b
> 
> -- What to do about the constructor (S ..) takes a bit more
> -- thought or at least some experimenting. I'll do the later...
> 
> -- One thing to try, is to simply translate foldr with as few
> -- changes as possible:
> 
> -- foldr            :: (a -> b -> b) -> b -> [a] -> b
> -- foldr _ z []     =  z
> -- foldr f z (x:xs) =  f x (foldr f z xs)
> 
> -- Unfortunately this leads to a problem:
> 
> foldrNat2 :: (Nat -> b -> b) -> b -> Nat -> b
> foldrNat2 f b Z     = b     -- Z case is the same as before
> foldrNat2 f b (S n) = f undefined (foldrNat2 f b n) -- Arggh! undefined
> 
> -- undefined is useful for prototyping, but its a real
> -- problem for running code!
> 
> -- Actually I had another problem as well...
> --
> -- The difference between Nat and [a] is that List 'carries' some data
> -- therefore (Nat -> b -> b) on Nat is not equivalent to (a -> b -> b)
> -- on [a].
> 
> -- So rather than change the type signature first, get rid of the
> -- undefined and see what happens
> 
> foldrNat3 f b Z     = b
> foldrNat3 f b (S n) = f (foldrNat3 f b n)
> 
> -- *GHCi> :t foldrNat3
> -- > (t -> t) -> t -> Nat -> t
> 
> -- GHCi likes to call type variables t, but the signature is equal to
> 
> -- foldrNat3 :: (b -> b) -> b -> Nat -> b
> 
> 
> -- This looks promising - it typechecks!
> -- So try a test:
> 
> fromNat :: Nat -> Int
> fromNat n = foldrNat3 (+1) 0 n
> 
> demo1 = fromNat (S (S (S Z)))   -- 3 ??
> 
> -- By experimenting we seem to have a good answer,
> -- other people might prefer a more rigorous proof though.

-- 
NEU: Mit GMX DSL über 1000,- ¿ sparen!
http://portal.gmx.net/de/go/dsl02