So, for example, if one of the base types of a lambda calculus was the natural numbers, the lambda theory would need to include rules to define equality over the natural numbers:<\/p>\n
- \n
- x = y if x=0 and y=0; and<\/li>\n
- x = y if x=s(x’) and y=s(y’) and x’ = y’<\/li>\n<\/ol>\n
So. Suppose we have a lambda-theory
. We can construct a corresponding category
. The objects in
\ncorresponds to the set of expressions of type
that contain a single free<\/em> variable of type
.<\/p>\n
The semantics<\/em> of the lambda-theory can be defined by a functor<\/em>; in particular, a cartesian closed<\/em> functor
that maps from
We describe how we build the category for the lambda theory in terms of a CCC using something called an interpretation function<\/em>. It’s really just a notation that allows us to describe the translation recursively. The interpretation function is written using brackets:
is the categorical interpretation of the type
So, first, we define an object for each type in
\ntype, which we call unit<\/em>. The idea behind unit is that we need to be able to talk about “functions” that either don’t take any real paramaters, or functions that don’t return anything. Unit is a type which contains exactly one atomic value. Since there’s only one possible value for unit, and unit doesn’t have any extractable sub-values, conceptually, it doesn’t ever need to be passed around. So it’s a “value” that never needs to get passed – perfect for a content-free placeholder.<\/p>\nAnyway, here we go with the base rules:<\/p>\n
- \n
<\/li>\n
<\/li>\n<\/ul>\n
Next, we need to define the typing rules for complex types:<\/p>\n
- \n
<\/li>\n
<\/li>\n<\/ul>\n
Now for the really interesting part. We need to look at type derivations – that is, the type inference rules of the lambda calculus – to show how to do the correspondences between more complicated expressions. Just like we did in lambda calculus, the type derivations are done with a context<\/em>
, containing a set of type judgements<\/em>. Each type judgement assigns a type to a lambda term. There are two translation rules for contexts:<\/p>\n
- \n
<\/li>\n
<\/li>\n<\/ul>\n
We also need to describe what to do with the values of the primitive types:<\/p>\n
- \n
- For each value
, there is an arrow
.<\/li>\n<\/ul>\n
And now the rest of the rules. Each of these is of the form
, where we’re saying that
entails the type judgement
. What it means is the object corresponding to the type information covering a type inference for an expression corresponds to the arrow in
- \n
- Unit evaluation:
. (A unit expression is a special arrow “!” to the unit object.)<\/li>\n
- Simple Typed Expressions:
. (A simple value expression is an arrow composing with ! to form an arrow from \u0393 to the type object of Cs type.)<\/li>\n
- Free Variables:
(A term which is a free variable of type A is an arrow from the product of \u0393 and the type object A to A; That is, an unknown value of type A is some arrow whose start point will be inferred by the continued interpretation of gamma, and which ends at A. So this is going to be an arrow from either unit or a parameter type to A – which is a statement that this expression evaluates to a value of type A.)<\/li>\n
- Inferred typed expressions:
, where
(If the type rules of \u0393 plus the judgement
, then the term
. This is almost the same as the previous rule: it says that this will evaluate to an arrow for an expression that results in type
- Function Abstraction:
. (A function maps to an arrow from the type context to an exponential
, which is a function from
- Function application:
,
,
. (function evaluation takes the eval arrow from the categorical exponent, and uses it to evaluate out the function.)<\/li>\n<\/ul>\n
There are also two projection rules for the decomposing categorical products, but they’re basically more of the same, and this is already dense enough.<\/p>\n
The intuition behind this is:<\/p>\n
- \n
- arrows<\/em> between types are families of values. A particular value is a particular arrow from unit to a type object.<\/li>\n
- the categorical exponent in a CC is exactly the same thing as a function type in \u03bb-calculus; and an arrow to an exponent is the same thing as a function value. Evaluating the function is using the categorical exponent’s eval arrow to “decompose” the exponent, and produce an arrow to the function’s result type; that<\/em> arrow is the value that the function evaluates to.<\/li>\n
- And the semantics – called functorial semantics – maps from the objects in this category,
Aside from the fact that this is actually a very clean way of defining the semantics of a not-so-simply typed lambda calculus, it’s also very useful in practice. There is a way of executing lambda calculus expressions as programs that is based on this, called the Categorical Abstract Machine<\/a>. The best performing lambda-calculus based programming language (and my personal all-time-favorite programming language), Objective-CAML<\/a> had its first implementation based on the CAM. (CAML stands for categorical abstract machine language.).<\/p>\n
From this, you can see how the CCCs and \u03bb-calculus are related. It turns out that that relation is not just cool, but downright useful<\/em>. Concepts from category theory – like monads, pullbacks, and functors are really useful things in programming languages! In some later posts, I’ll talk a bit about that. My current favorite programming language, Scala, is one of the languages where there’s a very active stream of work in applying categorical ideas to real-world programming problems.<\/p>\n","protected":false},"excerpt":{"rendered":"
Today I’m going to show you the basic idea behind the equivalency of closed cartesian categories and typed lambda calculus. I’ll do that by showing you how the \u03bb-theory of any simply typed lambda calculus can be mapped onto a CCC. First, let’s define the term “lambda theory”. In the simply typed lambda calculus, we […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[76,32],"tags":[],"class_list":["post-1735","post","type-post","status-publish","format-standard","hentry","category-category-theory","category-lambda-calculus"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-rZ","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1735","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=1735"}],"version-history":[{"count":2,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1735\/revisions"}],"predecessor-version":[{"id":3880,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1735\/revisions\/3880"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=1735"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=1735"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=1735"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}
- the categorical exponent in a CC is exactly the same thing as a function type in \u03bb-calculus; and an arrow to an exponent is the same thing as a function value. Evaluating the function is using the categorical exponent’s eval arrow to “decompose” the exponent, and produce an arrow to the function’s result type; that<\/em> arrow is the value that the function evaluates to.<\/li>\n
- arrows<\/em> between types are families of values. A particular value is a particular arrow from unit to a type object.<\/li>\n
- Unit evaluation:
- For each value