I cannot say that I understand everything about what you wrote,
Sebastian. (One of the reasons is that the code in the mail differs from
the really nice presentation on your website, esp. in being not type
correct.) But after looking at the animation, I have an idea what you
might drive at. Is it maybe something like this?
For our data Structure
data Nat = Z | S Nat
We define a standard folding
foldNat :: a -> (a -> a) -> Nat -> a
foldNat z _ Z = z
foldNat z s (S x) = s (foldNat z s x)
Now we want to use this fold to define plus, but are not sure about the
functions to use.
plus :: Nat -> Nat -> Nat
plus = foldNat z s
where z,s free
Old School says, first thing about writing a function is its type. To
get the type for z and s you have the nice idea to use addtypes:
cursor = (z,s)
where
z,s free
plus :: Nat -> Nat -> Nat
plus = foldNat z s
Now you get for the type of cursor:
cursor :: (Nat -> Nat,(Nat -> Nat) -> Nat -> Nat)
and some thinking gives us
plus = foldNat id (S .)
Right?
Greetings
Bernd
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Dez 15 2006 - 15:05:21 CET