module Cat.CartesianClosed.Lambda

Simply-typed lambda calculus๐Ÿ”—

The simply typed (STLC) is a very small typed programming language very strongly associated with Cartesian closed categories. In this module, we define the syntax for STLC with base types, and inhabitants of these, given by the objects and morphisms of an arbitrary CCC. This syntax can be used to reflect morphisms of a CCC, making the โ€œstructuralโ€ morphisms explicit. We then build a normalisation procedure, which can be used to effectively compare morphisms in the CCC.

The types of STLC are generated by function types a `โ‡’ b and product types a `ร— b, along with an inclusion of objects from the target category to serve as โ€œbase typesโ€, e.g.ย the natural numbers. The contexts are simply lists of types.

data Ty : Type o where
  _`ร—_ : Ty โ†’ Ty โ†’ Ty
  _`โ‡’_ : Ty โ†’ Ty โ†’ Ty
  `_   : Ob โ†’ Ty

data Cx : Type o where
  โˆ…   : Cx
  _,_ : Cx โ†’ Ty โ†’ Cx

To use contexts, we introduce variables. A variable gives an index in where something of type can be found. It can either be right here, in which case we stop, or it can be further back in the context, and we must pop the top variable off to get to it.

data Var : Cx โ†’ Ty โ†’ Type o where
  stop : Var (ฮ“ , ฯ„) ฯ„
  pop  : Var ฮ“ ฯ„ โ†’ Var (ฮ“ , ฯƒ) ฯ„

We can now write down the type of expressions, or, really, of typing judgements. An inhabitant of Expr ฮ“ ฯ„ is a tree representing a complete derivation of something of type ฯ„. We insist on the name expression rather than term since there are more expressions than there are terms: For example, in the context the expressions and denote the same term.

data Expr ฮ“ where
  `var    : Var ฮ“ ฯ„             โ†’ Expr ฮ“ ฯ„
  `ฯ€โ‚     : Expr ฮ“ (ฯ„ `ร— ฯƒ)     โ†’ Expr ฮ“ ฯ„
  `ฯ€โ‚‚     : Expr ฮ“ (ฯ„ `ร— ฯƒ)     โ†’ Expr ฮ“ ฯƒ
  `โŸจ_,_โŸฉ  : Expr ฮ“ ฯ„ โ†’ Expr ฮ“ ฯƒ โ†’ Expr ฮ“ (ฯ„ `ร— ฯƒ)
  `ฮป      : Expr (ฮ“ , ฯ„) ฯƒ      โ†’ Expr ฮ“ (ฯ„ `โ‡’ ฯƒ)
  `$      : Expr ฮ“ (ฯ„ `โ‡’ ฯƒ)     โ†’ Expr ฮ“ ฯ„ โ†’ Expr ฮ“ ฯƒ
  `_      : Hom โŸฆ ฮ“ โŸงแถœ โŸฆ ฯ„ โŸงแต—   โ†’ Expr ฮ“ ฯ„

Using the Cartesian closed structure, we can interpret types, contexts, variables and expressions in terms of the structural morphisms: For example, the empty context is interpreted by the terminal object, and1 the zeroth variable is given by the second projection map

โŸฆ X `ร— Y โŸงแต— = โŸฆ X โŸงแต— โŠ—โ‚€ โŸฆ Y โŸงแต—
โŸฆ X `โ‡’ Y โŸงแต— = Exp.B^A โŸฆ X โŸงแต— โŸฆ Y โŸงแต—
โŸฆ ` X โŸงแต—    = X

โŸฆ ฮ“ , ฯ„ โŸงแถœ = โŸฆ ฮ“ โŸงแถœ โŠ—โ‚€ โŸฆ ฯ„ โŸงแต—
โŸฆ โˆ… โŸงแถœ     = term

โŸฆ_โŸงโฟ : Var ฮ“ ฯ„ โ†’ Hom โŸฆ ฮ“ โŸงแถœ โŸฆ ฯ„ โŸงแต—
โŸฆ stop โŸงโฟ  = ฯ€โ‚‚
โŸฆ pop x โŸงโฟ = โŸฆ x โŸงโฟ โˆ˜ ฯ€โ‚

