Re: type-directed programming

From: Sebastian Hanowski <>
Date: Fri, 19 Jan 2007 12:55:23 +0100

Kudos! I had not been aware that Claus Reinke had written 'addtypes'
tools too in the form of text editor macros.

That's a nice thing to have too! Saves one from having to reload the
whole file. (Its nice in place updates feel a bit like having websites
with Ajax now.)

On can have fun with doing interactive theorem proving this way, showing
things like the peirce law being a theorem of classical logic

        Dec a -> ((a -> b) -> a) -> a

using some ingredients missing from the prelude

        data False

        type Not a = a -> False

        magic :: False -> a
        magic = \_ -> failed

        type Dec a = Either a (Not a)

If you've got a minute, let's pull over to the 'whiteboard' (if you can
stand compsci à la youtube once more):

 I don't want to get too repetitive on this, but my point was to show
that /free variables/ seem to be superior over lambda binding or
undefined for making partial programs checkable.

Using undefined brings a dangerous semantics. From the logical
perspective it's like claiming to have proved something by contradiction
assuming that contradiction straight away. Well, this used to happen to
me in maths then...

Moreover, computationally you can't decide when a program is ready.
Variables are much neater since a groundness analysis seems a reasonable
effort. But I didn't want to have to rely on a check for occurences of

By lambda abstracting you can't give the 'cursor' the type of the 'hole'
in your program, because it will have to be the domain of a functional
type. And what to do when you've got several sub-problems to tackle?
Abstracting them all at once gives an unfocused notion.

And Mixing both techniques by using only one parameter and other yet
unknowns as undefined will require heavy rewriting when moving the

What I had posted about after all was just functional-logical things I
found handy when tinkering with Curry:

- inductive datatypes w/ non-determinism

        'Generators' can help to get a clue of the shape of data, for
        example when facing intricated nested datatypes.

- static typing w/ free variables

        Circumvent getting stuck by abstracting yet unsolved
        sub-problems allowing to get help form the type-checker

Maybe one can imagine programs marked-up in html like it's done for the
Curry docs but with unknown programs rendered as input forms?


curry mailing list
Received on Fri Jan 19 2007 - 22:17:20 CET

This archive was generated by hypermail 2.3.0 : Mon Sep 16 2019 - 07:15:05 CEST