Home » forums » LtU Forum

Proofs that do things

Sigfpe

...sometimes you can write useful Haskell code merely by writing something that type checks successfully. Often there's only one way to write the code to have the correct type. Going one step further: the Curry-Howard isomorphism says that logical propositions corresponds to types. So here's a way to write code: pick a theorem, find the corresponding type, and find a function of that type.

Learning category theory and formal logic by writing proofs in Haskell.

Cool. :-D

By genneth at 2006-11-24 20:28 | LtU Forum | previous forum topic | next forum topic | other blogs | 5017 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Haskell can do some of the proofs itself

Incidentally, Haskell can do some of the proofs itself: you only need
to write a type, and you get the corresponding program. Please see
DJinn
and the de-typechecker


http://pobox.com/~oleg/ftp/Haskell/types.html#de-typechecker

The latter shows that the typeclass facility of Haskell itself is a
theorem prover. You write a type, and the typechecker gives you a
program.

By Oleg at Fri, 2006-11-24 23:35 | login or register to post comments

Typechecking is verification

Hi. Interesting food for thought IMHO. I am generally more the verification guy (in the automaton theory kind of sense), but when I had my first real class about type systems etc. it occurred to me that this is actually all exactly the same just rephrased.

A verifier is a type checker. A valid program is a correctly typed program. The process of validation is called type checking. Types can be arbitrarily complex as can formal specifications. However, the more complex they get, the harder they are to verify (speak "to typecheck"). Some type systems are even undecidable - just as some formal specification languages could be.

Eric

By ericbodden at Mon, 2006-11-27 04:57 | login or register to post comments

Terminological confusion

In parts of the literature validation, verification and typechecking are separated for good reasons.

By Kay Schluehr at Mon, 2006-11-27 14:26 | login or register to post comments

Yoneda lemma

One of the earlier posts on the Yoneda lemma was one of the coolest things I've ever seen. Now if only I was interested in something that I could explain to my girlfriend...

By genneth at Tue, 2006-11-28 11:36 | login or register to post comments