โŸฆ_โŸงแต‰ : Expr ฮ“ ฯ„ โ†’ Hom โŸฆ ฮ“ โŸงแถœ โŸฆ ฯ„ โŸงแต—
โŸฆ `var x     โŸงแต‰ = โŸฆ x โŸงโฟ
โŸฆ `ฯ€โ‚ p      โŸงแต‰ = ฯ€โ‚ โˆ˜ โŸฆ p โŸงแต‰
โŸฆ `ฯ€โ‚‚ p      โŸงแต‰ = ฯ€โ‚‚ โˆ˜ โŸฆ p โŸงแต‰
โŸฆ `โŸจ a , b โŸฉ โŸงแต‰ = โŸจ โŸฆ a โŸงแต‰ , โŸฆ b โŸงแต‰ โŸฉ
โŸฆ `ฮป e       โŸงแต‰ = ฦ› โŸฆ e โŸงแต‰
โŸฆ `$ f x     โŸงแต‰ = ev โˆ˜ โŸจ โŸฆ f โŸงแต‰ , โŸฆ x โŸงแต‰ โŸฉ
โŸฆ ` x        โŸงแต‰ = x

The type of expressions could (and, to some extent, should) be higher-inductive-recursive, with path constructors expressing the rules โ€” the universal properties that we want to capture. However, this would significantly complicate the development of the rest of this module. We choose to work with raw derivations, instead, for convenience. Equality of Expr being coarser than that of Hom does not significantly affect our application, which is metaprogramming.

Context inclusions๐Ÿ”—

We will implement our semantics using normalisation by evaluation, by embedding our expressions into a domain where the judgemental equalities of the object-level are also judgemental at the meta-level. We choose presheaves on a category of inclusions, where the objects are contexts and the maps indicate that, starting from you can get to by dropping some of the variables, and keeping everything else in-order.

data Ren : Cx โ†’ Cx โ†’ Type (o โŠ” โ„“) where
  stop : Ren ฮ“ ฮ“
  drop : Ren ฮ“ ฮ” โ†’ Ren (ฮ“ , ฯ„) ฮ”
  keep : Ren ฮ“ ฮ” โ†’ Ren (ฮ“ , ฯ„) (ฮ” , ฯ„)

Here we must confess to another crime: Since our (types, hence our) contexts include objects of the base category, they do not form a set: therefore, neither does the type Ren of context inclusions. This means that we can not use Ren as the morphisms in a (pre)category. This could be remedied by instead working relative to a given set of base types, which are equipped with a map into semantic objects. This does not significantly alter the development, but it would be an additional inconvenience.

Regardless, we can define composition of context inclusions by recursion, and, if necessary, we could prove that this is associative and unital. However, since we are not building an actual category of presheaves (only gesturing towards one), we omit these proofs.

_โˆ˜สณ_ : โˆ€ {ฮ“ ฮ” ฮ˜} โ†’ Ren ฮ“ ฮ” โ†’ Ren ฮ” ฮ˜ โ†’ Ren ฮ“ ฮ˜
stop   โˆ˜สณ ฯ      = ฯ
drop ฯƒ โˆ˜สณ ฯ      = drop (ฯƒ โˆ˜สณ ฯ)
keep ฯƒ โˆ˜สณ stop   = keep ฯƒ
keep ฯƒ โˆ˜สณ drop ฯ = drop (ฯƒ โˆ˜สณ ฯ)
keep ฯƒ โˆ˜สณ keep ฯ = keep (ฯƒ โˆ˜สณ ฯ)

If we fix a type then the family which sends a context to the variables in that context is actually a presheaf. Put less pretentiously, renamings act on variables:

ren-var : โˆ€ {ฮ“ ฮ” ฯ„} โ†’ Ren ฮ“ ฮ” โ†’ Var ฮ” ฯ„ โ†’ Var ฮ“ ฯ„
ren-var stop     v       = v
ren-var (drop ฯƒ) v       = pop (ren-var ฯƒ v)
ren-var (keep ฯƒ) stop    = stop
ren-var (keep ฯƒ) (pop v) = pop (ren-var ฯƒ v)

Finally, we can define an interpretation of renamings into our model CCC. Note that this interpretation lands in monomorphisms.

โŸฆ_โŸงสณ : Ren ฮ“ ฮ” โ†’ Hom โŸฆ ฮ“ โŸงแถœ โŸฆ ฮ” โŸงแถœ
โŸฆ stop   โŸงสณ = id
โŸฆ drop r โŸงสณ = โŸฆ r โŸงสณ โˆ˜ ฯ€โ‚
โŸฆ keep r โŸงสณ = โŸฆ r โŸงสณ โŠ—โ‚ id

Normals and neutrals๐Ÿ”—

To define evaluation, we need a type of normal forms: In our setting, these include lambda abstractions and pairs, along with morphisms of the base category. However, we are not working with evaluation, rather with normalisation, where reduction takes place in arbitrary contexts. Therefore, there are expressions that we can not give a value to, but for which no further normalisation can happen: for example, applying a variable. Therefore, we define mutually inductive types of normal forms and neutral forms.

data Nf : Cx โ†’ Ty โ†’ Type (o โŠ” โ„“)
data Ne : Cx โ†’ Ty โ†’ Type (o โŠ” โ„“)

A normal form is indeed one for which no more reduction is possible: lambda expressions and pairs. A neutral form is also normal. These come primarily from non-empty contexts. Neutral forms are, essentially, variables together with a stack of pending eliminations (applications or projections that will be reduced in the future). However, in our setting, we also consider the base terms as neutral at base types.

data Nf where
  lam  : Nf (ฮ“ , ฯ„) ฯƒ    โ†’ Nf ฮ“ (ฯ„ `โ‡’ ฯƒ)
  pair : Nf ฮ“ ฯ„ โ†’ Nf ฮ“ ฯƒ โ†’ Nf ฮ“ (ฯ„ `ร— ฯƒ)
  ne   : Ne ฮ“ ฯƒ โ†’ Nf ฮ“ ฯƒ

data Ne where
  var  : Var ฮ“ ฯ„ โ†’ Ne ฮ“ ฯ„
  app  : Ne ฮ“ (ฯ„ `โ‡’ ฯƒ) โ†’ Nf ฮ“ ฯ„ โ†’ Ne ฮ“ ฯƒ
  fstโ‚™ : Ne ฮ“ (ฯ„ `ร— ฯƒ) โ†’ Ne ฮ“ ฯ„
  sndโ‚™ : Ne ฮ“ (ฯ„ `ร— ฯƒ) โ†’ Ne ฮ“ ฯƒ
  hom  : โˆ€ {o} โ†’ Hom โŸฆ ฮ“ โŸงแถœ o โ†’ Ne ฮ“ (` o)

By a fairly obvious recursion, renamings act on neutrals and normals, thus making these, too, into presheaves.

ren-ne : โˆ€ {ฮ“ ฮ” ฯ„} โ†’ Ren ฮ” ฮ“ โ†’ Ne ฮ“ ฯ„ โ†’ Ne ฮ” ฯ„
ren-nf : โˆ€ {ฮ“ ฮ” ฯ„} โ†’ Ren ฮ” ฮ“ โ†’ Nf ฮ“ ฯ„ โ†’ Nf ฮ” ฯ„

This is the only case that requires attention: to rename a morphism of the base category, we must reify the renaming into its denotation, and compose with the morphism. The alternative here would be to keep a stack of pending renamings at each hom, which could then be optimised before composing at the end.

ren-ne ฯƒ (hom h)   = hom  (h โˆ˜ โŸฆ ฯƒ โŸงสณ)

Normals and neutrals also have a straightforward denotation given by the Cartesian closed structure.

โŸฆ_โŸงโ‚™  : Nf ฮ“ ฯ„ โ†’ Hom โŸฆ ฮ“ โŸงแถœ โŸฆ ฯ„ โŸงแต—
โŸฆ_โŸงโ‚›  : Ne ฮ“ ฯ„ โ†’ Hom โŸฆ ฮ“ โŸงแถœ โŸฆ ฯ„ โŸงแต—

โŸฆ lam h    โŸงโ‚™ = ฦ› โŸฆ h โŸงโ‚™
โŸฆ pair a b โŸงโ‚™ = โŸจ โŸฆ a โŸงโ‚™ , โŸฆ b โŸงโ‚™ โŸฉ
โŸฆ ne x     โŸงโ‚™ = โŸฆ x โŸงโ‚›

โŸฆ var x   โŸงโ‚› = โŸฆ x โŸงโฟ
โŸฆ app f x โŸงโ‚› = ev โˆ˜ โŸจ โŸฆ f โŸงโ‚› , โŸฆ x โŸงโ‚™ โŸฉ
โŸฆ fstโ‚™ h  โŸงโ‚› = ฯ€โ‚ โˆ˜ โŸฆ h โŸงโ‚›
โŸฆ sndโ‚™ h  โŸงโ‚› = ฯ€โ‚‚ โˆ˜ โŸฆ h โŸงโ‚›
โŸฆ hom h   โŸงโ‚› = h

We also have to prove a few hateful lemmas about how renamings, and its action on variables, neutrals and normals, interact with the denotation brackets. These lemmas essentially say that so that it doesnโ€™t matter whether we first pass to the semantics in or apply a renaming.

โŸฆโŸง-โˆ˜สณ   : (ฯ : Ren ฮ“ ฮ”) (ฯƒ : Ren ฮ” ฮ˜) โ†’ โŸฆ ฯ โˆ˜สณ ฯƒ โŸงสณ โ‰ก โŸฆ ฯƒ โŸงสณ โˆ˜ โŸฆ ฯ โŸงสณ

ren-โŸฆโŸงโฟ : (ฯ : Ren ฮ” ฮ“) (v : Var ฮ“ ฯ„) โ†’ โŸฆ ren-var ฯ v โŸงโฟ โ‰ก โŸฆ v โŸงโฟ โˆ˜ โŸฆ ฯ โŸงสณ
ren-โŸฆโŸงโ‚› : (ฯ : Ren ฮ” ฮ“) (t : Ne ฮ“ ฯ„)  โ†’ โŸฆ ren-ne ฯ t  โŸงโ‚› โ‰ก โŸฆ t โŸงโ‚› โˆ˜ โŸฆ ฯ โŸงสณ
ren-โŸฆโŸงโ‚™ : (ฯ : Ren ฮ” ฮ“) (t : Nf ฮ“ ฯ„)  โ†’ โŸฆ ren-nf ฯ t  โŸงโ‚™ โ‰ก โŸฆ t โŸงโ‚™ โˆ˜ โŸฆ ฯ โŸงสณ
If you want, you can choose to read the proofs of these substitution correctness lemmas by clicking on this <details> tag.
โŸฆโŸง-โˆ˜สณ stop ฯƒ = intror refl
โŸฆโŸง-โˆ˜สณ (drop ฯ) ฯƒ = pushl (โŸฆโŸง-โˆ˜สณ ฯ ฯƒ)
โŸฆโŸง-โˆ˜สณ (keep ฯ) stop = introl refl
โŸฆโŸง-โˆ˜สณ (keep ฯ) (drop ฯƒ) = pushl (โŸฆโŸง-โˆ˜สณ ฯ ฯƒ) โˆ™ sym (pullr ฯ€โ‚โˆ˜โŸจโŸฉ)
โŸฆโŸง-โˆ˜สณ (keep ฯ) (keep ฯƒ) = sym $ Product.unique (fp _ _) _
  (pulll ฯ€โ‚โˆ˜โŸจโŸฉ โˆ™ pullr ฯ€โ‚โˆ˜โŸจโŸฉ โˆ™ pulll (sym (โŸฆโŸง-โˆ˜สณ ฯ ฯƒ)))
  (pulll ฯ€โ‚‚โˆ˜โŸจโŸฉ โˆ™ pullr ฯ€โ‚‚โˆ˜โŸจโŸฉ โˆ™ idl _)

ren-โŸฆโŸงโฟ stop v           = intror refl
ren-โŸฆโŸงโฟ (drop ฯ) v       = pushl (ren-โŸฆโŸงโฟ ฯ v)
ren-โŸฆโŸงโฟ (keep ฯ) stop    = sym (ฯ€โ‚‚โˆ˜โŸจโŸฉ โˆ™ idl _)
ren-โŸฆโŸงโฟ (keep ฯ) (pop v) = pushl (ren-โŸฆโŸงโฟ ฯ v) โˆ™ sym (pullr ฯ€โ‚โˆ˜โŸจโŸฉ)

ren-โŸฆโŸงโ‚› ฯ (var x) = ren-โŸฆโŸงโฟ ฯ x
ren-โŸฆโŸงโ‚› ฯ (app f x) = apโ‚‚ _โˆ˜_ refl
  (apโ‚‚ โŸจ_,_โŸฉ (ren-โŸฆโŸงโ‚› ฯ f) (ren-โŸฆโŸงโ‚™ ฯ x) โˆ™ sym (โŸจโŸฉโˆ˜ _))
  โˆ™ pulll refl
ren-โŸฆโŸงโ‚› ฯ (fstโ‚™ t) = pushr (ren-โŸฆโŸงโ‚› ฯ t)
ren-โŸฆโŸงโ‚› ฯ (sndโ‚™ t) = pushr (ren-โŸฆโŸงโ‚› ฯ t)
ren-โŸฆโŸงโ‚› ฯ (hom x) = refl

ren-โŸฆโŸงโ‚™ ฯ (lam t) =
    ap ฦ› (ren-โŸฆโŸงโ‚™ (keep ฯ) t)
  โˆ™ sym (unique _ (apโ‚‚ _โˆ˜_ refl remโ‚ โˆ™ pulll (commutes โŸฆ t โŸงโ‚™)))
  remโ‚ : (โŸฆ lam t โŸงโ‚™ โˆ˜ โŸฆ ฯ โŸงสณ) โŠ—โ‚ id โ‰ก (โŸฆ lam t โŸงโ‚™ โŠ—โ‚ id) โˆ˜ โŸฆ ฯ โŸงสณ โŠ—โ‚ id
  remโ‚ = Bifunctor.firstโˆ˜first ร—-functor

ren-โŸฆโŸงโ‚™ ฯ (pair a b) = apโ‚‚ โŸจ_,_โŸฉ (ren-โŸฆโŸงโ‚™ ฯ a) (ren-โŸฆโŸงโ‚™ ฯ b) โˆ™ sym (โŸจโŸฉโˆ˜ _)
ren-โŸฆโŸงโ‚™ ฯ (ne x) = ren-โŸฆโŸงโ‚› ฯ x


We would like to write a map of type Expr ฮ“ ฯ„ โ†’ Nf ฮ“ ฯ„. However, by design, this is not straightforward: the type of normal forms isโ€ฆ 2 However, note that, since both Nf and Ne are โ€œpresheavesโ€ on the โ€œcategory of renamingsโ€, we can use the Cartesian closed structure of presheaves to interpret the lambda calculus. The idea here is that presheaves, being functors into have a computational structure on the relevant connectives that closely matches that of itself: for example, composing the first projection with a pairing, in the category of presheaves, is (componentwise) definitionally equal to the first component of the pair. Itโ€™s a boosted up version of exactly the same idea used for the category solver.

Then, as long as we can reify these presheaves back to normal forms, we have a normalisation procedure! Expressions are interpreted as sections of the relevant presheaves, then reified into normal forms. And, to be clear, we only need to reflect the presheaves that actually represent types: these can be built by recursion (on the type!) so that they are very easy to reify.

However, that still leaves the question of correctness for the NbE algorithm. Given an expression we will have two wildly different approaches to interpreting as a morphism Thereโ€™s the naรฏve denotation โŸฆ_โŸงแต‰, which interprets an expression directly using the relevant connections; But now we can also interpret an expression into a section then reify that to a normal form and take the denotation Normalisation should compute a form, and is validated by CCCs, so and should be the same. How do we ensure this?

It would be totally possible to do this in two passes - first define the algorithm, then prove it correct. But the proof of correctness would mirror the structure of the algorithm almost 1:1! Can we define the algorithm in a way that is forced into correctness? It turns out that we can! The idea here is an adaptation of the gluing method in the semantics of type theory. Rather than have a mere presheaf to represent the semantic values in our full construction Tyแต– has three arguments: The type the context (over which it is functorial), and a denotation โ€” and in prose, weโ€™ll write Tyแต– as we say that tracks when

Since all our operations on semantic values will be written against a type indexed by their denotations, the core of the algorithm will have to be written in a way that evidently preserves denotations โ€” the type checker is doing most of the work. Our only actual correctness theorem boils down to showing that, given we have in

To summarize all the parts, we have:

  • Expressions โ€” the user writes these, and they may have redices.

  • Denotations Since a CCC has โ€œstructuralโ€ morphisms corresponding to each kind of expression, we can directly read off a morphism from an expression.

  • Neutrals and normals A neutral is something that wants to reduce but canโ€™t (e.g.ย a projection applied to a variable), and a normal is something that definitely wonโ€™t reduce anymore (e.g.ย a lambda expression). Normals and neutrals also have denotations, so we may also write when or

  • Semantic values, The presheaf is computed by recursion on so that its sections have a good computational representation. As mentioned above, itโ€™s indexed by a denotation forcing the core of the algorithm to preserve denotations.

  • The reification and reflection transformations which turns a semantic value into a normal form, and which witnesses that the semantic values include the neutrals.

Our main objective is a normalisation function that maps expressions to semantic values Letโ€™s get started.

\ Warning

While we have been talking about presheaves above, the actual code does not actually set up a presheaf category to work in. The reason for this is parsimony. Referring to presheaves for the motivation, but working with simpler type families, lends itself better to formalisation; many of the details, e.g.ย functoriality of are not used, and would simply be noise.

Semantic values๐Ÿ”—

Tyแต– : (ฯ„ : Ty) (ฮ“ : Cx) โ†’ Hom โŸฆ ฮ“ โŸงแถœ โŸฆ ฯ„ โŸงแต— โ†’ Type (o โŠ” โ„“)

We define by recursion on and its definition is mostly unsurprising: at each case, we use the Cartesian closed structure of presheaf categories to interpret the given type into a presheaf that has the right universal property, but is โ€œdefinitionally nicerโ€. Letโ€™s go through it case-by-case. When faced with a product type in the object language, we can simply return a meta-language product type. However, we must also preserve the tracking information: if a section of a product type is to track what should each component track? Well, we know that by the uniqueness property of Cartesian products. So the first component should track and the second

Tyแต– (ฯ„ `ร— ฯƒ) ฮ“ h = Tyแต– ฯ„ ฮ“ (ฯ€โ‚ โˆ˜ h) ร— Tyแต– ฯƒ ฮ“ (ฯ€โ‚‚ โˆ˜ h)

