Read on Medium

Church and Curry Types

31 March 2022
Two Logicians

Alonzo Church was an American logician. He invented the lambda calculus and used it in 1934 to answer negatively Hilbert and Ackermann’s Entscheidungsproblem, the question of whether there’s an algorithm to solve every yes-or-no mathematical question. Turing got the same result with Turing machines independently a few months later.

Haskell Curry was another logician, also American, who developed the field of combinatory logic. Formally modeling variable binding is surprisingly subtle, and the notion of a combinator allows to eliminate both the binders in quantifiers as well as in the lambda calculus. The programming language Haskell is named for him, as is the operation of currying. The Curry–Howard isomorphism relates propositions and proofs to types and programs.

Figure 1. The other Curry–Howard isomorphism.

Two Notions of Type

For Church, types are like parts of speech: just as one cannot use an adverb where a verb is needed, one cannot use a string in place of an integer. Sometimes Church types are called “intrinsic” types, because the type of a value is an intrinsic part of the value. Intrinsic types are easy to check at compile time.

For Curry, types are filters that select subsets of the universal set of all values. An eagle is in the intersection of the set of birds and the set of national symbols. Sometimes Curry types are called “extrinsic” types, because the type of a value is something you test with a separate filter. Extrinsic types are usually checked at runtime.

Most compiled languages support both compile-time types and runtime errors, but because of their focus on Church types, the language designers don’t often think of runtime errors as being part of the type system. Interpreted, dynamically-typed languages like JavaScript and Python started with only Curry types, but industrial users found that some form of type checking before deployment was necessary for reliable products, so hundreds of millions of dollars have been spent on retrofitting them with Church types; see, for example, Microsoft’s TypeScript, Facebook’s Flow, Google’s Closure Compiler, and MyPy.

A few languages have successfully moved some Curry types to compile time. TypeScript, for instance, mostly uses Church types, but also supports narrowing; in particular, type predicates are Curry types. Eiffel’s assertions are checked at runtime, but one can use the AutoProof typechecking tool to show that the assertions necessarily hold even without running the code. AutoProof uses the Z3 SMT solver to work its magic.

Operational semantics

There are lots of platforms for formalizing the semantics of programming languages. K Framework is a popular one on which dozens of languages and virtual machines, particularly those used on blockchains, have been formalized.

Specifying an operational semantics involves giving a formal grammar for the state of the machine together with rewrite rules that say how the state changes over time. It may also include equations that hold on terms; for instance, in pi calculus concurrent execution is commutative, so P | Q = Q | P.

The formal grammar typically defines the different parts of the state as different symbols in the grammar, called “sorts”. For simple languages like lambda calculus or pi calculus, the state is trivial: there’s a single sort for terms. For more complicated languages like the Java virtual machine, there’s the stack, the heap, the registers, the memory, etc.

Such a specification gives rise to a category Th (for “theory”) in which the objects are sorts and the morphisms are generated by the production rules of the grammar. We can use the Yoneda embedding to embed the theory into a topos, followed by the functor taking each representable to its poset of subobjects. Then we can use the Grothendieck construction on the resulting functor to get a category Type whose objects are pairs (S, T ⊆ S) where S is a sort (a Church type) and T is a Curry type filtering the values of S. The morphisms of Type from (S, T) to (S’, T’) are compositions of production rules p: S → S’ such that pT ⊆ pT’. The resulting category is a formalization of the programming language in the calculus of constructions, the basis of the Coq theorem prover. You can read more in the paper “Native Type Theory” I co-authored with Christian Williams.

The upshot is that one can write predicates about programs that include reasoning about possible reductions, like whether security invariants are always preserved. Each release of Silvermint’s language project Symmetry will be building towards that eventual goal.