type-directed programming

From: Sebastian Hanowski <seha_at_informatik.uni-kiel.de>
Date: Fri, 15 Dec 2006 09:41:56 +0100

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 Fri Dec 15 2006 - 11:10:20 CET

This archive was generated by hypermail 2.3.0 : Fri Sep 20 2019 - 07:15:06 CEST