Church, Curry, and the code around the code

Consider these two lambda terms:

lambda x : Int  . x
lambda x : Bool . x

Now erase the annotations:

lambda x . x

Did we forget something about one term, or did we collapse two different terms into one?

Church-style and Curry-style typing give different answers to that question. In a Church-style presentation, the annotated terms are the objects being studied. The type annotation is part of the syntax, so the two identity functions above are different typed objects. They may erase to the same untyped term, but erasure is a translation, not equality.

In a Curry-style presentation, the untyped term is the object being studied. The type system makes judgments about it:

lambda x . x : Int  -> Int
lambda x . x : Bool -> Bool
lambda x . x : A    -> A

So the difference is not only whether the programmer writes annotations. It is a difference in what the theory treats as the program. Church-style typing builds type information into the term language. Curry-style typing keeps the raw term language smaller, then assigns types by a separate relation. That difference affects equality, erasure, inference, elaboration, and the shape of the metatheory.

Once this distinction is visible, similar placement questions start appearing in ordinary codebases. A codebase is rarely just executable code. It also contains claims about the code: types, tests, examples, documentation, contracts, comments, specifications. Different ecosystems put those claims at different distances from the program.

Modern type systems give familiar examples. In Rust or TypeScript, type syntax is part of the source language and the compiler understands it. In Python, type annotations are parsed and preserved, but the core language does not act on them in any way. In JSDoc, type information lives in comments. In TypeScript declaration files, type information can live in separate .d.ts files. The same happens in Ruby and its .rbs files.

The same pattern appears outside types. Python docstrings are real syntax: the first string in a function body becomes documentation metadata. JSDoc documentation is written as comments for external tools. Racket documentation is commonly written in Scribble, a separate documentation language. Literate programming reverses the usual relationship even further: the document becomes the main artifact, and code is extracted from it. Tests also move around: Rust and Racket often keep small tests near the code, while most ecosystems put tests in separate files or directories.

These examples are not all instances of Church-style or Curry-style typing in the formal sense. They are ordinary versions of the same placement problem. Some facts are pulled into the object language. Some facts sit in comments, sidecar files, test suites, documentation systems, or external tools.

References

This is like a reading map for the idea and its afterlife.

• H. B. Curry, “Functionality in Combinatory Logic” (1934).

  The historical root of the Curry side. Curry studies functionality over combinatory objects, rather than starting with a syntax where every variable occurrence already carries a type. This is one source of the later idea that types can be assigned to terms.

  PNAS page


• Alonzo Church, “A Formulation of the Simple Theory of Types” (1940).

  The historical root of the Church side. Church builds type information directly into the formal language. If you want the original “typed terms are the objects” attitude, this is the source.

  PDF


• J. Roger Hindley, “The Principal Type-Scheme of an Object in Combinatory Logic” (1969).

  A key bridge from Curry’s older world into programming-language type inference. Hindley proves that typable objects can have principal type-schemes. This is the mathematical ancestor of the feeling that a compiler can recover the best general type of an unannotated expression.

  PDF


• Robin Milner, “A Theory of Type Polymorphism in Programming” (1978).

  This is where the inference story becomes a programming-language story. Milner connects polymorphic type checking with ML, and makes the Curry-style experience familiar to programmers: write a small amount of syntax, and let the system infer a general type.

  PDF


• Frank Pfenning, “Church and Curry: Combining Intrinsic and Extrinsic Typing” (2008).

  The most useful single modern reference for the conceptual distinction. Pfenning presents Church-style typing as intrinsic and Curry-style typing as extrinsic, then shows why it can be useful to combine the two. This is also a good place to think about equality, erasure, substitution, and the cost of moving between typed and untyped views.

  PDF


• Adriana Compagnoni and Healfdene Goguen, “Relating Church-Style and Curry-Style Subtyping” (2011).

  A technical descendant showing that the distinction remains alive beyond introductory lambda calculus. In richer calculi, the choice of style can interact with subtyping and computation rules. This is where “where do types live?” becomes more than presentation.

  arXiv page


• Gilad Bracha, “Pluggable Type Systems”.

  Bracha argues for type systems that are optional and pluggable: useful to tools, but not required by the runtime semantics of the language. That makes the paper a natural modern companion to the Church/Curry distinction. It treats types as information that can be attached to a language without making the language depend on one mandatory type discipline.

  PDF


• Sam Tobin-Hochstadt and Matthias Felleisen, “The Design and Implementation of Typed Scheme”.

  Typed Scheme is about adding a typed layer to an existing untyped language. The paper describes type annotations as design information that programmers otherwise have to rediscover when maintaining growing scripts. That makes it a practical version of the same old question: when an untyped program acquires types, are those types a new language of programs, or a structured account of programs that were already there?

  arXiv page


• Jeremy Siek and Walid Taha, “Gradual Typing for Functional Languages”.

  Gradual typing is useful here because it gives types a place at the boundary. Some parts of a program may be statically typed, other parts may remain dynamically typed, and runtime checks mediate between them. The type information is neither merely external documentation nor simply erased decoration. It becomes a source of boundary behavior.

  PDF


• Python doctest.

  Doctest turns examples in documentation into executable checks. The same text teaches a reader what should happen and gives a tool something to verify. This makes it a small but concrete case where documentation, examples, and tests occupy the same piece of source text.

  doctest documentation


• Specification by Example.

  Specification by Example is a useful non-type-theory analogue. It tries to make examples serve several roles at once: requirements, tests, and documentation of existing behavior. The interesting part is the attempt to avoid three drifting descriptions of the same system. A single example can become a claim for humans and a check for machines.

  Martin Fowler's note


• Literate programming: code inside documentation.

  Most documentation systems attach prose to code. Literate programming makes the opposite move: the human-facing document is primary, and source files are produced from it. It is an older and more radical answer to the same placement question.

  Knuth, “Literate Programming”