For a function type, we once again appeal to the construction in presheaves. The components of the exponential are defined to be the natural transformations which, at the component, are given by maps A function value must preserve tracking information: A function which tracks if given an argument tracking it must return a value which tracks the application of to relative to the renaming In a CCC, thatโ€™s given by

which is precisely what we require.

Tyแต– (ฯ„ `โ‡’ ฯƒ) ฮ“ h =
  โˆ€ {ฮ”} (ฯ : Ren ฮ” ฮ“) {a}
  โ†’ Tyแต– ฯ„ ฮ” a
  โ†’ Tyแต– ฯƒ ฮ” (ev โˆ˜ โŸจ h โˆ˜ โŸฆ ฯ โŸงสณ , a โŸฉ)

Finally, we have the case of base types, for which the corresponding presheaf is that of neutral forms. Here, we can finally discharge the tracking information: a neutral tracks iff.

Tyแต– (` x)    ฮ“ h = ฮฃ (Ne ฮ“ (` x)) ฮป n โ†’ โŸฆ n โŸงโ‚› โ‰ก h

To work on open contexts, we can define (now by induction), the presheaf of parallel substitutions, which are decorated sequences of terms. These also have a morphism of attached, but keep in mind that a parallel substitution interprets as an element of hence that is what they are indexed over.

data Subแต– : โˆ€ ฮ“ ฮ” โ†’ Hom โŸฆ ฮ” โŸงแถœ โŸฆ ฮ“ โŸงแถœ โ†’ Type (o โŠ” โ„“) where
  โˆ…   : โˆ€ {i} โ†’ Subแต– โˆ… ฮ” i
  _,_ : โˆ€ {h} โ†’ Subแต– ฮ“ ฮ” (ฯ€โ‚ โˆ˜ h) โ†’ Tyแต– ฯƒ ฮ” (ฯ€โ‚‚ โˆ˜ h) โ†’ Subแต– (ฮ“ , ฯƒ) ฮ” h

As always, we must show that these have an action by renamings. Renamings act on the semantic component, too: if tracks then tracks

ren-tyแต–  : โˆ€ {ฮ” ฮ“ ฯ„ m} (ฯ : Ren ฮ” ฮ“) โ†’ Tyแต– ฯ„ ฮ“ m  โ†’ Tyแต–  ฯ„ ฮ” (m โˆ˜ โŸฆ ฯ โŸงสณ)
ren-subแต– : โˆ€ {ฮ” ฮ“ ฮ˜ m} (ฯ : Ren ฮ˜ ฮ”) โ†’ Subแต– ฮ“ ฮ” m โ†’ Subแต– ฮ“ ฮ˜ (m โˆ˜ โŸฆ ฯ โŸงสณ)

Reification and reflection๐Ÿ”—

We can now define the reification and reflection functions. Reflection embeds a neutral form into semantic values; Reification turns semantic values into normal forms. Since we have defined the semantic values by recursion, we can exploit the good computational behaviour of Agda types in our reification/reflection functions: for example, when reifying at a product type, we know that we have an honest-to-god product of semantic values at hand.

reifyแต–         : โˆ€ {h}                 โ†’ Tyแต– ฯ„ ฮ“ h โ†’ Nf ฮ“ ฯ„
reflectแต–       : (n : Ne ฮ“ ฯ„)          โ†’ Tyแต– ฯ„ ฮ“ โŸฆ n โŸงโ‚›
reifyแต–-correct : โˆ€ {h} (v : Tyแต– ฯ„ ฮ“ h) โ†’ โŸฆ reifyแต– v โŸงโ‚™ โ‰ก h

reifyแต– {ฯ„ = ฯ„ `ร— s} (a , b) = pair (reifyแต– a) (reifyแต– b)
reifyแต– {ฯ„ = ฯ„ `โ‡’ s} f       = lam (reifyแต– (f (drop stop) (reflectแต– (var stop))))
reifyแต– {ฯ„ = ` x} d          = ne (d .fst)

reflectแต– {ฯ„ = ฯ„ `ร— ฯƒ} n     = reflectแต– (fstโ‚™ n) , reflectแต– (sndโ‚™ n)
reflectแต– {ฯ„ = ฯ„ `โ‡’ ฯƒ} n ฯ a = tyแต–โŸจ apโ‚‚ (ฮป e f โ†’ ev โˆ˜ โŸจ e , f โŸฉ) (ren-โŸฆโŸงโ‚› ฯ n) (reifyแต–-correct a) โŸฉtyแต–
  (reflectแต– (app (ren-ne ฯ n) (reifyแต– a)))
reflectแต– {ฯ„ = ` x}    n     = n , refl

The interesting cases deal with function types: To reify a lambda โ€” which is semantically represented by a function that operates on (a renaming and) the actual argument โ€” we produce a lam constructor, but we must then somehow reify โ€œall possible bodiesโ€.

However, since the semantic value of a function takes arguments and returns results in an arbitrary extension of the given context, we can introduce a new variable โ€” thus a new neutral โ€” and apply the body to that. Evaluation keeps going, but anything that actually depends on the body will be blocked on this new neutral!

Conversely, reflection starts from a neutral, and must build a semantic value that captures all the pending applications. At the case of a lambda, we have a neutral a renaming and an argument We can thus build the stuck application

This is also where we encounter the only correctness lemma that is not forced on us by the types involved, since the type of normal forms is not indexed by a denotation in We must write an external function reifyแต–-correct, actually establishing that when tracks

reifyแต–-correct {ฯ„ = ฯ„ `ร— ฯƒ} (a , b) = sym $
  Product.unique (fp _ _) _ (sym (reifyแต–-correct a)) (sym (reifyแต–-correct b))
reifyแต–-correct {ฯ„ = ฯ„ `โ‡’ ฯƒ} {h = h} ฮฝ =
    p : โŸฆ reifyแต– (ฮฝ (drop stop) (reflectแต– (var stop))) โŸงโ‚™ โ‰ก ev โˆ˜ โŸจ h โˆ˜ id โˆ˜ ฯ€โ‚ , ฯ€โ‚‚ โŸฉ
    p = reifyแต–-correct (ฮฝ (drop stop) (reflectแต– (var stop)))
  in ap ฦ› p
   โˆ™ sym (unique _ (apโ‚‚ _โˆ˜_ refl (apโ‚‚ โŸจ_,_โŸฉ (sym (pulll (elimr refl))) (eliml refl))))
reifyแต–-correct {ฯ„ = ` x} d = d .snd

Interpreting expressions๐Ÿ”—

With our semantic values carefully chosen to allow reflection and reification, we can set out to build an Expr-algebra. To work in open contexts, an expression will be interpreted as a natural transformation from parallel substitutions to types: the parallel substitution acts as our โ€œenvironmentโ€, so is used in the interpretation of variables:

varแต– : โˆ€ {ฯ} (ฯ€ : Var ฮ” ฯ„) โ†’ Subแต– ฮ” ฮ“ ฯ โ†’ Tyแต– ฯ„ ฮ“ (โŸฆ ฯ€ โŸงโฟ โˆ˜ ฯ)
varแต– stop    (_ , x) = x
varแต– (pop v) (c , _) = tyแต–โŸจ assoc _ _ _ โŸฉtyแต– (varแต– v c)

We must interpret morphisms from the model category in a type-directed way, and eta-expand as we go. Thatโ€™s because we made the decision to only have morphisms as neutrals at base type. Therefore, if a morphism from the base category lands in (e.g.) products, we must interpret it as the semantic product of its projections:

baseแต– : โˆ€ {h'} (h : Hom โŸฆ ฮ” โŸงแถœ โŸฆ ฯ„ โŸงแต—) โ†’ Subแต– ฮ” ฮ“ h' โ†’ Tyแต– ฯ„ ฮ“ (h โˆ˜ h')

baseแต– {ฯ„ = ฯ„ `ร— ฯ„โ‚} x c     =
    tyแต–โŸจ sym (assoc _ _ _) โŸฉtyแต– (baseแต– (ฯ€โ‚ โˆ˜ x) c)
  , tyแต–โŸจ sym (assoc _ _ _) โŸฉtyแต– (baseแต– (ฯ€โ‚‚ โˆ˜ x) c)

baseแต– {ฯ„ = ฯ„ `โ‡’ ฯƒ} {h' = h'} h c ฯ {ฮฑ} a = tyแต–โŸจ pullr (Product.unique (fp _ _) _ (pulll ฯ€โ‚โˆ˜โŸจโŸฉ โˆ™ extendr ฯ€โ‚โˆ˜โŸจโŸฉ) (pulll ฯ€โ‚‚โˆ˜โŸจโŸฉ โˆ™ ฯ€โ‚‚โˆ˜โŸจโŸฉ)) โŸฉtyแต–
  (baseแต– (ev โˆ˜ โŸจ h โˆ˜ ฯ€โ‚ , ฯ€โ‚‚ โŸฉ) (
    subแต–โŸจ sym ฯ€โ‚โˆ˜โŸจโŸฉ โŸฉsubแต– (ren-subแต– ฯ c), tyแต–โŸจ sym ฯ€โ‚‚โˆ˜โŸจโŸฉ โŸฉtyแต– a))

baseแต– {ฯ„ = ` t} x c = hom (x โˆ˜ โŸฆ c โŸงหข) , ap (x โˆ˜_) (โŸฆโŸงหข-correct c)

Those are the hard bits, we can now interpret everything else by a simple recursion! Note that, when interpreting a lambda expression, we return a function which evaluates the body, and when eliminating it, we apply it to the value of its argument3.

exprแต– : โˆ€ {h} (e : Expr ฮ” ฯ„) (ฯ : Subแต– ฮ” ฮ“ h) โ†’ Tyแต– ฯ„ ฮ“ (โŸฆ e โŸงแต‰ โˆ˜ h)
exprแต– (`var x)   c = varแต– x c
exprแต– (`ฯ€โ‚ p)    c = tyแต–โŸจ assoc _ _ _ โŸฉtyแต– (exprแต– p c .fst)
exprแต– (`ฯ€โ‚‚ p)    c = tyแต–โŸจ assoc _ _ _ โŸฉtyแต– (exprแต– p c .snd)
exprแต– `โŸจ a , b โŸฉ c =
  tyแต–โŸจ sym (pulll ฯ€โ‚โˆ˜โŸจโŸฉ) โŸฉtyแต– (exprแต– a c) , tyแต–โŸจ sym (pulll ฯ€โ‚‚โˆ˜โŸจโŸฉ) โŸฉtyแต– (exprแต– b c)
exprแต– {h = h} (`$ f a) c = tyแต–โŸจ ap (ev โˆ˜_) (apโ‚‚ โŸจ_,_โŸฉ (idr _) refl โˆ™ sym (โŸจโŸฉโˆ˜ h)) โˆ™ assoc _ _ _ โŸฉtyแต–
  (exprแต– f c stop (exprแต– a c))
exprแต– (` x)      c = baseแต– x c
exprแต– {h = h} (`ฮป f) ฯ ฯƒ {m} a = tyแต–โŸจ fixup โŸฉtyแต– (exprแต– f
  ( subแต–โŸจ sym ฯ€โ‚โˆ˜โŸจโŸฉ โŸฉsubแต– (ren-subแต– ฯƒ ฯ)
  , tyแต–โŸจ sym ฯ€โ‚‚โˆ˜โŸจโŸฉ โŸฉtyแต–  a ))

If we apply the semantic value of an expression to the โ€œidentity parallel substitutionโ€, a context where all the variables are given a neutral value, we get a normal form!

id-subแต– : โˆ€ ฮ“ โ†’ Subแต– ฮ“ ฮ“ id
id-subแต– โˆ…     = โˆ…
id-subแต– (ฮ“ , x) =
    subแต–โŸจ idl _ ยทยท idl _ ยทยท sym (idr _) โŸฉsubแต– (ren-subแต– (drop stop) (id-subแต– ฮ“))
  , tyแต–โŸจ sym (idr _) โŸฉtyแต–  (reflectแต– (var stop))

nf : Expr ฮ“ ฯ„ โ†’ Nf ฮ“ ฯ„
nf x = reifyแต– (exprแต– x (id-subแต– _))

Moreover, we can appeal to our key correctness theorem to conclude the correctness of the entire normalisation procedure. Thatโ€™s the only explicit theorem we proved, with the rest of the pieces being threaded through the definitions of the various transformations.

  nf-sound : (e : Expr ฮ“ ฯ„) โ†’ โŸฆ nf e โŸงโ‚™ โ‰ก โŸฆ e โŸงแต‰
  nf-sound {ฮ“ = ฮ“} e = reifyแต–-correct (exprแต– e (id-subแต– ฮ“)) โˆ™ elimr refl

As a demonstration, we can normalise the expression

which lets Agda reduce it away to be simply the variable (which is the second in the context). Moreover, by appeal to the correctness theorem, we can prove that the complicated morphism that denotes is equal to the much simpler

module _ {a b : Ob} where private
  e1 : Expr ((โˆ… , ` a) , ` b) _
  e1 = `ฯ€โ‚ `โŸจ `$ (`ฮป (`var stop)) (`var (pop stop)) , `var stop โŸฉ

  _ : nf e1 โ‰ก ne (var (pop stop))
  _ = refl

  _ : ฯ€โ‚‚ โˆ˜ ฯ€โ‚ โ‰ก ฯ€โ‚ โˆ˜ โŸจ ev โˆ˜ โŸจ ฦ› ฯ€โ‚‚ , ฯ€โ‚‚ โˆ˜ ฯ€โ‚ โŸฉ , ฯ€โ‚‚ โŸฉ
  _ = nf-sound e1
  -- An attempt to normalise this proof produced 4 MiB of garbage, and
  -- ran for over an hour before our patience ran out.

An application๐Ÿ”—

The normalisation algorithm serves to decide the semantic equality of expressions in the simply-typed lambda calculus, but Iโ€™ll freely admit thatโ€™s not a task that comes up every day. We can also use this algorithm to prove things about the simply-typed lambda calculus! As an example, we have canonicity: every term in a base type denotes an actual element of the base type. In our categorical setting, that means that, given where is one of the non-pair, non-function types we have included from the category then there is a global element which denotes.

canonicity : โˆ€ {a} โ†’ (e : Expr โˆ… (` a)) โ†’ ฮฃ (Hom ( term) a) ฮป h โ†’ โŸฆ e โŸงแต‰ โ‰ก h
canonicity {a = a} e = go (nf e) (nf-sound e) where
  no-functions : โˆ€ {a b} โ†’ Ne โˆ… (a `โ‡’ b) โ†’ โŠฅ
  no-pairs     : โˆ€ {a b} โ†’ Ne โˆ… (a `ร— b) โ†’ โŠฅ

  no-functions (app f _) = no-functions f
  no-functions (fstโ‚™ x)  = no-pairs x
  no-functions (sndโ‚™ x)  = no-pairs x

  no-pairs (app f _) = no-functions f
  no-pairs (fstโ‚™ x)  = no-pairs x
  no-pairs (sndโ‚™ x)  = no-pairs x

  go : (nf : Nf โˆ… (` a)) โ†’ โŸฆ nf โŸงโ‚™ โ‰ก โŸฆ e โŸงแต‰ โ†’ ฮฃ (Hom ( term) a) ฮป h โ†’ โŸฆ e โŸงแต‰ โ‰ก h
  go (ne (app f _)) p = absurd (no-functions f)
  go (ne (fstโ‚™ x)) p  = absurd (no-pairs x)
  go (ne (sndโ‚™ x)) p  = absurd (no-pairs x)
  go (ne (hom x)) p   = x , sym p

  1. since contexts are built by extension on the rightโ†ฉ๏ธŽ

  2. It is not, however, โ†ฉ๏ธŽ

  3. and the identity renaming, since our argument lives in the same contextโ†ฉ๏ธŽ