Re: type-directed programming

From: Bernd Brassel <>
Date: Fri, 15 Dec 2006 12:34:38 +0100

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)
  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 .)



curry mailing list
Received on Fr Dez 15 2006 - 15:05:21 CET

This archive was generated by hypermail 2.3.0 : Mo Dez 04 2023 - 07:15:08 CET