nLab type refinement

Idea

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*?.

Predicate subtyping

Typing rules

Conditional expressions may be typed using the following rule:

$$\frac{\Gamma \vdash e:\mathsf{Bool} \qquad \Gamma, \underline{e} \vdash e_1 : T_1 \qquad \Gamma, \underline{\neg e} \vdash e_2 : T_2}{\Gamma \vdash \operatorname{if-then-else}(e, e_1, e_2) : T_1 \sqcup_e T_2}$$

where $\Gamma, \underline{e}$ is the enrichment of $\Gamma$ with the fact that $e$ is true, usually using a dummy variable, i.e., $\underline{e} = (\underline{} : \{ v : \mathsf{Unit} \mid e \})$, and where $T_1 \sqcup_e T_2$ is the dependent join of $T_1$ and $T_2$.

$$T_1 \sqcup_e T_2 = \{ v : T \mid (e \implies v \in T_1) \wedge (\neg e \implies v \in T_2) \}$$

Example

In a language with (dependent) predicate subtyping, one may implement and type negation as follows (see Jhala 2010):

val not : x:bool => bool[ b | b ⇔ ¬x ]
let not = x => { if (x) { false } else { true } };

Related concepts

• subset type?, subtype
• intrinsic and extrinsic views of typing

References

• Michael Greenberg, A refinement type by any other name, 2015, (blog post).
• Jana Dunfield, Combining Two Forms of Type Refinements, 2002, (report).
• Robert Atkey, Patricia Johann, Neil Ghani, When is a Type Refinement an Inductive Type?, (pdf).

On datasort refinements:

• Tim Freeman, Frank Pfenning, Refinement types for ML, Proceedings of the ACM Conference on Programming Language Design and Implementation, 1991, pp. 268–277, (pdf).
• Frank Pfenning, Church and Curry: Combining Intrinsic and Extrinsic Typing, (pdf).

On predicate subtyping:

• Ranjit Jhala, Niki Vazou, Refinement Types: A Tutorial, (arXiv:2010.07763).
• Yitzhak Mandelbaum, David Walker, Robert Harper, An Effective Theory of Type Refinements, (pdf).
• Susumu Hayashi, Logic of refinement types, Proceedings of the Workshop on Types for Proofs and Programs, 1993, pp. 157-172.

On index refinements in particular:

• Hongwei Xi, Frank Pfenning, Dependent types in practical programming, in A. Aiken, editor, Conference Record of the 26th Symposium on Principles of Programming Languages (POPL’99),pages 214–227. ACM Press, January 1999.

On refinement systems as functors:

• Paul-André Melliès, Noam Zeilberger, Type refinement and monoidal closed bifibrations, arXiv:1310.0263.
• Paul-André Melliès, Noam Zeilberger, Functors are Type Refinement Systems, (pdf , HAL).
• Paul-André Melliès, Noam Zeilberger, An Isbell Duality Theorem for Type Refinement Systems, (pdf).