natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Types enable the restriction of the domain and codomain of computer programs, but they may not always be precise enough. Refining the type system of a language involves introducing subtypes while retaining the syntax of its terms. For instance, predicate subtyping can be used to limit head to non-empty lists (list{ l : len(l) > 0}) and div to non-zero arguments (int{ n : n <> 0 }).
More precisely, in Greenberg 2015, Frank Pfenning describes type refinement as a long-term research program with the following goals:
capture more precise properties of programs,
retain the good theoretical and practical properties of the simpler disciplines,
retain usability, modularity, elegance, etc.
Works in this program include:
datasort refinements (types are named refinement types) of Freeman, Davies, and Pfenning, which refine the set of available constructors for a type;
predicate subtyping (types are named refined types or predicate subtypes), where predicates are taken from a tractable domain (see for example index refinements of Xi and Pfenning);
but don’t include general subset types?, as type checking becomes undecidable.
Predicate subtyping is found in languages like Liquid Haskell? and F*?.
On datasort refinements:
On predicate subtyping:
On index refinements in particular:
On refinement systems as functors:
Last revised on December 19, 2023 at 19:17:52. See the history of this page for a list of all contributions to it.