Cartesian Closed Categories for STLC

Stream: mathlib4

[Tanner Duve]

Hey, hoping someone could take a look at the error I'm getting.

I've done a complete formalization of the simply typed lambda calculus, with a proof of type soundness. As my next step I wanted to attempt the formalization of cartesian closed categories as a model of the STLC. I've started as follows:

Here is the syntax:

--Syntax
-- Types - base type is booleans, then we add arrow and product types
inductive ty : Type
  | Ty_Bool : ty
  | Ty_Arrow : ty -> ty -> ty
  | Ty_Prod : ty -> ty -> ty

-- Terms - variables, applications, abstractions, pairs, projections, true/false
inductive tm : Type
  | tm_var : String -> tm
  | tm_app : tm -> tm -> tm
  | tm_abs : String -> ty -> tm -> tm
  | tm_pair : tm -> tm -> tm
  | tm_proj1 : tm -> tm
  | tm_proj2 : tm -> tm
  | tm_true : tm
  | tm_false : tm

-- Custom notation
notation "<{" e:99 "}>" => e
notation S:50 " -> " T:50 => ty.Ty_Arrow S T
notation S:50 " × " T:50 => ty.Ty_Prod S T
notation "λ" x " : " t ", " y => tm.tm_abs x t y
notation " Bool " => ty.Ty_Bool
notation " true " => tm.tm_true
notation " false " => tm.tm_false
notation "⟨" t ", " t' "⟩" => tm.tm_pair t t'
notation "π₁ " u => tm.tm_proj1 u
notation "π₂ " u => tm.tm_proj2 u
infixl:99 " ∘ " => tm.tm_app

And here is my start to defining the categorical semantics:

--- Rough first sketch to start setting up categories, following Abramsky.

import LambdaCalc.syntax
import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Closed.Cartesian
import Mathlib.CategoryTheory.Products.Basic
import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

open CategoryTheory
open CategoryTheory.Closed

variable (C : Type) [Category C] [Limits.HasFiniteProducts C] [CartesianClosed C] -- C is a CCC

variable (B : C) -- B is an object in C

-- Semantic assignment for types
noncomputable def semantic_translation_ty (T : ty) : C :=
match T with
  | ty.Ty_Bool => B -- Booleans assigned to object B
  | ty.Ty_Arrow T₁ T₂ => (semantic_translation_ty T₁) ⟹ (semantic_translation_ty T₂) -- Arrow types assigned to exponentials
  | ty.Ty_Prod T₁ T₂ => Limits.prod (semantic_translation_ty T₁) (semantic_translation_ty T₂) -- Product types assigned to binary products

-- Typing contexts are lists of String, Type pairs
def context := List (String × ty)

-- Adding assignment to context
def update (Γ : context) (x : String) (T: ty) :=
  (x, T) :: Γ

notation x " ↦ " v " ; " m => update m x v

-- Semantic assignment for contexts, empty context gets assigned the terminal object and non empty contexts get assigned to binary products recursively

noncomputable def semantic_translation_ctx (Γ : context) : C :=
match Γ with
  | [] => Limits.terminal C
  | hd :: tl => Limits.prod (semantic_translation_ty hd.2) (semantic_translation_ctx tl)
-- not understanding this error, semantic_translation_ty is defined to take an element of type Ty,
-- but this error complains that I've given it an element of type Ty while it is expecting Type : Type 1.
-- Why is Lean expecting this?

In my function semantic_translation_ctx, in the recursive case, the argument "hd.2" to the call to semantic_translation_ty gives the error:
"application type mismatch
@semantic_translation_ty hd.2
argument
hd.2
has type
ty : Type
but is expected to have type
Type : Type 1"

It seems as though everything should type check. A context is of type List( String x Ty) (where Ty is the type of types in my STLC). Thus hd.2 has type Ty. Further, semantic_translation_ty is defined to take an input of element Ty, and outputs an object of C. So when I call semantic_translation_ty hd.2, I'm not sure why it would expect a different type.

[Alex J. Best]

The lines variable (C : Type) and (B : C) mean that semantic_translation_ty takes explicit C and B arguments, (try #check semantic_translation_ty) . You probably want semantic_translation_ty C B hd.2 I guess?

[Tanner Duve]

Thanks for your reply! I've defined semantic_translation_ty to take an element of type ty, and return an object in C. It doesn't take C and B as arguments.

[Alex J. Best]

Well how does the function know which C it will land in if that isn't provided as an argument? They are arguments of the function defined in your code I assure you

[Tanner Duve]

Ah, I see what you're saying, C B hd.2 did the trick. Thank you!