Contents Type checking Category theory

Guilhem Moulin

Description

Contents Type checking Category theory Category theory to the rescue of type checking Guilhem Moulin February 15, 2010

• list ty


• category theory


• tm ?


• typing rules


• ty


• calculus dependent


• simply typed


• typed ?-calculus

Sujets

• Moulin
• Category theory

Informations

• Publié par: pefav
• Nombre de lectures: 17
• Langue: English

Extrait

Contents Type checking Category theory
Category theory to the rescue of type checking
Guilhem Moulin
February 15, 2010Contents Type checking Category theory
Type checking
Simply typed λ-calculus
Dependent typed λ-calculus
Category theoryContents Type checking Category theory
Simply typed λ-calculus: types and terms
1 data Ty : Set where
2 ⋆ : Ty
3 ⇒ : Ty → Ty → Ty
5 Cxt : Set
6 Cxt = List Ty
8 data Tm : Set where
9 Var : Nat → Tm
10 @ : Tm → Tm → Tm
11 λ : Tm → TmContents Type checking Category theory
Simply typed λ-calculus: typing rules
Γ⊢ a⇒ b Γ⊢ a
Γ ,...,Γ ⊢ Γ Γ⊢ b1 n i
Γ,a⊢ b
Γ⊢ a⇒ bContents Type checking Category theory
Simply typed λ-calculus: typing rules
f : Γ⊢ a⇒ b x : Γ⊢ a
Var i : Γ ,...,Γ ⊢ Γ f @ x : Γ⊢ b1 n i
e : Γ,a⊢ b
λe : Γ⊢ a⇒ bContents Type checking Category theory
Simply typed λ-calculus: typing rules
f : Γ⊢ a⇒ b x : Γ⊢ a
Var i : Γ ,...,Γ ⊢ Γ f @ x : Γ⊢ b1 n i
e : Γ,a⊢ b
λe : Γ⊢ a⇒ b
"_: _ ⊢ _": Cxt → Tm → Ty → Prop
yContents Type checking Category theory
Simply typed λ-calculus: type-checking algorithm
Decidability of typing:
1 decTS : (Γ: Cxt) → (a: Ty) → (t: Tm)
2 → (t: Γ ⊢ a) ∨ Not (t: Γ ⊢ a)Contents Type checking Category theory
Simply typed λ-calculus: type-checking algorithm
Decidability of typing:
1 decTS : (Γ: Cxt) → (a: Ty) → (t: Tm)
2 → (t: Γ ⊢ a) ∨ Not (t: Γ ⊢ a)
Perform program extraction:
1 isTm : Cxt → Ty → Tm → BoolContents Type checking Category theory
Simply typed λ-calculus: type-checking algorithm
Decidability of typing:
1 decTS : (Γ: Cxt) → (a: Ty) → (t: Tm)
2 → (t: Γ ⊢ a) ∨ Not (t: Γ ⊢ a)
Perform program extraction:
1 isTm : Cxt → Ty → Tm → Bool
Correctness of type-checking:
1 corrTC : (Γ: Cxt) → (a: Ty) → (t: Tm)
2 → t: Γ ⊢ a ↔ isTm Γ a t = trueContents Type checking Category theory
What is dependent typed λ-calculus?
• dependent function types: (x : A)⇒ B(x) rather than A⇒ B
• universe Set of“sets”(small types)