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 ...
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
1Types that depend on or vary withvalues. 2Example :Vecτ(M), type of vectors of lengthM 3M is a value in the calculus 4The dependancy is writtenΠx:N.Vecτ(x) 5Benefits : types are more accurate (e.g.N→List(N)) 6More expressive static verification : H: Πx:N.Vecτ(Suc(x))→τ 7Programs on length dependent vectors must satisfy length constraints to type. 8Another 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
1Types that depend on or vary withvalues. 2Example :Vecτ(M), type of vectors of lengthM 3M is a value in the calculus 4The dependancy is writtenΠx:N.Vecτ(x) 5Benefits : types are more accurate (e.g.N→List(N)) 6More expressive static verification : H: Πx:N.Vecτ(Suc(x))→τ 7on length dependent vectors must satisfy lengthPrograms constraints to type. 8Another 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
1Types that depend on or vary withvalues. 2Example :Vecτ(M), type of vectors of lengthM 3M is a value in the calculus 4The dependancy is writtenΠx:N.Vecτ(x) 5Benefits : types are more accurate (e.g.N→List(N)) 6More expressive static verification : H: Πx:N.Vecτ(Suc(x))→τ 7on length dependent vectors must satisfy lengthPrograms constraints to type. 8Another 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
1Types that depend on or vary withvalues. 2Example :Vecτ(M), type of vectors of lengthM 3M is a value in the calculus 4The dependancy is writtenΠx:N.Vecτ(x) 5Benefits : types are more accurate (e.g.N→List(N)) 6More expressive static verification : H: Πx:N.Vecτ(Suc(x))→τ 7on length dependent vectors must satisfy lengthPrograms constraints to type. 8Another 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
1Types that depend on or vary withvalues. 2Example :Vecτ(M), type of vectors of lengthM 3M is a value in the calculus 4The dependancy is writtenΠx:N.Vecτ(x) 5Benefits : types are more accurate (e.g.N→List(N)) 6More expressive static verification : H: Πx:N.Vecτ(Suc(x))→τ 7on length dependent vectors must satisfy lengthPrograms constraints to type. 8Another 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
1Types that depend on or vary withvalues. 2Example :Vecτ(M), type of vectors of lengthM 3M is a value in the calculus 4The dependancy is writtenΠx:N.Vecτ(x) 5Benefits : types are more accurate (e.g.N→List(N)) 6More expressive static verification : H: Πx:N.Vecτ(Suc(x))→τ 7Programs on length dependent vectors must satisfy length constraints to type. 8Another 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
1Types that depend on or vary withvalues. 2Example :Vecτ(M), type of vectors of lengthM 3M is a value in the calculus 4The dependancy is writtenΠx:N.Vecτ(x) 5Benefits : types are more accurate (e.g.N→List(N)) 6More expressive static verification : H: Πx:N.Vecτ(Suc(x))→τ 7on length dependent vectors must satisfy lengthPrograms constraints to type. 8Another 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
1Types that depend on or vary withvalues. 2Example :Vecτ(M), type of vectors of lengthM 3M is a value in the calculus 4The dependancy is writtenΠx:N.Vecτ(x) 5Benefits : types are more accurate (e.g.N→List(N)) 6More expressive static verification : H: Πx:N.Vecτ(Suc(x))→τ 7Programs on length dependent vectors must satisfy length constraints to type. 8Another 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
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 2Computationmay be requiredVecτ(1),Vecτ(0+0+1) 3Arbitrary dependance : typing is undecidable. 4Built-in type equality