Hello,
I'd had liked to post about how /static typing/ combined with locally
declared /free variables/ as available in Curry allows for a method to
incrementally refine partially implemented programs with aid from the
typechecker.
As an example I will show how to develop addition with this method.
data Nat = Zero | Suc Nat
prec :: a -> (Nat -> a -> a) -> Nat -> a
prec Zero mz _ = mz
prec (Suc n) mz ms = ms n (prec mz ms n)
We start by declaring the type together with a partial implementation
abstracting subprograms with free variables.
plus :: Nat -> Nat -> Nat
plus = \x -> prec x mz ms where mz,ms free
The idea is to attach a 'cursor' to our program pointing at the
subprogram that we are going to implement next:
cursor = mz
where
plus :: Nat -> Nat -> Nat
plus = \x -> prec x mz ms
mz,ms free
Having saved this program to a file we invoke Bernd Brassel's addtypes
tool on it which ships with the PAKCS distribution of Curry. And after
having reloaded the file into our editor we will find our top-level
binding equipped with a suitable signature.
cursor :: Nat -> Nat
cursor = z
where
plus :: Nat -> Nat -> Nat
plus = \x -> prec x mz ms
mz,ms free
Which may help us proceeding with our programming task.
cursor = mz
where
plus :: Nat -> Nat -> Nat
plus = \x -> prec x mz ms
mz :: Nat -> Nat
mz = \y -> y
ms free
We do this again with our cursor updated to the next 'gap' in our
program which is yet to be 'filled'.
cursor :: Nat -> (Nat -> Nat) -> Nat -> Nat
cursor = ms
where
plus :: Nat -> Nat -> Nat
plus = \x -> prec x z s
mz :: Nat -> Nat
mz = \y -> y
ms free
And we'll again be able to complete our program with help from a typing.
plus :: Nat -> Nat -> Nat
plus = \x -> prec x z s
where
mz :: Nat -> Nat
mz = \y -> y
ms :: Nat -> (Nat -> Nat) -> Nat -> Nat
ms = \x -> \plusx -> \y -> Suc (plusx y)
I should note that Conor McBride uses exactly this program to show how
little primitive recursion with simple types tells us about the tasks to
be accomplish by the subprograms compared to constructing programs with
induction principles in a dependently typed setting. For example we have
to ensure ourselves that in the successor case we are to write a program
that /for all x, y/ will compute /plus (Suc x) y/ given /plus x y/ .
But I had anyway liked to give it as a demo for how easy it is in Curry
to focus the typechecker on subparts of programs, because I think that
/free variables/ are crucial to this method. In a genuine functional
setting one could implement subprograms partially with a little help
from
_|_ :: a
_|_ = _|_
which inhabits the intersection of all types.
Thus
plus = \x -> prec x _|_ _|_
typechecks but we can't get no specific signatures.
Which we would get otherwise by lambda-abstracting subprograms
cursor = \z s -> let plus = \x -> prec x z s :: Nat -> Nat in ()
but this gives a less focused notion. And combining stragegies
(1) cursor = \z -> let plus = \x -> prec x z _|_ :: Nat -> Nat in ()
(2) cursor = \s -> let plus = \x -> prec x _|_ s :: Nat -> Nat in ()
is likely to make your program too much a moving target.
Since (simple) types provide a machine-checkable (partial)
specification, it's always a good idea to start out with them first.
Moreover, in order to write total, non-divergent programs it's indicated
to use the eliminator associated with the type of a programs input. Many
of these are already contained in the Curry prelude.
But I can introduce this methodology only by example. I've put up a
screencast showing a session from which the first listings in this mail
could be taken as 'snapshots'.
http://informatik.uni-kiel.de/~seha/plus.html
Paraphrasing T. Sheard this method might be regarded as a way of
'putting Curry to work the Curry-Howard Isomorphism'.
Cheers,
Sebastian
--
\ C
/\ U |-
r Free Your Variables...and Your Programs Will Follow
r
y
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Dez 15 2006 - 11:10:20 CET