Syntax and semantics of dependent types. - Cours MPRI catégories et lambda-calcul.

Description

Syntaxandsemanticsofdependenttypes.AntoineDelignat-LavaudSyntax and semantics of dependenttypes.Cours MPRI catégories et lambda-calcul.Outline15 février 2010 Dependent typesSome motivationsThe type systemDependent functionNatural numbersDependent sumIdentity typesUniversesCategory-theoreticsemanticsContext morphismsCategories with familiesInterpretationAntoine Delignat-LavaudÉcole Normale Supérieure de Cachan1SyntaxandOutline semanticsofdependenttypes.AntoineDelignat-Lavaud1 DependenttypesSome motivationsThe type systemOutlineDependent functionDependent typesSome motivationsNatural numbersThe type system sum Dependent functionNatural numbersIdentity types Dependent sumIdentity typesUniversesUniversesCategory-theoreticsemanticsContext morphisms2 Category-theoreticsemantics Categories with familiesInterpretationContext morphismsCategories with familiesInterpretation2Syntaxandsemanticsofdependenttypes.AntoineDelignat-LavaudDependenttypes1 Types that depend on or vary with values.2 Example : Vec (M), type of vectors of length M OutlineDependent types3 M is a value in the calculusSome motivationsThe type system4 The dependancy is written x : N:Vec (x)Dependent functionNatural numbers5 Benefits : types are more accurate (e.g. N! List(N))Dependent sumIdentity types6 More expressive static verification :UniversesH : x : N:Vec (Suc(x))! Category-theoreticsemanticsContext morphisms7 Programs on length ...

Subjects

• Documents
• Savoirs
• Formal sciences

Informations

• Published by: Thaub
• Reads: 29
• Language: English

Exrait

Syntax and semantics of dependent types. Cours MPRI catégories et lambda-calcul.

15 février 2010

Antoine Delignat-Lavaud École Normale Supérieure de Cachan

Syntax and semantics of dependent types. Antoine Delignat-Lavaud

Outline Dependent types Some motivations The type system Dependent function Natural numbers Dependent sum Identity types Universes Category-theoretic semantics Context morphisms Categories with families Interpretation

1

Outline

1

2

Dependent types Some motivations The type system Dependent function Natural numbers Dependent sum Identity types Universes

Category-theoretic semantics Context morphisms Categories with families Interpretation

Syntax and semantics of dependent types.

Antoine Delignat-Lavaud

Outline Dependent types Some motivations The type system Dependent function Natural numbers Dependent sum Identity types Universes

Category-theoretic semantics Context morphisms Categories with families Interpretation

2

Dependent types

1 Types that depend on or vary withvalues. 2 Example :Vec τ (M), type of vectors of lengthM 3 M is a value in the calculus 4 The dependancy is writtenΠx:N.Vec τ (x) 5 Benefits : types are more accurate (e.g.N→List(N)) 6 More expressive static verification : H: Πx:N.Vec τ (Suc(x))→τ 7 Programs on length dependent vectors must satisfy length constraints to type. 8 Another example : ordered vectors

Syntax and semantics of dependent types.

Antoine Delignat-Lavaud

Outline Dependent types Some motivations The type system Dependent function Natural numbers Dependent sum Identity types Universes Category-theoretic semantics Context morphisms Categories with families Interpretation

3

Dependent types

1 Types that depend on or vary withvalues. 2 Example :Vec τ (M), type of vectors of lengthM 3 M is a value in the calculus 4 The dependancy is writtenΠx:N.Vec τ (x) 5 Benefits : types are more accurate (e.g.N→List(N)) 6 More expressive static verification : H: Πx:N.Vec τ (Suc(x))→τ 7 on length dependent vectors must satisfy lengthPrograms constraints to type. 8 Another example : ordered vectors

Syntax and semantics of dependent types.

Antoine Delignat-Lavaud

Outline Dependent types Some motivations The type system Dependent function Natural numbers Dependent sum Identity types Universes Category-theoretic semantics Context morphisms Categories with families Interpretation

3

Dependent types

1 Types that depend on or vary withvalues. 2 Example :Vec τ (M), type of vectors of lengthM 3 M is a value in the calculus 4 The dependancy is writtenΠx:N.Vec τ (x) 5 Benefits : types are more accurate (e.g.N→List(N)) 6 More expressive static verification : H: Πx:N.Vec τ (Suc(x))→τ 7 on length dependent vectors must satisfy lengthPrograms constraints to type. 8 Another example : ordered vectors

Syntax and semantics of dependent types.

Antoine Delignat-Lavaud

