Curry-Howard isomorphism

Curry-Howard isomorphism

Back

Every type can be interpreted as a proposition - a statement or a judgment that may be true or false. Such a proposition is considered true if the type is inhabited and false if it isn’t. In particular, a logical implication is true if the function type corresponding to it is inhabited, or a function exists of that type. An example of a function is a proof of a theorem.