Kudos! I had not been aware that Claus Reinke had written 'addtypes'
tools too in the form of text editor macros.
http://www.cs.kent.ac.uk/people/staff/cr3/toolbox/haskell/
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):
http://www.informatik.uni-kiel.de/~seha/plaw.html
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
undefined...
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
focus.
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
eventually.
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?
Cheers,
Sebastian
_______________________________________________
curry mailing list
curry_at_lists.RWTH-Aachen.DE
http://MailMan.RWTH-Aachen.DE/mailman/listinfo/curry
Received on Fr Jan 19 2007 - 22:17:20 CET