Abstract
We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core calculus can express a rich variety of typing idioms; for example, intersection, union, negation, singleton, nullable, variant, and algebraic types are all derivable. We formulate a semantics in which expressions denote terms, and types are interpreted as first-order logic formulas. Subtyping is defined as valid implication between the semantics of types. The formulas are interpreted in a
specific model that we axiomatize using standard first-order theories. On this basis, we present a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The key idea is to rely on a Satisfiability Modulo Theories solver to compute subtyping efficiently. Moreover, using a satisfiability modulo theories solver allows us to show the uniqueness of normal forms for non-deterministic expressions, provide precise counterexamples when type-checking fails, detect empty types, and compute instances of types statically and at run-time.
specific model that we axiomatize using standard first-order theories. On this basis, we present a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The key idea is to rely on a Satisfiability Modulo Theories solver to compute subtyping efficiently. Moreover, using a satisfiability modulo theories solver allows us to show the uniqueness of normal forms for non-deterministic expressions, provide precise counterexamples when type-checking fails, detect empty types, and compute instances of types statically and at run-time.
Original language | English |
---|---|
Pages (from-to) | 31-105 |
Number of pages | 75 |
Journal | Journal of Functional Programming |
Volume | 22 |
Issue number | 1 |
DOIs | |
Publication status | Published - 2012 |