Church and Curry
When defining a programming language and its typing rules there are two main approaches:
The intrinsic approach, also called Church-style (named after Alonzo Church, discoverer of the lambda calculus). In this approach, every term in a language intrinsically has a type which we can check. Some languages which exemplify this approach are Haskell, OCaml, Agda, and Coq. Branching out from functional languages, C / C++ and Java are also Church-style because terms have built-in types.
The extrinsic approach, also called Curry-style (named after Haskell Curry, founder of combinatory logic). In this style, a term in a language don't necessarily have a built-in type, though you may still be able to typecheck it. That is, types classify (untyped) terms. Most lisps are good examples of this approach. So is NuPRL.
In LVCA
The reason I bring up this distinction is to clarify my thoughts on the two approaches as they relate to LVCA.
A design decision that's been nagging at me for a while is, how are terms stored in LVCA? Is it Church-style, with statics attached? Or is it Curry-style, just the term without reference to its statics?
I recently came to a conclusion that I'm happy with, realizing that allowing
terms to be stored independently of their statics is strictly more general. For
example, suppose we have some term t
, typed by some statics s
. Now, if we
want to operate à la Curry, we can simply store the term t
. Then t
exists
as an essentially untyped term in our store. Yet if we have a statics s
, it's
possible to check t
against s
. However, if we prefer to operate à la
Church, we can define typed(term; statics) = typed(term; statics)
and store
the term typed(t; s)
. Now our term is defined with reference to its statics,
and we can check that it's a valid term if it typechecks.