O'Reilly logo

Functional Programming: A PragPub Anthology by Michael Swaine

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

Propositions Are Types, and Proofs Are Programs

We can use any values of arbitrary complexity inside type expressions, not just simple values like numbers. We can even encode logical propositions too, and use these to express pre and post conditions, and more. For example, the following represents a property of equality—that when two things are equal, then what we can do with one thing, we can do with the other.

 foo2 :: (A:Type)(P:A -> Type)(a,b:A)Eq A a b -> P(a) -> P(b)

We can do more than just encode logical propositions: we can work with proofs of them entirely inside the language as well. If you’ve done any logic before, you may recognize the following as a statement of transitivity of implication. “If B implies C, and A implies B, then ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required