![[ICO]](/icons/blank.gif){kind=icon}
![[PARENTDIR]](/icons/back.gif){kind=icon}
![[TXT]](/icons/text.gif){kind=icon}
------------------------------------------------------------------------ -- A library for working with dependently typed syntax -- Nils Anders Danielsson ------------------------------------------------------------------------ -- This library is leaning heavily on two of Conor McBride's papers: -- -- * Type-Preserving Renaming and Substitution. -- -- * Outrageous but Meaningful Coincidences: Dependent type-safe -- syntax and evaluation. -- This module gives a brief overview of the modules in the library. module README where ------------------------------------------------------------------------ -- The library -- Contexts, variables, context morphisms, context extensions, etc. import deBruijn.Context -- Parallel substitutions (defined using an inductive family). import deBruijn.Substitution.Data.Basics -- A map function for the substitutions. import deBruijn.Substitution.Data.Map -- Some simple substitution combinators. (Given a term type which -- supports weakening and transformation of variables to terms various -- substitutions are defined and various lemmas proved.) import deBruijn.Substitution.Data.Simple -- Given an operation which applies a substitution to a term, -- satisfying some properties, more operations and lemmas are -- defined/proved. -- -- (This module reexports various other modules.) import deBruijn.Substitution.Data.Application -- A module which repackages (and reexports) the development under -- deBruijn.Substitution.Data. import deBruijn.Substitution.Data -- Some modules mirroring the development under -- deBruijn.Substitution.Data, but using substitutions defined as -- functions rather than data. -- -- The functional version of substitutions is in some respects easier -- to work with than the one based on data, but in other respects more -- awkward. I maintain both developments so that they can be compared. import deBruijn.Substitution.Function.Basics import deBruijn.Substitution.Function.Map import deBruijn.Substitution.Function.Simple -- The two definitions of substitutions are isomorphic (assuming -- extensionality). import deBruijn.Substitution.Isomorphic ------------------------------------------------------------------------ -- An example showing how the library can be used -- A well-typed representation of a dependently typed language. import README.DependentlyTyped.Term -- Normal and neutral terms. import README.DependentlyTyped.NormalForm -- Instantiation of deBruijn.Substitution.Data for terms. import README.DependentlyTyped.Term.Substitution -- Instantiation of deBruijn.Substitution.Data for normal and neutral -- terms. import README.DependentlyTyped.NormalForm.Substitution -- Normalisation by evaluation. import README.DependentlyTyped.NBE -- Various equality checkers (some complete, all sound). import README.DependentlyTyped.Equality-checker -- Raw terms. import README.DependentlyTyped.Raw-term -- A type-checker (sound). import README.DependentlyTyped.Type-checker -- A definability result: A "closed value" is the semantics of a -- closed term if and only if it satisfies all "Kripke predicates". import README.DependentlyTyped.Definability -- An observation: There is a term without a corresponding syntactic -- type (given some assumptions). import README.DependentlyTyped.Term-without-type -- Another observation: If the "Outrageous but Meaningful -- Coincidences" approach is used to formalise a language, then you -- can end up with an extensional type theory (with equality -- reflection). import README.DependentlyTyped.Extensional-type-theory -- Inductively defined beta-eta-equality. import README.DependentlyTyped.Beta-Eta -- TODO: Add an untyped example.