25 Pages
English
Gain access to the library to view online
Learn more

Contents Type checking Category theory

-

Gain access to the library to view online
Learn more
25 Pages
English

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


Subjects

Informations

Published by
Reads 17
Language English

Exrait

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)