Outline Dependent types Some motivations The type system Dependent function Natural numbers Dependent sum Identity types Universes Category-theoretic semantics Context morphisms Categories with families Interpretation

3

Dependent types

1 Types that depend on or vary withvalues. 2 Example :Vec τ (M), type of vectors of lengthM 3 M is a value in the calculus 4 The dependancy is writtenΠx:N.Vec τ (x) 5 Benefits : types are more accurate (e.g.N→List(N)) 6 More expressive static verification : H: Πx:N.Vec τ (Suc(x))→τ 7 on length dependent vectors must satisfy lengthPrograms constraints to type. 8 Another example : ordered vectors

Syntax and semantics of dependent types.

Antoine Delignat-Lavaud

Outline Dependent types Some motivations The type system Dependent function Natural numbers Dependent sum Identity types Universes Category-theoretic semantics Context morphisms Categories with families Interpretation

3

Dependent types

1 Types that depend on or vary withvalues. 2 Example :Vec τ (M), type of vectors of lengthM 3 M is a value in the calculus 4 The dependancy is writtenΠx:N.Vec τ (x) 5 Benefits : types are more accurate (e.g.N→List(N)) 6 More expressive static verification : H: Πx:N.Vec τ (Suc(x))→τ 7 on length dependent vectors must satisfy lengthPrograms constraints to type. 8 Another example : ordered vectors

Syntax and semantics of dependent types.

Antoine Delignat-Lavaud

Outline Dependent types Some motivations The type system Dependent function Natural numbers Dependent sum Identity types Universes Category-theoretic semantics Context morphisms Categories with families Interpretation

3

Dependent types

1 Types that depend on or vary withvalues. 2 Example :Vec τ (M), type of vectors of lengthM 3 M is a value in the calculus 4 The dependancy is writtenΠx:N.Vec τ (x) 5 Benefits : types are more accurate (e.g.N→List(N)) 6 More expressive static verification : H: Πx:N.Vec τ (Suc(x))→τ 7 Programs on length dependent vectors must satisfy length constraints to type. 8 Another example : ordered vectors

Syntax and semantics of dependent types. Antoine Delignat-Lavaud

Outline Dependent types Some motivations The type system Dependent function Natural numbers Dependent sum Identity types Universes Category-theoretic semantics Context morphisms Categories with families Interpretation

3

Dependent types

1 Types that depend on or vary withvalues. 2 Example :Vec τ (M), type of vectors of lengthM 3 M is a value in the calculus 4 The dependancy is writtenΠx:N.Vec τ (x) 5 Benefits : types are more accurate (e.g.N→List(N)) 6 More expressive static verification : H: Πx:N.Vec τ (Suc(x))→τ 7 on length dependent vectors must satisfy lengthPrograms constraints to type. 8 Another example : ordered vectors

Syntax and semantics of dependent types. Antoine Delignat-Lavaud

Outline Dependent types Some motivations The type system Dependent function Natural numbers Dependent sum Identity types Universes Category-theoretic semantics Context morphisms Categories with families Interpretation

3

Dependent types

1 Types that depend on or vary withvalues. 2 Example :Vec τ (M), type of vectors of lengthM 3 M is a value in the calculus 4 The dependancy is writtenΠx:N.Vec τ (x) 5 Benefits : types are more accurate (e.g.N→List(N)) 6 More expressive static verification : H: Πx:N.Vec τ (Suc(x))→τ 7 Programs on length dependent vectors must satisfy length constraints to type. 8 Another example : ordered vectors

Syntax and semantics of dependent types. Antoine Delignat-Lavaud

Outline Dependent types Some motivations The type system Dependent function Natural numbers Dependent sum Identity types Universes Category-theoretic semantics Context morphisms Categories with families Interpretation

3

4 naxa mes dtnyS pedeennd tianofcs tnioen eD ttpyse A . avaudlignat-L

Type-checking

Outline Dependent types Some motivations The type system Dependent function Natural numbers Dependent sum Identity types Universes Category-theoretic semantics Context morphisms Categories with families Interpretation

`ΓctxΓis a valid context Γ`σtypeσis a valid type in contextΓ Γ`M:σMis a term of typeσin contextΓ `Γ = ΔctxΓ,Δare definitionally equal contexts Γ`σ=τtypeσ, τare definitionally equal types in contextΓ Γ`M=N:σM,Nare equal terms of typeσin contextΓ

1  ?How to test equality of dependent types 2 Computationmay be requiredVec τ (1),Vec τ (0+0+1) 3 Arbitrary dependance : typing is undecidable. 4 Built-in type equality