Proofs that do things


...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

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
and the 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

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.


Terminological confusion

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

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...