Functional Programming: A PragPub Anthology

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