Extensible Datasort Refinements
Joshua Dunfield

arXiv:1701.02842v1 [cs.PL] 11 Jan 2017

University of British Columbia
Vancouver, Canada

Abstract. Refinement types turn typechecking into lightweight verification. The classic form of refinement type is the datasort refinement, in
which datasorts identify subclasses of inductive datatypes.
Existing type systems for datasort refinements require that all the refinements of a type be specified when the type is declared; multiple refinements of the same type can be obtained only by duplicating type
definitions, and consequently, duplicating code.
We enrich the traditional notion of a signature, which describes the inhabitants of datasorts, to allow re-refinement via signature extension,
without duplicating definitions. Since arbitrary updates to a signature
can invalidate the inversion principles used to check case expressions,
we develop a definition of signature well-formedness that ensures that
extensions maintain existing inversion principles. This definition allows
different parts of a program to extend the same signature in different
ways, without conflicting with each other. Each part can be type-checked
independently, allowing separate compilation.

1 Introduction
Type systems provide guarantees about run-time behaviour; for example, that
a record will not be multiplied by a string. However, the guarantees provided
by traditional type systems like Hindley–Milner do not include the absence of a
practically important class of run-time failures: nonexhaustive match exceptions.
For example, the type system of Standard ML allows a case expression over lists
that omits a branch for the empty list:
case elems of head :: tail => ...
If this expression is evaluated with elems bound to the empty list [], the exception Match will be raised.
Datasort refinements eliminate this problem: a datasort can express, within
the static type system, that elems is not empty; therefore, the case expression
is safe. Datasorts can also express less shallow properties. For example, the
definition in Figure 1 encodes conjunctive normal form—a formula that consists
of (possibly nested) Ands of clauses, where a clause consists of (possibly nested)
Ors of literals, where a literal is either a positive literal (a variable) or a negation
of a positive literal. A case expression comparing two values of type clause would

2
pos-literal
Var
Not
Or
And


:
:
:
:

literal, literal  clause, clause  cnf,
symbol → pos-literal,
pos-literal → literal,
(clause ∗ clause) → clause,
(cnf ∗ cnf) → cnf

Fig. 1. Datasorts for conjunctive normal form

only need branches for Or, Not and Var; the And branch could be omitted, since
And does not produce a clause.
Datasorts correspond to regular tree grammars, which can encode various
data structure invariants (such as the colour invariant of red-black trees), as
well as properties such as CNF and A-normal form. Datasort refinements are
less expressive than the “refinement type” systems (such as liquid types) that
followed work on index refinements and indexed types; like regular expressions,
which “can’t count”, datasorts cannot “count” the length of a list or the height
of a tree. However, types with datasorts are simpler in some respects; most
importantly, types with datasorts never require quantifiers. Avoiding quantifiers,
especially existential quantifiers, also avoids many complications in the type
checker. By analogy, regular expressions cannot solve every problem—but when
they can solve the problem, they may be the best solution.
The goal of this paper is to make datasort refinements more usable—not by
making datasorts express more invariants, but by liberating them from the necessity of a fixed specification (a fixed signature). First, we review the trajectory
of research on datasorts.
The first approach to datasort refinements (Freeman and Pfenning 1991;
Freeman 1994) extended ML, using abstract interpretation (Cousot and Cousot
1977) to infer refined types. The usual argument in favour of type inference is
that it reduces a direct burden on the programmer. When type annotations are
boring or self-evident, as they often are in plain ML, this argument is plausible.
But datasorts can express more subtle specifications, calling that argument into
question. Moreover, inference defeats a form of fine-grained modularity. Just as
we expect a module system to support information hiding, so that clients of a
module cannot depend on its internal details, a type system should prevent the
callers of a function from depending on its internal details. Inferring refinements
exposes those details. For example, if a function over lists is written with only
nonempty input in mind, the programmer may not have thought about what
the function should do for empty input, so the type system shouldn’t let the
function be applied to an empty list. Finally, inferring all properties means that
the inferred refined types can be long, e.g. inferring a 16-part intersection type
for a simple function (Freeman and Pfenning 1991, p. 271).
Thus, the second generation of work on datasort refinements (Davies and
Pfenning 2000; Davies 2005) used bidirectional typing, rather than inference.
Programmers have to write more annotations, but refinement checking will never
fabricate unintended invariants. A third generation of work (Dunfield and Pfen-

3

ning 2004; Dunfield 2007b) stuck with bidirectional type checking, though this
was overdetermined: other features of their type system made inference untenable.
All three generations (and later work by Lovas (2010) on datasorts for LF)
shared the constraint that a given datatype could be refined only once. The
properties tracked by datasorts could not be subsequently extended; the same
set of properties must be used throughout the program. Modular refinement
checking could be achieved only by duplicating the type definition and all related
code. Separate type-checking of refinements enables simpler reasoning about
programs, separate compilation, and faster type-checking (simpler refinement
relations lead to simpler case analyses).
The history of pattern typing (typing for case expressions) is also worth
noting, as formulating pattern typing seems to be the most difficult step in the
design of datasort type systems. Freeman supported a form of pattern matching
that was oversimplified. Davies implemented the full SML pattern language and
formalized most of it, but omitted as-patterns—which become nontrivial when
datasort refinements are in the picture.
In this paper, we allow multiple, separately declared refinements of a type
by revising a fundamental mechanism of datasort refinements: the signature.
Refinements are traditionally described using a signature that specifies—for the
entire program—which values of a datatype belong to which refinements. For
example, the type system can track the parity of bitstrings using the following
signature, which says that even and odd are subsorts (subtypes) of the type bits
of bitstrings, the empty bitstring has even parity, appending a 1 flips the parity,
and appending a 0 preserves parity.
even
Empty
One
Zero


:
:
:

bits, odd  bits,
even,
(even → odd) ∧ (odd → even),
(even → even) ∧ (odd → odd)

The connective ∧, read “and” or “intersection”, denotes conjunction of properties: adding a One makes an even bitstring odd (even → odd), and makes an odd
bitstring even (odd → even). Thus, if b is a bitstring known to have odd parity,
then appending a 1 yields a bitstring with even parity:
b : odd ⊢ One(b) : even
In some datasort refinement systems (Dunfield 2007b; Lovas 2010), the programmer specifies the refinements by writing a signature like the one above. In
the older systems of Freeman and Davies, the programmer writes a regular tree
grammar1, from which the system infers a signature, including the constructor
types and the subsort relation:
1

A regular tree grammar is like a regular grammar (the class of grammars equivalent
to regular expressions), but over trees instead of strings (Comon et al. 2008); the
leftmost terminal symbol in a production of a regular grammar corresponds to the
symbol at the root of a tree.

4

even = Empty | Zero(even) | One(odd)
odd = Zero(odd) | One(even)
In either design, the typing phase uses the same form of signature. We use
the first design, where the programmer gives the signature directly. Giving the
signature directly is more expressive, because it enables refinements to carry
information not present at run time. For example, we can refine natural numbers
by Tainted and Untainted:
Z
tainted
Z
Z

:

:
:

nat,
S : nat → nat,
nat, untainted  nat,
tainted,
S : tainted → tainted,
untainted, S : untainted → untainted

The sorts tainted and untainted have the same closed inhabitants, but a program
cannot directly create an instance of untainted from an instance of tainted:
x : tainted 6⊢ S(x) : untainted
Thus, the two sorts have different open inhabitants. This is analogous to dimension typing, where an underlying value is just an integer or float, but the type
system tracks that the number is in (for example) metres (Kennedy 1996).
Being able to give the signature directly allows programmers to choose between a variety of subsorting relationships. For example, to allow untainted data
to be used where tainted data is expected, write untainted  tainted. In effect,
subsorting can be either structural (as the signatures generated from grammars)
or nominal (as in the example above).
In this paper, giving signatures directly is helpful: it enables extension of a
signature without translating between signatures and grammars.
Contributions. This paper makes the following contributions:
– A language and type system with extensible signatures for datasort refinements (Section 3). Refinements are extended by blocks that are checked to
ensure that they do not weaken a sort’s inversion principle, which would
make typing unsound.
– A new formulation of typing (Section 4) for case expressions. This formulation is based on a notion of finding the intersection of a type with a pattern;
it concisely models the interesting aspects of realistic ML-style patterns.
– Type (datasort) preservation and progress for the type assignment system,
stated in Section 6 and proved in Appendix B, with respect to a standard
call-by-value operational semantics (Section 5).
– A bidirectional type system (Section 7), which directly yields an algorithm.
We prove that this system is sound (given a bidirectional typing derivation, erasing annotations yields a type assignment derivation) and complete
(given any type assignment derivation, annotations can be added to make
bidirectional typing succeed).
The appendix, which includes definitions and proofs omitted for space reasons, can be found at http://www.cs.cmu.edu/∼joshuad/papers/extensible/.

5

2 Datasort Refinements
What are datasort refinements? Datasort refinements are a syntactic discipline
for enforcing invariants. This is a play on Reynolds’s definition of types as a “syntactic discipline for enforcing levels of abstraction” (Reynolds 1983). Datasorts
allow programmers to conveniently categorize inductive data, and operations on
such data, more precisely than in conventional type systems.
Indexed types and related systems (e.g. liquid types and other “refinement
types”) also serve that purpose, but datasorts are highly syntactic, whereas
indexed types depend on the semantics of a constraint domain. For example,
to check the safety of accessing the element at position 2k of a 0-based array of length n, an indexed type system must check whether the proposition
2k < n is entailed in the theory of integers (under some set of assumptions,
e.g. 0 ≤ k ≤ n/3). The truth of 2k < n depends on the semantics of arithmetic, whereas membership in a datasort only depends on a head constructor
and the datasorts of its arguments. Put roughly, datasorts express regular grammars, and indexed types express grammars with more powerful side conditions.
(Unrestricted dependent types can express arbitrarily precise side conditions.)
Applications of datasort refinements. Datasorts are especially suited to applications of symbolic computing, such as compilers and theorem provers. Compilers
usually work with multiple internal languages, from abstract syntax through to
intermediate languages. These internal languages may be decomposed into further variants: source ASTs with and without syntactic sugar, A-normal form,
and so on. Similarly, theorem provers, SMT solvers, and related tools transform
formulas into various normal forms or sublanguages: quantifier-free Boolean formulas, conjunctive normal form, formulas with no free variables, etc. Many such
invariants can be expressed by regular tree grammars, and hence by datasorts.
Our extensible refinements offer the ability to use new refinements of a
datatype when the need arises, without the need to update a global refinement
declaration. For example, we could extend the types in Figure 1, in which clause
contains disjunctions of literals and cnf contains conjunctions of clauses, with a
new sort for conjunctions of literals:
[everything from Figure 1]

literal  conj-literal, conj-literal  cnf,
And : (conj-literal ∗ conj-literal) → conj-literal

What are datasort refinements not? First, datasorts are not really types, at least
not in the sense of Hindley–Milner type systems. A function on bitstrings (Section 1) has a best, or principal, type: bits → bits. In contrast, such a function may
have many refined types (sometimes called sorts), depending not only on the way
the programmer chose to refine the bits type, but on which possible properties
they wish to check. The type, or sort, of a function is a tiny module interface. In a
conventional Hindley–Milner type system, there is a best interface (the principal
type); with datasorts, the “best” interface is—as with a module interface, which
may reveal different aspects of the module—the one the programmer thinks best.

6
Term vars. x, y, . . .
Expressions e ::= x | λx. e | e1 e2 | (e1 , e2 ) | c(e) | case e of ms
| declare Σ in e —signature extension (Fig. 4)

Matches ms ::= · | (p ⇒ e) | ms
Values

v

::=

Patterns

p

::=

x | λx. e | (v1 , v2 ) | c(v) | (v:A)

| ∅ | c(p) | (p1 , p2 ) | x as p | p1 ⊔ p2
Fig. 2. Expressions

Datasorts
s, t, . . .
Types
A, B, D ::=
Typing contexts Γ ::=

1 | A→B | A ∗ B | s | A ∧ B
· | Γ, x : A

Fig. 3. Types and contexts

Maybe the programmer only cares that the function preserves odd parity, and
annotates it with odd → odd; the compiler will reject calls with even bitstrings,
even though such a call would be conventionally well-typed.
To infer sorts, as in the original work of Freeman, is like assuming that
all declarations in a module should be exposed. (Tools that suggest possible
invariants could be useful, just as a tool that suggests possible module interfaces
could be useful. But such tools are not the focus of this paper.)

3 A Type System with Extensible Refinements
This section gives our language’s syntax, introduces signatures, discusses the
introduction and elimination forms for datasorts, and presents the typing rules.
The details of typing pattern matching are in Section 4.
3.1 Syntax
The syntax of expressions (Figure 2) includes functions λx. e, function application e1 e2 , pairs (e1 , e2 ), constructors c(e), and case expressions. Signatures are
extended by declare Σ in e.
Types (Figure 3), written A and B, include unit (1), function, and product
types, along with datasorts s and t. The intersection type A ∧ B represents the
conjunction of the two properties denoted by A and B; for example, a function to
repeat a bitstring could be checked against type (odd → even) ∧ (even → even):
given any bitstring b, the repetition bb has even parity.
3.2 Unrefined types and signatures
Our unrefined types τ, in Figure 4, are very simple: unit 1, functions τ1 → τ2 ,
products τ1 ∗ τ2 , and datatypes d. We assume that each datatype has a known
set of constructors: for example, the bitstring type of Section 1 has constructors

7
Unrefined datatype names d
Unrefined types
τ ::= 1 | τ1 → τ2 | τ1 ∗ τ2 | d
Unrefined signatures
U ::= · | U, d | U, c : τ → d
Constructor types
Blocks

C ::= A → s
K ::= ·
empty block
| K, s1  s2
subsorting declaration
| K, c : C
constructor type decl.
Sort sets
S ::= (s1 ❁d1 , . . . , sn ❁dn )
Abbrev. sort sets
S ::= (s1 , . . . , sn )
Signatures
Σ, Ω ::= ·
empty signature
| Σ, ShKi
datasort specification
Under signature Σ (and unrefined signature U),

Σ ⊢ A ❁ τ type A is a refinement of unrefined type τ
Σ⊢1❁1

❁1

Σ ⊢ A1 ❁ τ1

Σ ⊢ A2 ❁ τ2

Σ ⊢ (A1 → A2 ) ❁ (τ1 → τ2 )

(s❁d) ∈ Σ
Σ⊢s❁d

❁Data

❁→

Σ ⊢ A1 ❁ τ1

Σ ⊢ A1 ❁ τ

Σ ⊢ A2 ❁ τ2

Σ ⊢ (A1 ∗ A2 ) ❁ (τ1 ∗ τ2 )
Σ ⊢ A2 ❁ τ

Σ ⊢ (A1 ∧ A2 ) ❁ τ

❁∗

❁∧

Fig. 4. Unrefined types and signatures, refined signatures, ❁

Empty, One and Zero. Refinements don’t add constructors; they only refine the
types of the given constructors. We assume that each program has some unrefined
signature U that gives datatype names (d) and (unrefined) constructor typings
(c : τ → d). Since this signature is the same throughout a program, we elide it
in most judgment forms.
The judgment Σ ⊢ A ❁ τ says that A is a refinement of τ. Both the symbol
❁ and several of the rules are reminiscent of subtyping, but that is misleading:
sorts and types are not in an inclusion relation in the sense of subtyping, because
the rule for → is covariant, not contravariant. Covariance is needed for functions
whose domains are nontrivially refined, e.g. odd → · · · , which is not a subtype
of bits → · · · because bits 6≤ odd.
Rule ❁∧ implements the usual refinement restriction: both parts of an intersection A1 ∧ A2 must refine the same unrefined type τ.
3.3 Signatures
Refinements are defined by signatures Σ (Figure 4).
As in past datasort systems, we separate signatures Σ from typing contexts
Γ . Typing assumptions over term variables (x, y, etc.) in Γ can mention sorts
declared in Σ, but the signature Σ cannot mention the term variables declared
in Γ . Thus, our judgment for term typing will have the form Σ; Γ ⊢ e : A, where
the term e can include constructors declared in Σ and variables declared in Γ ,
and the type A can include sorts declared in Σ. Some judgments, like subsorting

8

Σ ⊢ A type Type A is well-formed
Σ ⊢ 1 type

Σ ⊢ A1 type

WfType1

Σ ⊢ A1 type
Σ ⊢ A2 type
Σ ⊢ A1 → A2 type

Σ ⊢ A2 type

Σ ⊢ A1 ∗ A2 type

WfType→

Σ ⊢ A1 type
Σ ⊢ A2 type

Σ ⊢ A1 ❁ τ
Σ ⊢ A2 ❁ τ

Σ ⊢ A1 ∧ A2 type

s∈S
Σ, ShKi, Σ ′ ⊢ s type

WfType∗

WfType∧

WfTypeSort

Σ ⊢ c : C contype Under (prefix) context Σ, the typing c : C refines a typing in U
Σ ⊢ A type

Σ ⊢ s type

(c : τ → d) ∈ U

Σ ⊢ c : A → s contype

Σ ⊢ (A → s) ❁ (τ → d)

ContypeArr

Fig. 5. Type well-formedness

Σ ⊢ s  t and subtyping Σ ⊢ A ≤ B, are independent of variable typing and
don’t include Γ at all.
Traditional formulations of refinements assume the signature is given once
at the beginning of the program. Since the same signature is used throughout a
given typing derivation, the signature can be omitted from the typing judgments.
In this paper, our goal is to support extensible refinements, where the signature
can evolve within a typing derivation; in this respect, the signature is analogous
to an ordinary typing context Γ , which is extended in subderivations that type
λ-expressions and other binding forms. So the signature must be explicit in our
judgment forms.
Constructor types C are types of the form A → s. In past formulations of
datasorts, constructor types in the signature use intersection to represent multiple behaviours. For example, a “one” constructor for bitstrings, which represents
appending a 1 bit, takes odd-parity bitstrings to even-parity and vice versa; its
type in the signature is the intersection type (odd → even) ∧ (even → odd). Such
a formulation ensures that the signature has a standard property of (typing)
contexts: each data constructor is declared only once; additional behaviours are
conjoined (intersected) within a single declaration c : C1 ∧ C2 ∧ · · · . In our
setting, we must be careful about not only which types a constructor has, but
when those types were declared. The reasons are explained below; for now, just
note that we will write something like c : C1 , . . . , c : C2 rather than c : C1 ∧ C2 .
Structure of signatures. A signature Σ is a sequence of blocks ShKi of declarations, where refinements declared in outer scopes in the program appear to the
left of those declared in inner scopes.
Writing (s❁d)hKi declares s to be a sort refining some (unrefined) datatype
d; however, we usually elide the datatype and write just shKi. The declarations
K, called the block of s, define the values (constructors) of s, and the subsortings
for s. Declarations outside this block may declare new subsorts and supersorts

9

of s only if doing so would not affect s—for example, adding inhabitants to
s via a constructor declaration, or declaring a new subsorting between s and
previously declared sorts, would affect s and will be forbidden (via signature
well-formedness). The grammar generalizes this construct to multiple sorts, e.g.
(s1 ❁d1 , s2 ❁d2 )hKi, abbreviated as (s1 , s2 )hKi.
Writing s1  s2 says that s1 is a subsort of s2 , and c : C says that constructor
c has type C, where C has the form A → s. A constructor c can be given more
than one type: Σ = (s, s1 , s2 )hs1  s, s2  s, c : s1 →s2 , c : s2 →s1 i.
Adding inhabitants to a sort is only allowed within its block. Thus, the
following signature is ill-formed, because c ′ : 1→s adds the value c ′ () to s,
but c ′ : 1→s is not within s’s block: shc : s→si, thc ′ : 1→si. New sorts can be
declared as subsorts and supersorts of each other, and of previously declared
sorts: shc1 : 1→s, c2 : 1→si, tht  s, c2 : 1→ti.
However, a block cannot modify the subsorting relation between earlier sorts;
“backpatching” s1  s2 into the first block, through a new intermediate sort t, is
not permitted: The signature Σ∗ = (s1 , s2 )hc : 1→s1 , c : 1→s2 i, ths1  t, t  s2 i
is not permitted even though it looks safe: sorts s1 and s2 have the same set of
inhabitants—the singleton set {c()}—so the values of s1 are a subset of the values
of s2 . But this fact was not declared in the first block, which is the definition
of s1 and s2 . We assume the declaration of the first block completely reflects
the programmer’s intent: if they had wanted structural subsorting, rather than
nominal subsorting, they should have declared s1 s2 in the first block. Allowing
backpatching would not violate soundness, but would reduce the power of the
type system: nominal subsorting would no longer be supported, since it could
be made structural after the fact.
Ordering. A block ShKi can refer to the sorts S being defined and to sorts
declared to the left. In contrast to block ordering, the order of declarations
inside a block doesn’t matter.
3.4 Introduction form
From a type-theoretic perspective, the first questions about a type are: (1) How
are the type’s inhabitants created? That is, what are the type’s introduction
rules? (2) How are its inhabitants used? That is, what are its elimination rules?
(Gentzen (1934) would ask the questions in this order; the reverse order has
been considered by Dummett, among others (Zeilberger 2009).) In our setting,
we must also ask: What happens with the introduction and elimination forms
when new refinements are introduced?
In the introduction rule—DataI in Figure 6—the signature Σ is separated from
the ordinary context Γ (which contains typing assumptions of the form x : A).
The typing of c is delegated to its first premise, Σ ⊢ c : A → s, so we need a way
to derive this judgment. At the top of Figure 6, we define a single rule ConArr,
which looks up the constructor in the signature and weakens the result type
(codomain), expressing a subsumption principle. (Since we’ll have subsumption
as a typing rule, including it here is an unforced choice; its presence is meant to
make the metatheory of constructor typing go more smoothly.)

10

In a system of extensible refinements, adding refinements to a signature
should preserve typing. That is, if Σ; Γ ⊢ e : B, then Σ, Σ ′ ; Γ ⊢ e : B. This
is a weakening property: we can derive, from the judgment that e has type B
under Σ, the logically weaker judgment that e has type B under more assumptions Σ, Σ ′ . (The signature becomes longer, therefore stronger; but a turnstile
is a kind of implication with the signature as antecedent, so the judgment becomes weaker, hence “weakening”.) So for the introduction form, we need that
if Σ ⊢ c : A → s, then Σ, Σ ′ ⊢ c : A → s. Under our formulation of the signature,
this holds: If c : A → s, then there exists (c : A → s ′ ) ∈ Σ such that s ′  s.
Therefore, there exists (c : A → s ′ ) ∈ (Σ, Σ ′ ). Likewise, since Σ ⊢ s ′  s, we also
have Σ, Σ ′ ⊢ s ′  s. One cannot use Σ ′ to withdraw a commitment made in Σ.2
3.5 Elimination form: case expressions
Exhaustiveness checking for case expressions assumes complete knowledge about
the inhabitants of types. Thus, we must avoid extending a signature in a way
that adds inhabitants to previously declared sorts. Consider the case expression case x : empty of Nil() ⇒ () which is exhaustive for the signature Σ =
(list, empty)hempty  list, Nil : 1→empty, Cons : list→listi but not for
(Σ, Σ ′ ) = (list, empty)hempty  list, Nil : 1→empty, Cons : list→listi,
hCons : list→emptyi
Suppose we type-check the case expression under Σ, but then extend Σ to (Σ, Σ ′ ).
Evaluating the above case expression with x = Cons(Nil()) will “fall off the end”.
The inversion principle that “every empty has the form Nil()” is valid under Σ,
but with the additional type for Cons in Σ ′ , that inversion principle becomes
invalid under (Σ, Σ ′ ). Our system will reject the latter signature as ill-formed.
In the following, “up” and “down” are used in the usual sense: a subsort is
below its supersort. In Σ ′ , the second constructor type for Cons had a smaller
codomain than the first: the second type had empty, instead of list. Varying the
codomain downward can be sound when the lower codomain is newly defined:
Σ, Σ ′′ = Σ, subemptyhsubempty  empty, Nil : 1→subemptyi. Here, the inversion
principle that every empty is Nil is still valid (along with the new inversion
principle that every subempty is Nil). We only added information about a new
sort subempty, without changing the definition of list and empty.
Moving the domain down. Giving a new type whose domain is smaller, but that
has the same codomain, is sound but pointless. For example, extending Σ with
Cons : empty→list, which is the same as the type Σ has for Cons except that the
2

Under the traditional formulation where each constructor has just one type in a
signature, the relationship between the old signature Σ and the new signature would
be slightly more complicated: the old signature might contain c : C1 , and the new
signature c : C1 ∧ C2 , and we would need to explicitly eliminate the intersection to
expose the old type C1 . In our formulation, the new signature appends additional
typings for c while keeping the typing c : C1 intact.

11

domain is empty instead of list, is sound. The inversion principle for values v of
type list in Σ alone is “either (1) v has the form Nil(), or (2) v has the form
Cons(y) where y has type list”. Reading off the new inversion principle for list
from Σ, Cons : empty→list, we get “either (1) v has the form Nil(), or (2) v has
the form Cons(y) where y has type list, or (3) v has the form Cons(y) where
y has type empty”. Since empty is a subsort of list, part (3) implies part (2),
and any case arm that checks under the assumption that y : list must also check
under the assumption that y : empty. Here, the new signature is equivalent to Σ
alone; the “new” type for Cons is spurious.
Moving the codomain up. Symmetrically, giving a new type whose codomain gets
larger is sound but pointless. For example, adding Nil : 1→list to Σ has no effect,
because (in the introduction form) we could use the old type Nil : 1 → empty
with subsumption (empty  list).
Moving the domain up. Making the domain of a constructor larger is unsound
in general. To show this, we need a different starting signature Σ2 .
Σ2 = (list, empty, nonempty)hempty  list, nonempty  list,
Nil : 1→empty, Cons : empty→nonemptyi
This isn’t a very useful signature—it doesn’t allow construction of any list with
more than one element—but it is illustrative. We can read off from Σ2 the following inversion principle for values v of sort nonempty: “v has the form Cons(y)
where y has type empty”. If x : nonempty then case x of Cons(Nil()) ⇒ () is
exhaustive under Σ2 . Now, extend Σ2 : Σ2 , Σ2′ = Σ2 , hCons : list→nonemptyi.
For the signature Σ2 , Σ2′ , the inversion principle for nonempty should be “(1) v
has the form Cons(y) where y has type empty, or (2) v has the form Cons(y)
where y has type list”. But there are more values of type list than of type empty.
The new inversion principle gives less precise information about the argument
y, meaning that the old inversion principle gives more precise information than
(Σ2 , Σ2′ ) allows. Concretely, the case expression above was exhaustive under Σ2 ,
but is not exhaustive under (Σ2 , Σ2′ ) because Cons(Cons(Nil())) has type list.
The above examples show that signature extension can be sound but useless,
unsound, or sound and useful (when the domain and codomain, or just the
codomain, are moved down). Ruling out unsoundness will be the main purpose
of our type system, where unsoundness includes raising a “match” exception due
to a nonexhaustive case. The critical requirement is that each block must not
affect previously declared sorts by adding constructors to them, or by adding
subsortings between them.
3.6 Typing
Figure 6 gives rules deriving the main typing judgment Σ; Γ ⊢ e : A. The variable
rule Var, the introduction (→I) and elimination (→E) rules for →, and the introduction rules for the unit type (1I) and products (∗I) are standard. Products
can be eliminated via case e of (x1 , x2 ) ⇒ · · ·, so they need no elimination rule.

12
Under signature Σ,

(c : A → s ′ ) ∈ Σ

Σ ⊢ c : C constructor c has type C

Σ ⊢ s′  s

Σ ⊢ c : A→s

ConArr

Σ; Γ ⊢ e : A Under signature Σ and context Γ , expression e has type A
Σ; Γ, x : A, Γ ′ ⊢ x : A
Σ; Γ, x : A ⊢ e : B
Σ; Γ ⊢ (λx. e) : (A → B)
Σ; Γ ⊢ v : A1

Σ; Γ ⊢ e : A

Var

Σ; Γ ⊢ e1 : (A → B)

→I

Σ; Γ ⊢ v : A2
Σ; Γ ⊢ e2 : A2

Σ; Γ ⊢ (e1 , e2 ) : A1 ∗ A2
Σ; Γ ⊢ () : 1

Σ; Γ ⊢ e : A
Σ; Γ ; : A ⊢ ms : B
Σ; Γ ⊢ (case e of ms) : B

Σ; Γ ⊢ e2 : A

∗I

elimination via DataE
with (x1 , x2 ) ⇒ · · ·
Σ; Γ ⊢ e : A

Σ; Γ ⊢ c(e) : s

DataE

→E

∧Ek admissible
via Sub + ≤∧Lk

∧I

Σ ⊢ c : A→s

1I

Sub

Σ; Γ ⊢ e1 e2 : B

Σ; Γ ⊢ v : (A1 ∧ A2 )
Σ; Γ ⊢ e1 : A1

Σ⊢A≤B

Σ; Γ ⊢ e : B

(Σ, Σ ′ ) sig
Σ ⊢ B type

DataI

Σ, Σ ′ ; Γ ⊢ e : B

Σ; Γ ⊢ (declare Σ ′ in e) : B

Declare

Fig. 6. Typing rules for constructors and expressions

Subsumption. A subsumption rule Sub incorporates subtyping, based on the
subsort relation ; see Section 3.7. Several of the subtyping rules express the
same properties as elimination rules would; for example, anything of type A1 ∧
A2 has type A1 and also type A2 . Consequently, we can omit these elimination
rules without losing expressive power.
Intersection. The introduction rule ∧I corresponds to a binary version of the
introduction rule for parametric polymorphism in System F. The restriction
to a value v avoids unsoundness in the presence of mutable references (Davies
and Pfenning 2000), similar to SML’s value restriction for parametric polymorphism (Wright 1995). We omit the elimination rules, which are admissible using
Sub and subtyping (Section 3.7).
Σ; Γ ⊢ e : A1 ∧ A2
Σ; Γ ⊢ e : A1

Σ; Γ ⊢ e : A1 ∧ A2
Σ; Γ ⊢ e : A2

Datasorts. Rule DataI introduces a datasort, according to a constructor type
found in Σ (via the Σ ⊢ c : C judgment). Rule DataE examines an expression
e of type A and checks matches ms under the assumption that the expression
matches the wildcard pattern ; see Section 4.
Re-refinement. Rule Declare allows sorts to be declared. Its premises check that
(1) the signature Σ ′ is a valid extension of Σ (see Section 3.8); (2) the type B
of the expression is well-formed without the extension Σ ′ , which prevents sorts
declared in Σ ′ from escaping their scope; (3) that the expression e is well-typed
under the extended signature (Σ, Σ ′ ).

13

Σ ⊢ A ≤ B A is a subtype of B
Σ⊢1≤1
Σ ⊢ B1 ≤ A 1

≤1

Σ⊢ st

Σ ⊢ A 1 ≤ B1

Σ ⊢ A 2 ≤ B2

Σ ⊢ (A1 ∗ A2 ) ≤ (B1 ∗ B2 )

Σ ⊢ A 2 ≤ B2

Σ ⊢ (A1 → A2 ) ≤ (B1 → B2 )

≤→

Σ ⊢ Ak ≤ B
Σ ⊢ (A1 ∧ A2 ) ≤ B

≤∗

≤∧Lk

Σ⊢s≤t

≤Data

Σ ⊢ A ≤ B1
Σ ⊢ A ≤ B2
Σ ⊢ A ≤ (B1 ∧ B2 )

≤∧R

Fig. 7. Subtyping

3.7 Subtyping
Our subtyping judgment Σ ⊢ A ≤ B says that all values of type A also have type
B. The rules follow the style of Dunfield and Pfenning (2003); in particular, the
rules are orthogonal (each rule mentions only one kind of connective) and transitivity is admissible. Instead of an explicit transitivity rule, we bake transitivity
into each rule; for example, rule ≤∧L1 has a premise A1 ≤ B and conclusion
(A1 ∧ A2 ) ≤ B, rather than just (A1 ∧ A2 ) ≤ A1 (with no premises). This
makes the rules easier to implement: to decide whether A ≤ C, we never have
to guess a middle type B such that A ≤ B and B ≤ C.
3.8 Signature well-formedness
A signature is well-formed if standard conditions (e.g. no duplicate declarations
of sorts) and conservation conditions hold. Reading Figure 8 from bottom to
top, we start with well-formedness of signatures Σ sig. For each block ShKi, rule
SigBlock checks that the sorts S are not duplicates (S ∩ dom(Σ) = ∅), and then
checks that (1) subsorting is conserved by K and (2) each element in K is safe.
(1) Subsorting preservation. The subsortings declared in K must not affect the
subsort relation between sorts previously declared in Σ. The left-to-right direction of this “iff” always holds by weakening: adding to a signature cannot delete
edges in the subsort relation. The right-to-left direction is contingent on the contents of K; see signature Σ∗ in Section 3.3. This premise could also be written as
(Σ ⊢ |dom(Σ) ) = (Σ, ShKi ⊢ |dom(Σ) ), where |dom(Σ) is the  relation restricted
to sorts in dom(Σ).
(2a) Subsort elements. Rule BlockSubsort checks that the subsorts are in scope.
(2b) Constructor element safety. Rule BlockCon’s first premise checks that s ∈ S.
(Certain declarations with s ∈
/ S would be safe, but useless.) Its second premise
checks that the constructor type A → s is well-formed. Finally, for all sorts t that
were (1) previously declared (in dom(Σ)) and (2) supersorts of the constructor’s
codomain (s  t), the rule checks that the constructor is “safe at t”.
The judgment Σ; ShKi ⊢ c : A → s safe at t says that adding the constructor
typing c : A → s does not invalidate Σ’s inversion principle for t. Rule SafeConAt
checks that signature Σ already has a constructor typing c : A ′ → s ′ , where s ′ t,
such that A ≤ A ′ . Thus, any value c(v) typed using c : A → s can already be

14

dom(Σ) Domain (declared sorts) of Σ: dom(S1 hK1 i, . . . , Sn hKn i) = S1 ∪ · · · ∪ Sn

Σ ⊢ s1  s2 Sort s1 is a subsort of s2
s ∈ dom(Σ)
Σ⊢ss

ΣL , Sh. . . , s1  s2 , . . .i, ΣR ⊢ s1  s2
Refl

Σ ⊢ s1  s2

Σ ⊢ s2  s3

Assum

Trans

Σ ⊢ s1  s3

Σ; ShKi ⊢ c : C safe at t C safely extends a type given by Σ for c
(c : A ′ → s ′ ) ∈ Σ

Σ, ShKi ⊢ s ′  t
Σ, ShKi ⊢ s  s ′

Σ, ShKi ⊢ A ≤ A ′

Σ; ShKi ⊢ c : A → s safe at t

SafeConAt

Σ; ShKi ⊢ Kelem safe Kelem ∈ K is safe for Σ; ShKi
s1 , s2 ∈ (dom(Σ) ∪ S)
Σ; ShKi ⊢ s1  s2 safe

BlockSubsort

s∈S

Σ sig Signature Σ is well-formed
Σ sig
(S ∩ dom(Σ)) = ∅

Σ, ShKi ⊢ c : A → s contype
for all t ∈ dom(Σ)
such that Σ, ShKi ⊢ s  t,
Σ; ShKi ⊢ c : A → s safe at t

Σ; ShKi ⊢ c : A → s safe

for all t1 , t2 ∈dom(Σ),
Σ ⊢ t1  t2

iff Σ, ShKi ⊢ t1  t2

· sig

BlockCon

SigEmpty

for all Kelem ∈ K,
Σ; ShKi ⊢ Kelem safe

Σ, ShKi sig

SigBlock

Fig. 8. Signature well-formedness and subsorting

typed using c : A ′  s ′ , which is a subsort of t, so the new constructor typing
c : A → s does not add inhabitants to t.

This check is not analogous to function subtyping, because we need covariance (A ≤ A ′ ), not contravariance. The relation ❁ (Figure 4) is a closer analogy.
More subtly, SafeConAt also checks that ss ′ . Suppose we have the signature
Σ = (t, s1 , s2 )hs1  t, s2  t, c1 : s1 , c2 : s2 i and extend it with shs  t, c1 : si.
(To focus on the issue at hand, we assume c1 and c2 take no arguments.) For
the original signature Σ, the inversion principle for t is: If a value v has type t,
then either v = c1 and v has type s1 , or v = c2 and v has type s2 . However,
under the extended signature, there is a new possibility: v has type s. Merely
being inhabited by c1 is not sufficient to allow s to be a subsort of t.
If, instead, we start with Σ ′ = (t, s1 , s2 )hc1 : t , s1  t, s2  t, c1 : s1 , c2 : s2 i
then the inversion principle for t under Σ ′ is that v has type s1 , type s2 , or type
t. Therefore, any case arm whose pattern is x as c1 must be checked assuming
x : t. If an expression can be typed assuming x : t, then it can be typed assuming
x : t ′ for any t ′  t, so the inversion principle (again, under Σ ′ before extension)
is equivalent to “v has type t”. Extending Σ ′ with shs  t, c1 : si would extend

15

the inversion principle to say “if v : t then v has type t, or v has type s”, but
since s  t the extended inversion principle is equivalent to that for t under Σ ′ .
The s  s ′ premise of SafeConAt is needed to prove the constructor lemma
(Lemma 12), which says that a constructor typing in an extended signature must
be below a constructor typing in the original signature.

4 Typing Pattern Matching
Pattern matching is how a program gives different answers on different inputs. A
key motivation for datasort refinements is to exclude impossible patterns, so that
programmers can avoid having to choose between writing impossible case arms
(that raise an “impossible” exception) and ignoring nonexhaustiveness warnings.
The pattern typing rules must model the relationship between datasorts and the
operational semantics of pattern matching. It’s no surprise, then, that in datasort
refinement systems, case expressions lead to the most interesting typing rules.
The relationship between types and patterns is more involved than with, say,
Damas–Milner plus inductive datatypes: with (unrefined) inductive datatypes,
all the information needed to check for exhaustiveness (also called coverage) is
immediately available as soon as the type of the scrutinee is known. Moreover,
types for pattern variables can be “read off” by traversing the pattern top-down,
tracking the definition of the scrutinee’s inductive datatype. But with datasorts,
a set of patterns that looks nonexhaustive at first glance—looking only at the
head constructors—may in fact be exhaustive, thanks to the inner patterns.
Giving types to pattern variables is also tricky, because sufficiently precise
types may be evident only after examining the whole pattern. For example, when
matching x : bits against the pattern y as One(Empty), we shouldn’t settle on
y : bits because the scrutinee x has type bits; we should descend into the pattern
and observe that Empty : even and One : (even → odd), so y must have type odd.
Restricting the form of case expressions to a single layer of clearly disjoint
patterns c1 (x1 ) | . . . | cn (xn ) would simplify the rules, at the cost of a big gap
between theory and practice: Since real implementations need to support nested
patterns, the theory fails to model the real complexities of exhaustiveness checking and pattern variable typing. Giving code examples becomes fraught; either
we flatten case expressions (resulting in code explosion), or we handwave a lot.
Another option is to support the full syntax of case expressions, except for
as-patterns, so that pattern variables occur only at the leaves. If subsorting were
always structural, as in Davies’s system, we could exploit a handy equivalence
between patterns and values: if the pattern is x as c(p0 ), let-bind x to c(p0 )
inside the case arm, letting rule DataI figure out the type of x. But with nominal
subsorting, constructing a value is not equivalent; see Davies (2005, pp. 234–5)
and Dunfield (2007b, pp. 112–3).
Our approach is to support the full syntax, including as-patterns. This approach was taken by Dunfield (2007b, Chapter 4), but our system seems simpler—
partly because (except for signature extension) our type system omits indexed

16

U ⊢ p : τ Pattern p is suitable for values of unrefined type τ
U⊢

:τ

U ⊢p:τ

p-Wild

U ⊢ p1 : τ
U ⊢ p2 : τ
U ⊢ (p1 ⊔ p2 ) : τ

U ⊢ (x as p) : τ

p-Or

p-As

U ⊢ p1 : τ1
U ⊢ p2 : τ2
U ⊢ (p1 , p2 ) : τ1 ∗ τ2

U ⊢∅:τ

p-Pair

p-Empty

U ⊢ c : (τ → d)

U ⊢ () : 1

p-Unit

U ⊢p:τ

U ⊢ c(p) : d

p-Con

Fig. 9. Pattern type rules
For a scrutinee of type A that matches residual pattern p,

Σ; Γ ; p : A ⊢ ms : D check each match in ms against D
Σ⊢A❁τ
U ⊢ p1 : τ

for all (Γ ′ ⊢ B)
∈ intersect(Σ ⊢ A; p ∩ p1 ):
Σ; Γ, Γ ′ ⊢ e1 : D

Σ; Γ ; (p ∩ ¬p1 ) : A ⊢ ms : D

TypeMs
Σ; Γ ; p : A ⊢ (p1 ⇒ e1 ) | ms : D
intersect(Σ ⊢ A; p) = ∅
Σ; Γ ; p : A ⊢ ∅ : D

TypeMsEmpty

Fig. 10. Match typing

types and union types, but also because we avoid embedding typing derivations
inside derivations of pattern typing.
Instead, we confine most of the complexity to a single mechanism: a function
called intersect, which returns a set of types (and contexts that type as-variables)
that represent the intersection between a type and a pattern. The definition of
this function is not trivial, but does not refer to expression-level typing.
4.1 Unrefined pattern typing, match typing, and pattern operations
Figure 9 defines a judgment U ⊢ p : τ that says that pattern p matches values
of unrefined type τ under the unrefined signature U.
Rule DataE for case expressions (Figure 6) invokes a match typing judgment,
Σ; Γ ; p : A ⊢ ms : D. In this judgment, p is a residual pattern that represents the
space of possible values. For the first arm in a case expression, no patterns have
yet failed to match, so the residual pattern in the premise of DataE is .
Each arm, of the form p1 ⇒ e1 , is checked by rule TypeMs (Figure 10). The
leftmost premises check that the type A corresponds to the pattern type τ. The
middle “for all” checks e1 under various assumptions produced by the intersect
function (Section 4.2) with respect to the pattern p ∩ p1 , ensuring that if p1
matches the value at run time, the arm is well-typed. The last premise moves
on to the remaining matches; there, we know that the value did not match p1 ,
so we subtract p1 from the previous residual pattern p—expressed as p ∩ ¬p1 .
These operations are defined in the appendix (Figure 13).

17
Intersection of type A with pattern p

intersect(Σ ⊢ A; p) = B~∗ where each B∗ has the form (Γ ′ ⊢ B ′ )


intersect(Σ ⊢ A; ) = (· ⊢ A)
intersect(Σ ⊢ A; ∅) = ∅

intersect(Σ ⊢ A; x as p) = (Γ ′ , x : B ⊢ B) (Γ ′ ⊢ B) ∈ intersect(Σ ⊢ A; p)
intersect(Σ ⊢ A; p1 ⊔ p2 ) = intersect(Σ ⊢ A; p1 ) ∪ intersect(Σ ⊢ A; p2 )

intersect(Σ ⊢ A1 ∗ A2 ; (p1 , p2 )) = (Γ1 , Γ2 ⊢ B1 ∗ B2 ) (Γ1 ⊢ B1 ) ∈ intersect(Σ ⊢ A1 ; p1 )
and (Γ2 ⊢ B2 ) ∈ intersect(Σ ⊢ A2 ; p2 )

intersect(Σ ⊢ s; c(p0 )) = (Γ ′ ⊢ sc ) (c : Ac → sc ) ∈ Σ and Σ ⊢ sc  s
and (Γ ′ ⊢ B) ∈ intersect(Σ ⊢ Ac ; p0 )
Fig. 11. Intersection of a type with a pattern

When typing reaches the end of the matches, ms = ∅ in rule TypeMsEmpty,
we check that the case expression is exhaustive by checking that intersect returns
∅. For case expressions that are syntactically exhaustive, such as a case expression
over lists that has both Nil and Cons arms, the residual pattern p will be the
empty pattern ∅; the intersect function on an empty pattern returns ∅.
We define pattern complement ¬p and pattern intersection p1 ∩ p2 in the
appendix (Figure 13). For example, ¬ = ∅. No types appear in these definitions,
but the complement of a constructor pattern c(p0 ) uses the (implicit) unrefined
signature U. Our definition of pattern complement never generates as-patterns,
so we need not define intersection for as-patterns.
4.2 The intersect function
We define a function intersect that builds the “intersection” of a type and a
pattern. Given a signature Σ, type A and pattern p, the intersect function returns
a (possibly empty) set of tracks {(Γ1′ ⊢ B1 ), . . . , (Γn′ ⊢ Bn )}. Each track (Γ ′ ⊢ B) has
a list of typings Γ ′ (giving the types of as-variables) and a type B that represents
the subset of values inhabiting A that also match p. The union of B1 through Bn
constitutes the intersection of A and p. We call these “tracks” because each one
represents a possible shape of the values that match p, and the type-checking
“train” must check a given case arm under each track’s Γ ′ .
Many of the clauses in the definition of intersect (see Figure 10) are straightforward. The intersection of A with the wildcard is just {(· ⊢ A)}. Dually, the
intersection of A with the empty pattern ∅ is the empty set. In the same vein,
the intersection of A with the or-pattern p1 ⊔ p2 is the union of two intersections
(A with p1 , and A with p2 ). The intersection of a product A1 ∗ A2 with a pair
pattern is the union of products of the pointwise intersections.
The most interesting case is when we intersect a sort s with a pattern of the
form c(p0 ). For this case, intersect iterates through all the constructor declarations in Σ that could have been used to create the given value: those of the form
(c : Ac → sc ) where sc  s. For each such declaration, it calls intersect on Ac and
p0 . For each resulting track (Γ ′ ⊢ B), it returns a track (Γ ′ ⊢ sc ).

18

Optimization. In practice, it may be necessary to optimize the result of intersect.
If Σ = (list, empty)hempty  list, Nil : 1→empty, Cons : empty→list, Cons : list→listi

then intersect(Σ ⊢ Cons(x as ); list) returns (x : empty ⊢ list), (x : list ⊢ list) .
Since any case arm that checks under x : list will check under x : empty, there is
no point in trying to check under x : empty. Instead, we should check only under
x : list. A similar optimization in the Stardust type checker could reduce the size
of the set of tracks by “about an order of magnitude” (Dunfield 2007b, p. 112).
Missing clauses? As is standard in typed languages, pattern matching doesn’t
look inside λ, so intersect needs no clause for →/λ. If we can’t match on an arrow
type, we don’t need to match on intersections of arrows. The other useful case of
intersection is on sorts, s1 ∧ s2 . However, an intersection of sorts can be obtained
by declaring a new sort below s1 and s2 with the appropriate constructor typings,
so we omit such a clause from the definition.
Comparison to an earlier system. A declarative system of rules in Dunfield
(2007b, Chapter 4) appears to be a conservative extension of intersect: the earlier system supports a richer type system, but for the features in common, the
information produced is similar to that of intersect. The earlier system was based
on a judgment Σ ⊢ p ⇐ A ✄ (e ⇐ D). To clarify the connection to the present
system, we adjust notation; for example, we make Σ explicit.
The meta-variables Σ, p, and A directly correspond to the arguments to
intersect, while e and D correspond to e1 and D in our rule TypeMs. No metavariables correspond directly to the tracks in the result of intersect, but within
Σ ⊢ p ⇐ A ✄ (e ⇐ B), we find subderivations of B + Γ ⊢ forgettype ✄ e ⇐
D, where the set of pairs hΓ, Bi indeed correspond to the result of intersect.
Cutting through the differences in the formalism, and omitting rules for
unions and other features not present in this paper, the earlier system behaves
like intersect. For example, (p1 , p2 ) was also handled by considering each component, and assembling all resulting combinations. Perhaps most importantly,
c(p0 ) was also handled by considering each constructor type in the signature,
filtering out inappropriate codomains, and recursing on p0 . A rule for ∧ appears
in the declarative system in Dunfield (2007b, Chapter 4), but the rule was never
implemented, and seems not to be needed in practice.
Since the information given by the older system is precise enough to check
interesting invariants of actual programs, our definition of intersect should also
be precise enough.

5 Operational Semantics
We prove our results with respect to a call-by-value, small-step operational semantics. The main judgment form is e 7→ e ′ , which uses evaluation contexts E.
Stepping case expressions is modelled using a judgment ms 7→v e ′ , which compares each pattern in ms against the value v being cased upon. This comparison
is handled by the judgment p match v −→ θ, which says that θ is evidence that
p matches v (that is, [θ]p = v). The rules are in Figure 14 in the appendix.

19

6 Metatheory
This section gives definitions, states some lemmas and theorems, and discusses
their significance in proving our main results. For space reasons, we summarize
a number of lemmas; their full statements appear in the appendix. All proofs
are also relegated to the appendix.
Subtyping and subsorting. Subtyping is reflexive and transitive (Lemmas 6–7).
We define what it means for signature extension to preserve subsorting:
Definition 1 (Preserving subsorting). Given Σ1 and Σ2 , we say that Σ2 preserves
subsorting of Σ1 iff for all sorts s, t ∈ dom(Σ1 ), if Σ1 , Σ2 ⊢ s  t then Σ1 ⊢ s  t.
This definition allows new sorts in dom(Σ2 ) to be subsorts or supersorts of
the old sorts in dom(Σ1 ), provided that the subsort relation between the old
sorts doesn’t change.
If two signatures do not have subsortings that cross into each other’s domain,
they are non-adjacent ; non-adjacent signatures preserve subsorting.
Definition 2 (Non-adjacency). Two signatures Σ1 and Σ2 are non-adjacent iff
each signature contains no subsortings of the form s1  s2 or s2  s1 , where
s1 ∈ dom(Σ1 ) and s2 ∈ dom(Σ2 ).
Theorem 1 (Non-adjacent preservation).
If Σ2 preserves subsorting of Σ1 and Σ3 preserves subsorting of Σ1
and Σ2 and Σ3 are non-adjacent then Σ3 preserves subsorting of (Σ1 , Σ2 ).
Strengthening, weakening, and substitution. Theorem 4 (Weakening) will allow
the assumptions in a judgment to be changed in two ways: (1) the signature may
be strengthened by replacing a signature (Σ, Σ ′ ) with a signature (Σ, Ω, Σ ′ ); and
(2) the context may be strengthened by replacing Γ with a context Γ + in which
any typing assumption (x : A) ∈ Γ can be replaced with (x : A+ ) ∈ Γ , if A ≤ A+ .
Repeatedly applying (1) with different Ω leads to a more general notion of
strengthening a signature:
Definition 3. A signature Σ ′ is stronger than Σ, written Σ ′ ≤sig Σ, if Σ ′ can be
obtained from Σ by inserting entire signatures at any position in Σ.
We often use the less general notion (inserting a single Ω), which simplifies
proofs. For any result stated less generally, however, the more general strengthening of Definition 3 can be shown by induction on the number of blocks inserted.
Definition 4. Under Σ, a context Γ ′ is stronger than Γ , written Σ ⊢ Γ ′ ≤ctx Γ , if
for each (x : A ′ ) ∈ Γ ′ , there exists (x : A) ∈ Γ such that Σ ⊢ A ′ ≤ A.
Several lemmas show weakening. Lemma 8 says that Σ in Σ ⊢ J can be
replaced by a stronger Σ ′ , where J has the form A type or s1  s2 or A ≤ B or
c : A → s or A ❁ τ or c : C. Lemma 9 says that (Σ, Ω, Σ ′ ) can replace (Σ, Σ ′ ) in
Σ, Σ ′ ; ShKi ⊢ c : A → s safe at t. Lemma 10 allows the sort t ′ in the judgment
Σ; ShKi ⊢ c : A → s safe at t ′ to be replaced by a supersort t.
Using the above lemmas and Theorem 1, we can show that the key judgment
“· · · c : A→s safe” can be weakened by inserting Ω inside the signature:

20

Theorem 2 (Weakening ‘safe’).
If (Σ, Σ ′ ) sig and (Σ, Ω) sig and dom(Σ ′ ) ∩ dom(Ω) = ∅
and dom(Σ, Ω, Σ ′ ) ∩ S = ∅ and K does not mention anything in dom(Ω)
and ShKi preserves subsorting for (Σ, Σ ′ )
and (c : A → s) ∈ K and Σ, Σ ′ ; ShKi ⊢ c : A → s safe
then Σ, Ω, Σ ′ ; ShKi ⊢ c : A → s safe.

With this additional lemma, we have weakening for the judgments involved
in checking that a signature is well-formed, so we can show that if Σ is safely
extended by Σ ′ and separately by Ω, then Ω and Σ ′ , together, safely extend Σ.
Theorem 3 (Signature Interleaving).
If (Σ, Σ ′ ) sig and (Σ, Ω) sig and dom(Σ ′ ) ∩ dom(Ω) = ∅ then (Σ, Ω, Σ ′ ) sig.
Ultimately, we will show type preservation; in the preservation case for the
Declare rule, we extend the signature in a premise. We therefore need to show
that the typing judgment can be weakened. Since the typing rules for matches
involve the intersect function, we need to show that a stronger input to intersect
yields a stronger output; that is, a longer (stronger) signature yields a stronger
type B+ (a subtype of B) and a stronger context Γ+ typing as-variables.
Definition 5. Under a signature Σ, a track (Γ+ ⊢ B+ ) is stronger than (Γ ⊢ B),
written Σ ⊢ (Γ+ ⊢ B+ ) ≤trk (Γ ⊢ B), if and only if Σ ⊢ Γ+ ≤ctx Γ and Σ ⊢ B+ ≤ B.
A set of tracks B~∗+ is stronger than B~∗ , written B~∗+ ≤trk B~∗ , if and only
if, for each track (Γ+ ⊢ B+ ) ∈ B~∗+ , there exists a track (Γ ⊢ B) ∈ B~∗ such that
(Γ+ ⊢ B+ ) ≤trk (Γ ⊢ B) ∈ B~∗ .
Lemma 13 says that the result of intersect on a stronger signature is stronger.
We can then show that weakening holds for the typing judgment itself, along
with substitution typing (defined in the appendix) and match typing.
Theorem 4 (Weakening).
If (Σ, Σ ′ ) sig, (Σ, Ω) sig, dom(Σ ′ ) ∩ dom(Ω) = ∅ and Σ, Ω, Σ ′ ⊢ Γ + ≤ctx Γ then
(1) If Σ, Σ ′ ; Γ ⊢ e : A then Σ, Ω, Σ ′ ; Γ + ⊢ e : A.
(2) If Σ, Σ ′ ; Γ ⊢ θ : Γ ′ then Σ, Ω, Σ ′; Γ + ⊢ θ : Γ ′ .
(3) If Σ, Σ ′ ; Γ ; p : A ⊢ ms : D then Σ, Ω, Σ ′ ; Γ + ; p : A ⊢ ms : D.
Properties of values. Substitution properties (Lemmas 14 and 15) and inversion
(or canonical forms) properties (Lemma 16) hold.
Type preservation and progress. The last important piece needed for type preservation is that intersect does what it says: if a value v matches p, then v has type
B where B is one of the outputs of intersect.
Theorem 5 (Intersect). If Σ sig and Σ; · ⊢ v : A and Σ ⊢ A type and p match v −→
θ and intersect(Σ ⊢ A; p) = B~∗ then there exists (Γ ′ ⊢ B) ∈ B~∗ s.t. Σ; · ⊢ v : B
and Σ; · ⊢ θ : Γ ′ where Σ ⊢ B type and Σ ⊢ B ≤ A.
The preservation result allows for a longer signature, to model entering the
scope of a declare expression or the arms of a match. We implicitly assume
that, in the given typing derivation, all types are well-formed under the local
signature: for any subderivation of Σ; Γ ⊢ e ′ : B, it is the case that Σ ⊢ B type.

21

Theorem 6 (Preservation). If Σ sig and Σ; · ⊢ e : A and e 7→ e ′
then there exists Σ ′ such that Σ, Σ ′ ⊢ e ′ : A where (Σ, Σ ′ ) sig.
Theorem 7 (Progress).
If Σ sig and Σ; · ⊢ e : A then e is a value or there exists e ′ such that e 7→ e ′ .

7 Bidirectional Typing
The type assignment system in Figure 6 is not syntax-directed, because the rules
Sub and ∧I apply to any shape of expression. Nor is the system directed by the
syntax of types: rule Sub can conclude e : B for any type B that is a supertype
of some other type A. Finally, while the choice to apply rule DataI is guided
by the shape of the expression—it must be a constructor application c(e)—the
resulting sort is not uniquely determined, since the signature can have multiple
constructor typings for c.
Fortunately, obtaining an algorithmic system is straightforward, following
previous work with datasort refinements and intersection types. We follow the
bidirectional typing recipe of Davies and Pfenning (2000); Davies (2005); Dunfield and Pfenning (2004):
1. Split the typing judgment into checking Σ; Γ ⊢ e ⇐ A and synthesis Σ; Γ ⊢
e ⇒ A judgments. In the checking judgment, the type A is input (it might be
given via type annotation); in the synthesis judgment, the type A is output.
2. Allow change of direction: Change the subsumption rule to synthesize a
type, then check if it is a subtype of a type being checked against; add an
annotation rule that checks e against A in the annotated expression (e : A).
3. In each introduction rule, e.g. →I, make the conclusion a checking judgment;
in each elimination rule, e.g. DataE, make the premise that contains the
eliminated connective a synthesis judgment.
4. Make the other judgments in the rules either checking or synthesizing, according to what information is available. For example, the premise of →I
becomes a checking judgment, because we know B from the conclusion.
5. Since the subsumption rule cannot synthesize, add rules such as Syn∧E1 ,
which were admissible in the type assignment system.
This yields the rules in Figure 12. (Rules for the match typing judgment Σ; Γ ; p :
A ⊢ ms ⇐ B can be obtained from Figure 10 by replacing “:” in “e1 : D” and
“ms : D” with “⇐”.) While this system is much more algorithmic than Figure
6, the presence of intersection types requires backtracking: if we apply a function
of type (even → odd) ∧ (odd → even), we need to synthesize even → odd first; if
we subsequently fail (e.g. if the argument has type odd), we backtrack and try
odd → even. Similarly, if the signature contains several typings for a constructor
c, we may need to try rule ChkDataI with each typing.
Type-checking for this system is almost certainly PSPACE-complete (Reynolds
1996); however, the experience of Davies (2005) shows that a similar system, differing primarily in whether the signature can be extended, is practical if certain
techniques, chiefly memoization, are used.

22

Σ; Γ ⊢ e ⇐ A

Σ; Γ ⊢ e ⇒ A Expr. e checks against (⇐) / synthesizes (⇒) type A

′

Σ; Γ, x : A, Γ ⊢ x ⇒ A

SynVar

Σ; Γ, x : A ⊢ e ⇐ B

Σ; Γ ⊢ v ⇐ A2

Σ; Γ ⊢ v ⇐ (A1 ∧ A2 )
Σ; Γ ⊢ e1 ⇐ A1

Σ ⊢ c : A→s

Σ; Γ ⊢ e ⇐ B

Σ; Γ ⊢ e ⇐ A

(Σ, Σ ′ ) sig

~
A∈A

Σ; Γ ⊢ e ⇐ A
SynAnno
~ ⇒A
Σ; Γ ⊢ (e:A)
Σ; Γ ⊢ e2 ⇐ A

Σ; Γ ⊢ e1 e2 ⇒ B

Σ; Γ ⊢ e ⇒ (A1 ∧ A2 )

Chk∧I

Σ; Γ ⊢ e2 ⇐ A2

Σ; Γ ⊢ (e1 , e2 ) ⇐ A1 ∗ A2

Σ; Γ ⊢ c(e) ⇐ s

ChkSub

Σ; Γ ⊢ e1 ⇒ (A → B)

Chk→I

Σ; Γ ⊢ (λx. e) ⇐ (A → B)

Σ; Γ ⊢ v ⇐ A1

Σ; Γ ⊢ e ⇒ A
Σ⊢A≤B

ChkDataI
Σ ⊢ B type

k ∈ {1, 2}

Σ; Γ ⊢ e ⇒ Ak

Chk∗I

Σ; Γ ⊢ e ⇒ A

Σ; Γ ⊢ () ⇐ 1
Σ; Γ ;

Σ; Γ ⊢ (declare Σ ′ in e) ⇐ B

Syn∧Ek

Chk1I

: A ⊢ ms ⇐ B

Σ; Γ ⊢ (case e of ms) ⇐ B

Σ, Σ ′ ; Γ ⊢ e ⇐ B

Syn→E

ChkDataE

ChkDeclare

Fig. 12. Bidirectional typing rules

Using these rules, annotations are required exactly on (1) the entire program
e (if e is a checked form, such as a λ) and (2) expressions not in normal form,
such as a λ immediately applied to an argument, a recursive function declaration,
or a let-binding (assuming the rule for let synthesizes a type for the bound
expression). Rules with “more synthesis”—such as a synthesizing version of ∗I—
could be added along the lines of previous bidirectional type systems (Xi 1998;
Dunfield and Krishnaswami 2013).
~ Rule SynAnno
Following Davies (2005), an annotation can list several types A.
chooses one of these, backtracking if necessary. Multiple types may be needed
if a λ-term is checked against intersection type: when checking (λx. x) against
(even → even) ∧ (odd → odd), the type of x will be even inside the left subderivation of Chk∧I, but odd inside the right subderivation. Thus, if we annotate x
with even, the check against odd → odd fails; if we annotate x with odd, the
check against even → even fails. For a less contrived example, and for a variant
annotation form that reduces backtracking, see Dunfield and Pfenning (2004).
In the appendix, we prove that our bidirectional system is sound and complete
with respect to our type assignment system:
Theorem 8 (Bidirectional soundness). If Γ ⊢ e ⇐ A or Γ ⊢ e ⇒ A then
Γ ⊢ |e| : A where |e| is e with all annotations erased.
Theorem 9 (Annotatability).

If Γ ⊢ e : A then:

(1) There exists e⇐ such that |e⇐ | = e and Γ ⊢ e⇐ ⇐ A.
(2) There exists e⇒ such that |e⇒ | = e and Γ ⊢ e⇒ ⇒ A.
We also prove that the ⇒ and ⇐ judgments are decidable (Theorem 10).

23

8 Related Work
Datasort refinements. Freeman and Pfenning (1991) introduced datasort refinements with intersection types, defined the refinement restriction (where A ∧ B
is well-formed only if A and B are refinements of the same type), and developed
an inference algorithm in the spirit of abstract interpretation. As discussed earlier, the lack of annotations not only makes the types difficult to see, but makes
inference prone to finding long, complex types that include accidental invariants.
Davies (2005), building on the type system developed by Davies and Pfenning
(2000), used a bidirectional typing algorithm, guided by annotations on redexes.
This system supports parametric polymorphism through a front end based on
Damas–Milner inference, but—like Freeman’s system—does not support extensible refinements. Davies’s CIDRE implementation (Davies 2013) goes beyond
his formalism by allowing a single type to be refined via multiple declarations,
but this has no formal basis; CIDRE appears to simply gather the multiple declarations together, and check the entire program using the combined declaration,
even when this violates the expected scoping rules of SML declarations.
Datasort refinements were combined with union types and indexed types by
Dunfield and Pfenning (2003, 2004), who noticed the expressive power of nominal
subsorting, called “invaluable refinement” (Dunfield 2007b, pp. 113, 220–230).
Giving multiple refinement declarations for a single datatype was mentioned
early on, as future work: “embedded refinement type declarations” (Freeman and
Pfenning 1991, p. 275); “or even . . . declarations that have their scope limited”
(Freeman 1994, p. 167); “it does seem desirable to be able to make local datasort
declarations” (Davies 2005, p. 245). But the idea seems not to have been pursued.
Logical frameworks. In the logical framework LF (Harper et al. 1993), data is
characterized by declaring constructors with their types. In this respect, our system is closer to LF than to ML: LF doesn’t require all of a type’s constructors to
be declared together. By itself, LF has no need for inversion principles. However,
systems such as Twelf (Pfenning and Schürmann 1999), Delphin (Poswolsky and
Schürmann 2009) and Beluga (Pientka and Dunfield 2010) use LF as an objectlevel language but also provide meta-level features. One such feature is coverage
(exhaustiveness) checking, which needs inversion principles for LF types. Thus,
these systems mark a type as frozen when its inversion principle is applied (to
process %covers in Twelf, or a case expression in Beluga); they also allow the
user to mark types as frozen. These systems lack subtyping and subsorting; once
a type is frozen, it is an error to declare a new constructor for it.
Lovas (2010) extended LF with refinements and subsorting, and developed
a constraint-based algorithm for signature checking. This work did not consider
meta-level features such as coverage checking, so it yields no immediate insights
about inversion principles or freezing. Since Lovas’s system takes the subsorting
relation directly from declarations, rather than by inferring it from a grammar,
it supports what Dunfield (2007b) called invaluable refinements; see Lovas’s example (Lovas 2010, pp. 145–147).

24

Indexed types and refinement types. As the second generation of datasort refinements (exemplified by the work of Davies and Pfenning) began, so did a related
approach to lightweight type-based verification: indexed types or limited dependent types (Xi and Pfenning 1999; Xi 1998), in which datatypes are refined by
indices drawn from a (possibly infinite) constraint domain. Integers with linear
inequalities are the standard example of an index domain; another good example is physical units or dimensions (Dunfield 2007a). More recent work in this
vein, such as liquid types (Rondon et al. 2008), uses “refinement types” for a
mechanism close to indexed types.
Datasort refinements have always smelled like a special case of indexed types.
At the dawn of indexed types (and the second generation of datasort refinements), the relationship was obscured by datasorts’ “fellow traveller”, intersection types, which were absent from the first indexed type systems, and remain
absent from the approaches now called “refinement types”. That is, while datasorts themselves strongly resemble a specific form of indices—albeit related by
a partial order (subtyping), rather than by equality—and would thus suggest
that indexed type systems subsume datasort refinement type systems, the inclusion of intersection types confounds such a comparison. Intersection types are
present, along with both datasorts and indices, in Dunfield and Pfenning (2003)
and Dunfield (2007b); the relationship is less obscured. But no one has given an
encoding of types with datasorts into types with indices, intersections or no.
The focus of this paper is a particular kind of extensibility of datasort refinements, so it is natural to ask whether indexed types and (latter-day) refinement
types have anything similar. Indexed types are not immediately extensible: both
Xi’s DML and Dunfield’s Stardust require that a given datatype be refined exactly once. Thus, a particular list type may carry its length, or the value of its
largest element, or the parity of its boolean elements. By refining the type with
a tuple of indices, it may also carry combinations of these, such as its length
and its largest element. Subsequent uses of the type can leave out some of the
indices, but the combination must be stated up front.
However, some of the approaches descended from DML, such as liquid types,
allow refinement with a predicate that can mention various attributes. These
attributes are declared separately from the datatype; adding a new attribute
does not invalidate existing code. Abstract refinement types (Vazou et al. 2013)
even allow types to quantify over predicates.
Setting aside extensibility, datasort refinements can express certain invariants
more clearly and succinctly than indexed types (and their descendants).
Program analysis. Koot and Hage (2015) formulate a type system that analyzes
where exceptions can be raised, including match exceptions raised by nonexhaustive case expressions. This system appears to be less precise than datasorts, but
has advantages typical to program analysis: no type annotations are required.

25

9 Future Work
Modular refinements. This paper establishes a critical mechanism for extensible
refinements, safe signature extension, in the setting of a core language without
modules: refinements are lexically scoped. To scale up to a language with modules, we need to ask: what notions of scope are appropriate? For example, a
strict λ-calculus interpreter could be refined with a sort val of values, while a
lazy interpreter could be refined with a sort whnf of terms in weak head normal
form. If every val is a whnf, we might want to have val  whnf. In the present
system, these two refinements could be in separate declare blocks; in that case,
val and whnf could not both be in scope, and the subsorting is not well-formed.
Alternatively, one declare block could be nested inside the other. In that case,
val  whnf could be given in the nested block, since it would not add new subsortings within the outer refinement. In a system with modules, we would likely
want to have val  whnf, at least for clients of both modules; such backpatching
is currently not allowed, but should be safe since the new subsorting crosses two
independent signature blocks (the block declaring val and the block declaring
whnf) without changing the subsortings within each block.
Type polymorphism. Standard parametric polymorphism is absent in this paper,
but it should be feasible to follow the approach of Davies (2005), as long as
the unrefined datatype declarations are not themselves extensible (which would
break signature well-formedness, even without polymorphism).
Datasort polymorphism. Extensible signatures open the door to sort-bounded
polymorphism. In our current system, a function that iterates over an abstract
syntax tree and α-renames free variables—which would conventionally have the
type exp → exp—must be duplicated, even though the resulting tree has the same
shape and the same constructors, and therefore should always produce a tree of
the same sort as the input tree (at least, if the free variables are not specified
with datasorts). We would like the function to check against a polymorphic type
∀αexp. α → α, which works for any sort α below exp.
We would like to reason “backwards” from a pattern match over a polymorphic sort variable α. For example, if a value of type α matches the pattern
Plus(x1, x2), then we know that Plus : (α1 ∗ α2 ) → α for some sorts α1 and α2 .
The recursive calls on x1 and x2 must preserve the property of being in α1 and
α2 , so Plus(f x1, f x2) has type α, as needed. The mechanisms we have developed
may be a good foundation for adding sort-bounded polymorphism: the intersect
function would need to return a signature, as well as a context and type, so that
the constructor typing Plus : (α1 ∗ α2 ) → α can be made available.
Implementation. Currently, we have a prototype of a few pieces of the system,
including a parser and implementations of the Σ sig judgment and the intersect
function. Experimenting with these pieces was helpful during the design of the
system (and reassured us that the most novel parts of our system can be implemented), but they fall short of a usable implementation.

Bibliography

H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and
M. Tommasi. Tree automata techniques and applications. https://gforge.
inria.fr/frs/download.php/file/10994/tata.pdf, 2008. Release of 18
November 2008.
Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice
model for static analysis of programs by construction or approximation of
fixpoints. In Principles of Programming Languages, pages 238–252, 1977.
Rowan Davies. Practical Refinement-Type Checking. PhD thesis, Carnegie Mellon University, 2005. CMU-CS-05-110.
Rowan Davies. SML checker for intersection and datasort refinements (pronounced “cider”). https://github.com/rowandavies/sml-cidre, 2013.
Rowan Davies and Frank Pfenning. Intersection types and computational effects.
In ICFP, pages 198–208, 2000.
Joshua Dunfield. Refined typechecking with Stardust. In Programming Languages meets Program Verification (PLPV ’07), 2007a.
Joshua Dunfield. A Unified System of Type Refinements. PhD thesis, Carnegie
Mellon University, 2007b. CMU-CS-07-129.
Joshua Dunfield and Neelakantan R. Krishnaswami. Complete and easy
bidirectional typechecking for higher-rank polymorphism. In ICFP, 2013.
arXiv:1306.6032 [cs.PL].
Joshua Dunfield and Frank Pfenning. Type assignment for intersections and
unions in call-by-value languages. In Found. Software Science and Computation Structures (FoSSaCS ’03), pages 250–266, 2003.
Joshua Dunfield and Frank Pfenning. Tridirectional typechecking. In Principles
of Programming Languages, pages 281–292, 2004.
Tim Freeman. Refinement Types for ML. PhD thesis, Carnegie Mellon University, 1994. CMU-CS-94-110.
Tim Freeman and Frank Pfenning. Refinement types for ML. In Programming
Language Design and Implementation, pages 268–277, 1991.
Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische
Zeitschrift, 39:176–210, 405–431, 1934. English translation, Investigations into
logical deduction, in M. Szabo, editor, Collected papers of Gerhard Gentzen
(North-Holland, 1969), pages 68–131.
Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining
logics. Journal of the ACM, 40(1):143–184, 1993.
Andrew Kennedy. Programming languages and dimensions. PhD thesis, University of Cambridge, 1996.
Ruud Koot and Jurriaan Hage. Type-based exception analysis for non-strict
higher-order functional languages with imprecise exception semantics. In Pro-

27

ceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, pages 127–138, 2015.
William Lovas. Refinement Types for Logical Frameworks. PhD thesis, Carnegie
Mellon University, 2010. CMU-CS-10-138.
Frank Pfenning and Carsten Schürmann. System description: Twelf—a metalogical framework for deductive systems. In Int’l Conf. Automated Deduction
(CADE-16), pages 202–206, 1999.
Brigitte Pientka and Joshua Dunfield. Beluga: A framework for programming
and reasoning with deductive systems (system description). In Int’l Joint
Conference on Automated Reasoning (IJCAR), pages 15–21, 2010.
Adam Poswolsky and Carsten Schürmann. System description: Delphin—a functional programming language for deductive systems. In Int’l Workshop on
Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP’08),
volume 228 of Electronic Notes in Theoretical Computer Science, pages 135–
141, 2009.
John C. Reynolds. Types, abstraction, and parametric polymorphism. In Information Processing 83, pages 513–523. Elsevier, 1983. http://www.cs.cmu.
edu/afs/cs/user/jcr/ftp/typesabpara.pdf.
John C. Reynolds. Design of the programming language Forsythe. Technical
Report CMU-CS-96-146, Carnegie Mellon University, 1996.
Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala. Liquid types. In Programming Language Design and Implementation, pages 159–169, 2008.
Niki Vazou, Patrick M. Rondon, and Ranjit Jhala. Abstract refinement types.
In European Symp. on Programming, pages 209–228, 2013.
Andrew K. Wright. Simple imperative polymorphism. Lisp and Symbolic Computation, 8(4):343–355, 1995.
Hongwei Xi. Dependent Types in Practical Programming. PhD thesis, Carnegie
Mellon University, 1998.
Hongwei Xi and Frank Pfenning. Dependent types in practical programming.
In Principles of Programming Languages, pages 214–227, 1999.
Noam Zeilberger. The Logical Basis of Evaluation Order and Pattern-Matching.
PhD thesis, Carnegie Mellon University, 2009. CMU-CS-09-122.

28

A

Omitted Definitions

A.1 Pattern complement and intersection

¬p Complement of a pattern under unrefined signature U
¬
¬∅
¬(x as p)
¬(p1 , p2 )

¬(p1 ⊔ p2 ) = (¬p1 ) ∩ (¬p2 )
= ∅
¬c(p) = c(¬p) ⊔ c1 ( ) ⊔ . . . ⊔ cn ( )
=
= ¬p
where constructors(U) \ {c} = {c1 , . . . , cn }
= (¬p1 , ) ⊔ ( , ¬p2 )

p1 ∩ p2 Intersection of patterns
∅∩p = p∩∅
∩p = p∩
c(p1 ) ∩ c(p2 )
c1 (p1 ) ∩ c2 (p2 )
(p1 , p2 ) ∩ c(p)

=
=
=
=
=

(p11 , p12 ) ∩ (p21 , p22 ) = (p11 ∩ p21 , p12 ∩ p22 )
∅
(p1 ⊔ p2 ) ∩ p = (p1 ∩ p) ⊔ (p2 ∩ p)
p
where p ∈
/ {∅, }
c(p1 ∩ p2 )
∅ where c1 6= c2
p ∩ (p1 ⊔ p2 ) = (p ∩ p1 ) ⊔ (p ∩ p2 )
c(p) ∩ (p1 , p2 ) = ∅
where p ∈
/ {∅, , · · · ⊔ · · · }

Fig. 13. Pattern complement and pattern intersection

29

A.2 Evaluation contexts, matching, and stepping

Evaluation contexts E ::= [ ] | E e | v E | c E | (E , e) | (v, E ) | case E of ms

p match v −→ θ Value v matches pattern p by substitution θ, i.e. [θ]p = v
match v −→ ·
pk match v −→ θ

p match v −→ θ

MatchWild

x as p match v −→ θ, v/x

for some k ∈ {1, 2}

p1 ⊔ p2 match v −→ θ
() match () −→ ·

MatchUnit

p match v −→ θ

MatchOr

c(p) match c(v) −→ θ

p1 match v1 −→ θ1

p2 match v2 −→ θ2

(p1 , p2 ) match (v1 , v2 ) −→ (θ1 , θ2 )

p match v 6→ Value v does not match pattern p
∅ match v 6→

NoMWild

p match v 6→

x as p match v 6→

p1 match v 6→
p2 match v 6→

NoMAs

p1 ⊔ p2 match v 6→

there does not exist v ′ such that v = c(v ′ )

p match v 6→

c(p) match c(v) 6→

v not a pair

(p1 , p2 ) match v 6→

MatchAs

c(p) match v 6→

NoMPairHead

Matching v,

ms 7→v e ′ ms step to e ′

pk match vk 6→

MatchPair

NoMOr

NoMConHead

v 6= ()

NoMConInner

MatchCon

() match v 6→

NoMUnit

for some k ∈ {1, 2}

(p1 , p2 ) match (v1 , v2 ) 6→

NoMPairInner

p1 match v −→ θ

StepMatch
(p1 ⇒ e1 ) | ms 7→v [θ]e1

ms 7→v e ′

StepElse
(p1 ⇒ e1 ) | ms 7→v e ′

p1 match v 6→

e 7→ e ′ e steps to e ′

(λx. e1 ) v2 7→ [v2 /x]e1
′

(declare Σ in e) 7→ e

StepDeclare

StepBeta

case v of ms 7→ e ′

e 7→ e ′

E [e] 7→ E [e ′ ]

Fig. 14. Operational semantics

ms 7→v e ′

StepContext

StepCase

30

A.3 Substitution typing

Substitution θ, applied to something well-formed under Σ; (Γ, Γ ′ ),

Σ; Γ ⊢ θ : Γ ′ replaces variables in Γ ′ to yield something well-formed under Γ
Σ; Γ ⊢ · : ·

SubstEmpty

Σ; Γ ⊢ θ : Γ ′

Σ; Γ ⊢ v : A

Σ; Γ ⊢ (θ, v/x) : (Γ ′ , x : A)

SubstVar

Fig. 15. Substitution typing

Substitution typing (Figure 15) is used to state Lemma 15 (Multiple substitution).

B
B.1

Proofs
Properties of subtyping

Lemma 6 (Reflexivity). If Σ ⊢ A type then Σ ⊢ A ≤ A.
Proof. By structural induction on A.
The case for A = 1, the case for A = A1 ∗ A2 , and the case for A = A1 → A2
are straightforward.
– Case A = s:

Use Refl and ≤Data.

Lemma 7 (Transitivity).
If Σ ⊢ A ≤ B and Σ ⊢ B ≤ C where Σ ⊢ A type and Σ ⊢ B type and Σ ⊢ C type
then Σ ⊢ A ≤ C.
Proof. By simultaneous induction on the given derivations.
– If either derivation is by ≤1, then A = B or B = C, and the other given
derivation is the desired result.
– If both derivations are by ≤∗, apply the i.h. as needed, then apply ≤∗.
– If both derivations are by ≤→, apply the i.h. as needed, then apply ≤→.
– If both derivations are by ≤Data, apply Trans, then apply ≤Data.
– If the first derivation is by ≤∧Lk , we have A = A1 ∧ A2 .
Σ ⊢ Ak ≤ B
Subderivation
Σ ⊢ Ak ≤ C
By i.h.
Σ ⊢ (A1 ∧ A2 ) ≤ C By ≤∧Lk
– If the second derivation is by ≤∧R, we have C = C1 ∧ C2 .
Σ ⊢ A≤B
Given
Σ ⊢ B ≤ C1
Subderivation
Σ ⊢ A ≤ C1
By i.h.
Σ ⊢ A ≤ C2
Similar (B ≤ C2 subderivation)
Σ ⊢ A ≤ (C1 ∧ C2 ) By ≤∧R

31

– If the first derivation D1 is by ≤∧R and the second derivation D2 is by
≤∧Lk , we have B = B1 ∧ B2 .
Σ ⊢ A ≤ Bk Subderivation of D1
Σ ⊢ Bk ≤ C Subderivation of D2
Σ ⊢ A ≤ C By i.h.
Other combinations of concluding rules are impossible.
B.2

Subsort properties

Theorem 1 (Non-adjacent preservation).
If Σ2 preserves subsorting of Σ1 and Σ3 preserves subsorting of Σ1
and Σ2 and Σ3 are non-adjacent then Σ3 preserves subsorting of (Σ1 , Σ2 ).
Proof. Suppose Σ1 , Σ2 , Σ3 ⊢ s  t where s, t ∈ dom(Σ1 , Σ2 ). Following Definition
1, we need to show that Σ1 , Σ2 ⊢ s  t.
Every derivation of a subsorting judgment is essentially a finite path in a
directed graph from the subsort to the supersort. The path from s to t must
pass through edges (subsortings) in Σ3 a finite number of times, say n times.
Proceed by induction on n:
– If n = 0, the path from s to t does not pass through Σ3 at all, so we can
simply replace (Σ1 , Σ2 , Σ3 ) in the given derivation with (Σ1 , Σ2 ).
– If n > 0, choose the last Σ3 segment in the path:
s  . . .  s1  t3  . . .  t3′ s1′  . . .  t
{z
}
|
subsort edges in Σ3

Here, t3 , t3′ ∈ dom(Σ3 ). Now consider the vertices (sorts) s1 and s1′ . These
sorts must be in dom(Σ1 , Σ2 ). Since Σ2 and Σ3 are non-adjacent, neither s1
nor s1′ can be in dom(Σ2 ). Therefore, s1 , s1′ ∈ dom(Σ1 ).
All the edges from t3 to t3′ are in Σ3 , so from Σ1 , Σ2 , Σ3 ⊢ s1  s1′ we get
Σ1 , Σ3 ⊢ s1  s1′ .
It is given that Σ3 preserves subsorting of Σ1 . Therefore, Σ1 ⊢ s1  s1′ ,
yielding a path
s  . . .  s1  . . .  s1′  . . .  t
{z
}
|
subsort edges in Σ1

This path has one less Σ3 segment than the one we started with, so the result
follows by induction.
B.3

Strengthening, weakening, and substitution

Weakening of the supporting judgments
Lemma 8 (Weakening (lowest level)). Given Σ and Σ ′ such that Σ ′ ≤sig Σ:

32

(i)
(ii)
(iii)
(iv)
(v)
(vi)

If
If
If
If
If
If

Σ ⊢ A type then Σ ′ ⊢ A type.
Σ ⊢ s1  s2 then Σ ′ ⊢ s1  s2 .
Σ ⊢ A ≤ B then Σ ′ ⊢ A ≤ B.
Σ ⊢ c : A → s then Σ ′ ⊢ c : A → s.
Σ ⊢ A ❁ τ then Σ ′ ⊢ A ❁ τ.
Σ ⊢ c : C contype then Σ ′ ⊢ c : C contype.

In part (iii), the resulting derivation has the same size (number of horizontal
lines) as the given derivation.
Proof. For each part, by induction on the given derivation, assuming lowernumbered parts.
Part (i): All cases are straightforward.
Part (ii), subsorting: All 3 cases (Assum, Refl and Trans) are straightforward.
Part (iii), subtyping: All cases are straightforward; the case for ≤Data uses
part (ii) of the i.h.
Part (iv), constructor typing: There is one case, ConArr, which uses the i.h.
(ii).
Part (v), A ❁ τ: Straightforward.
Part (vi), constructor type well-formedness: use part (i).
Lemma 9 (Weakening ‘SafeConAt’).
If Σ, Σ ′ ; ShKi ⊢ c : A → s safe at t then Σ, Ω, Σ ′; ShKi ⊢ c : A → s safe at t.
Proof. By inversion on SafeConAt and applying Lemma 8 (Weakening (lowest
level)) parts (ii), (ii), and (iii), and then applying SafeConAt.
Lemma 10 (Supersorting ‘SafeConAt’).
If Σ; ShKi ⊢ c : A → s safe at t ′ and Σ, ShKi ⊢ t ′ t then Σ; ShKi ⊢ c : A → s safe at t.
Proof. Some of the premises of SafeConAt do not involve t ′ at all, so we can
reuse them directly. The exception is the premise Σ, ShKi ⊢ s ′  t ′ . Applying
Trans gives Σ, ShKi ⊢ s ′  t. Now we can apply SafeConAt.
Theorem 2 (Weakening ‘safe’).
If (Σ, Σ ′ ) sig and (Σ, Ω) sig and dom(Σ ′ ) ∩ dom(Ω) = ∅
and dom(Σ, Ω, Σ ′ ) ∩ S = ∅ and K does not mention anything in dom(Ω)
and ShKi preserves subsorting for (Σ, Σ ′ )
and (c : A → s) ∈ K and Σ, Σ ′ ; ShKi ⊢ c : A → s safe
then Σ, Ω, Σ ′ ; ShKi ⊢ c : A → s safe.

Proof.

Σ, Σ ′ ; ShKi
1
s
Σ, Σ ′ , ShKi
Σ, Σ ′ ; ShKi
2 Σ, Σ ′ , ShKi

⊢
∈
⊢
⊢
⊢

c : A→s
S
c : A→s
c : A→s
c : A→s

safe

Given
By inversion on BlockCon

contype ′′
safe at t ′′ for all t ∈ dom(Σ, Σ ′ ) such that . . .
contype By Lemma 8 (Weakening (lowest level)) (vi)

Suppose that t ∈ dom(Σ, Ω, Σ ′ ) and Σ, Ω, Σ ′ , ShKi ⊢ s  t.

33

– Case t ∈ dom(Σ, Σ ′ ):
Σ, Ω, Σ ′, ShKi ⊢ s  t Assumption
It is given that ShKi preserves subsorting for (Σ, Σ ′ ). By inversion on (Σ, Σ ′ ) sig,
signature Σ ′ preserves subsorting for Σ. Combining these, we have that
(Σ ′ , ShKi) preserves subsorting for Σ.
It is also given that K does not mention anything in dom(Ω), and by inversion
on (Σ, Ω) sig (and using dom(Σ, Ω, Σ ′ ) ∩ S = ∅), we know that Ω does not
mention anything in S; therefore, ShKi and Ω are non-adjacent (Definition
2).
By Theorem 1 with Σ1 = Σ and Σ2 = (Σ ′ , ShKi) and Σ3 = Ω, we have that
Ω preserves subsorting of (Σ, Σ ′ , ShKi).
Preservation of subsorting is invariant under signature permutation, so Ω can
be permuted leftward: Σ, Ω, Σ ′, ShKi ⊢ s  t if and only if Σ, Σ ′ , ShKi ⊢ s  t,
and we assumed the former judgment. Therefore:
Σ, Σ ′ , ShKi ⊢ s  t
This is the guard of one of the premises under the above “for all”. Therefore:
Σ, Σ ′ ; ShKi ⊢ c : A → s safe at t
Σ, Ω, Σ ′; ShKi ⊢ c : A → s safe at t By Lemma 9 (Weakening ‘SafeConAt’)
– Case t ∈ dom(Ω):
Here we have Σ, Ω, Σ ′ , ShKi ⊢ s  t.
It is given that K does not mention any sorts in dom(Ω). Therefore, s 
t must have been derived transitively: there must exist another sort s ′ ∈
dom(Σ, Σ ′ ) ∪ S such that s  s ′ and s ′  t. Using the reasoning in the
subcase for when t ∈ dom(Σ, Σ ′ ), we get
Σ, Ω, Σ ′; ShKi ⊢ c : A → s safe at s ′
Σ, Ω, Σ ′; ShKi ⊢ c : A → s safe at t By Lemma 10 (Supersorting ‘SafeConAt’)
This shows the “for all” part of BlockCon. Together with “1” and “2” above, we
can apply BlockCon:
Σ, Ω, Σ ′; ShKi ⊢ c : A → s safe By BlockCon
Theorem 3 (Signature Interleaving).
If (Σ, Σ ′ ) sig and (Σ, Ω) sig and dom(Σ ′ ) ∩ dom(Ω) = ∅ then (Σ, Ω, Σ ′ ) sig.

Proof. By induction on Σ ′ .
If Σ ′ = ·, then we already have our result.
Otherwise, Σ ′ = (Σ0′ , ShKi).

34

(Σ, Σ0′ , ShKi) sig
Above
(Σ, Σ0′ ) sig
By inversion on SigBlock
′
′′
S ∩ dom(Σ, Σ0 ) = ∅
′
′
(Σ, Σ0 ⊢ |dom(Σ,Σ0′ ) ) = (Σ, Σ0 , ShKi ⊢ |dom(Σ,Σ0′ ) ) ′′ [Preservation]
′′
Σ, Σ0′ ; ShKi ⊢ c : A → s safe
for all (c : A → s) ∈ K
1
dom(Σ ′ )
dom(Σ0′ , ShKi)

dom(Σ0′ ) ∪ S
S
S
2
S

(Σ, Ω, Σ0′ ) sig
∩
∩
∩
∩
∩
∩

By i.h.

dom(Ω) = ∅
dom(Ω) = ∅
dom(Ω) = ∅
dom(Ω) = ∅
dom(Σ, Σ0′ ) = ∅
dom(Σ, Ω, Σ0′ ) = ∅

Given
Σ ′ = (Σ0′ , ShKi)
By def. of dom(−)
By a property of ∩ and ∪
Above
By def. of dom(−) and a property of ∩

We still need to prove the following:
3 (Σ, Ω, Σ0′ ⊢ |dom(Σ,Ω,Σ0′ ) ) = (Σ, Ω, Σ0′ , ShKi ⊢ |dom(Σ,Ω,Σ0′ ) ) To be proved
4 Σ, Ω, Σ0′ ; ShKi ⊢ c : A → s safe To be proved for all (c : A → s) ∈ K
(Σ, Ω, Σ0′ , ShKi) sig

By SigBlock (1, 2, 3, 4)

– Proof of 3:
We have (Σ, Ω) sig.
Elaborating equation 3, we need to show, for all t1 , t2 ∈ dom(Σ, Ω, Σ0′ ), that
each direction holds:
• (a) If Σ, Ω, Σ0′ ⊢ t1  t2 then Σ, Ω, Σ0′ , ShKi ⊢ t1  t2 .
• (b) If Σ, Ω, Σ0′ , ShKi ⊢ t1  t2 then Σ, Ω, Σ0′ ⊢ t1  t2 .
For direction (a), Lemma 8 (Weakening (lowest level)) (ii) suffices.
For direction (b):
We have (Σ, Σ0′ , ShKi) sig.
By inversion on SigBlock, the block K preserves subsorting of the signature
(Σ, Σ0′ ).
By inversion on BlockSubsort, none of the subsortings added by K are in
dom(Ω), and none of the subsortings added by Ω are in S. That is, ShKi and
Ω are non-adjacent.
By Theorem 1 with Σ1 = (Σ, Σ0′ ) and Σ2 = Ω and Σ3 = ShKi, we have
that Σ3 preserves subsorting of (Σ1 , Σ2 ), that is, ShKi preserves subsorting
of (Σ, Σ0′ , Ω).
Preservation of subsorting is invariant under signature permutation, so ShKi
preserves subsorting of (Σ, Ω, Σ0′ ). By Definition 1, (b) holds.
– Proof of 4:
Most of the work will be done by Theorem 2. We need to show all of that
theorem’s conditions. All of our meta-variables match up with the statement
of the lemma, except that our Σ0′ will play the role of Σ ′ .

35

• (Σ, Σ0′ ) sig: Above.
• (Σ, Ω) sig: Given.
• dom(Σ0′ ) ∩ dom(Ω) = ∅: Follows from dom(Σ ′ ) ∩ dom(Ω) = ∅, which
was given.
• dom(Σ, Ω, Σ0′ ) ∩ S = ∅: This is “2”, shown above.
• K does not mention anything in dom(Ω):
If K mentioned anything in dom(Ω), it would contradict the premise of
BlockSubsort and/or the contype premise of BlockCon.
• K preserves subsorting for (Σ, Σ0′ ): This is “Preservation”, shown above.
• (c : A → s) ∈ K: Assumption.
• Σ, Σ0′ ; ShKi ⊢ c : A → s safe: Above.
The judgment marked 4 follows by Theorem 2.
Now we can apply SigBlock.
(Σ, Ω, Σ0′ , ShKi) sig By SigBlock (1, 2, 3, 4)
Intersect strengthening
Lemma 11 (Properties of stronger contexts).
(i) Reflexivity: For all contexts Γ , we have Σ ⊢ Γ ≤ctx Γ .
(ii) Transitivity: If Σ ⊢ Γ ′′ ≤ctx Γ ′ and Σ ⊢ Γ ′ ≤ctx Γ then Σ ⊢ Γ ′′ ≤ctx Γ .
(iii) Concatenation: If Σ ⊢ Γ1′ ≤ctx Γ1 and Σ ⊢ Γ2′ ≤ctx Γ2 then
Σ ⊢ (Γ1′ , Γ2′ ) ≤ctx (Γ1 , Γ2 ).
Proof. Part (i): By induction on Γ , using Lemma 6 (Reflexivity).
Part (ii): Use Lemma 7 (Transitivity).
Part (iii): By induction on Γ2 .
Lemma 12 (Constructor).
If Σ sig and Σ+ sig and Σ+ ≤sig Σ
+
+
and (c : A+
c → sc ) ∈ Σ+ and Σ+ ⊢ sc  s and s ∈ dom(Σ)
+
then (c : Ac → sc ) ∈ Σ and Σ+ ⊢ s+
c  sc and Σ+ ⊢ Ac ≤ Ac .

+
+
+
Proof. If (c : A+
c → sc ) ∈ Σ, then: Let Ac = Ac and sc = sc . By Lemma 6
+
(Reflexivity), Σ+ ⊢ Ac ≤ Ac .
Otherwise, by inversion on Σ+ sig, there is a derivation using BlockCon
that says that, for some Σ1 such that Σ = (Σ1 , Σ2 ), we have Σ1 ; ShKi ⊢ c :
+
+
A+
c → sc safe at t for all t ∈ dom(Σ1 ) such that Σ1 , ShKi ⊢ sc  t.
+
We have Σ+ ⊢ sc  s. By well-formedness of the given signatures, all blocks
preserve subsorting of previously-defined sorts. Therefore

Σ1 , ShKi ⊢ s+
c s
Instantiating the above t with s gives
+
Σ1 ; ShKi ⊢ c : A+
c → sc safe at s

36

(c : Ac → sc )
Σ1 , ShKi
Σ1 , ShKi
Σ1 , ShKi

∈
⊢
⊢
⊢

Σ1
By inversion on SafeConAt
′′
sc  s
′′
s+
c  sc
+
′′
Ac ≤ Ac

Σ + ⊢ s+
By Lemma 8 (Weakening (lowest level)) (ii)
c  sc
Σ + ⊢ A+
≤
A
By Lemma 8 (Weakening (lowest level)) (iii)
c
c
Lemma 13 (Intersect strengthening).
If Σ+ sig and Σ sig and Σ+ ≤sig Σ and Σ ⊢ A type
and Σ+ ⊢ A+ ≤ A
then Σ+ ⊢ intersect(Σ+ ⊢ A+ ; p) ≤trk intersect(Σ ⊢ A; p).
Proof. By structural induction on p.
Suppose we have

1
n
n
intersect(Σ+ ⊢ A+ ; p) = (Σ1+ ; Γ+
⊢ B1+ ), . . . , (Σn
+ ; Γ+ ⊢ B+ )
 1 1
intersect(Σ ⊢ A; p) = (Σ ; Γ ⊢ B1 ), . . . , (Σm ; Γ m ⊢ Bm )
+
+
For each track B∗+ = (Σ+
k ; Γk ⊢ Bk ) ∈ intersect(Σ+ ⊢ A+ ; p), we need to find
∗
some track B in intersect(Σ ⊢ A; p) such that B∗+ ≤trk B∗ .

– Case p = : In this case, intersect ignores the signature entirely. The result
follows by Lemma 11 (Properties of stronger contexts) (i), and the given
subtyping Σ+ ⊢ A+ ≤ A.
– Case p = (x as p0 ):
intersect(Σ+ ⊢ A+ ; p0 ) ≤trk intersect(Σ ⊢ A; p0 ) By i.h.
Suppose (Γ+′ ⊢ B+ ) ∈ intersect(Σ+ ⊢ A+ ; p0 ).
(Γ+′ , x : B+ ⊢ B+ ) ∈ intersect(Σ+ ⊢ A+ ; x as p0 ) By definition of intersect
(Γ+′

(Γ ′ ⊢ B) ∈
⊢ B+ ) ≤trk
Σ+ ⊢
Σ+ ⊢

intersect(Σ ⊢ A; p0 )
(Γ ′ ⊢ B)
Γ+′ ≤ctx Γ ′
B+ ≤ B

(Γ ′ , x : B ⊢ B) ∈ intersect(Σ ⊢ A; x as p0 )
(Γ+′ , x

: B+ ⊢ B+ ) ≤trk (Γ , x : B ⊢ B)
′

By above ≤trk
′′

From Definition 5
′′

By definition of intersect
By Definition 5

– Case p = ∅: In this case, intersect ignores the signature—and the result is
the empty set, which is, trivially, a strengthening of the empty set.
– Case p = (p1 ⊔ p2 ):
By i.h., intersect(Σ+ ⊢ A+ ; p1 ) ≤trk intersect(Σ ⊢ A; p1 ).
Similarly, intersect(Σ+ ⊢ A+ ; p2 ) ≤trk intersect(Σ ⊢ A; p2 ).
Then:

intersect(Σ+ ⊢ A+ ; p1 ) ∪ intersect(Σ+ ⊢ A+; p2 )
≤trk intersect(Σ ⊢ A; p1 ) ∪ intersect(Σ ⊢ A; p2 )

37

– Case p = (p1 ∗ p2 ):
Σ+ ⊢
Σ+ ⊢
Σ+ ⊢
1
intersect(Σ+ ⊢ A+ ; p1 ) ≤trk
intersect(Σ+ ⊢ A2+ ; p2 ) ≤trk

(A1+ ∗ A2+ ) ≤ (A1 ∗ A2 )
A1+ ≤ A1
A2+ ≤ A2
intersect(Σ ⊢ A1 ; p1 )
intersect(Σ ⊢ A2 ; p2 )

Given
By inversion on ≤∗
′′

By i.h.
By i.h.

Suppose:
1
(Γ+
⊢ B1+ ) ∈ intersect(Σ+ ⊢ A1+ ; p1 )
2
(Γ+
⊢ B2+ ) ∈ intersect(Σ+ ⊢ A2+ ; p2 )

1
2
(Γ+
, Γ+
⊢ B1+ ∗ B2+ ) ∈ intersect(Σ+ ⊢ A1 ∗ A2 ; (p1 , p2 )) By definition of intersect

(Γ 1 ⊢ B1 ) ∈
⊢ B1+ ) ≤trk
Σ+ ⊢
Σ+ ⊢

1
(Γ+

intersect(Σ ⊢ A1 ; p1 )
(Γ 1 ⊢ B1 )
1
Γ+
≤ctx Γ 1
1
B+ ≤ B1

2
Σ+ ⊢ Γ+
≤ctx Γ 2
2
Σ+ ⊢ B+ ≤ B2

By above ≤trk
′′

From Definition 5
′′

Similar, with 2 substituted for 1
′′

1
2
Σ+ ⊢ (Γ+
, Γ+
) ≤ctx (Γ 1 , Γ 2 ) By Lemma 11 (iii)
1
Σ+ ⊢ (B+ ∗ B2+ ) ≤ (B1 ∗ B2 ) By ≤∗

(Γ 1 , Γ 2 ⊢ (B1 ∗ B2 )) ∈ intersect(Σ ⊢ A1 ∗ A2 ; (p1 , p2 )) By definition of intersect
2
1
⊢ B1+ ∗ B2+ ) ≤trk (Γ 1 , Γ 2 ⊢ B1 ∗ B2 )
, Γ+
(Γ+

– Case p = c(p0 ):
+
(c : A+
c → sc )
Σ+
Σ
s

∈
⊢
⊢
∈

By Definition 5

+
+
Suppose c : (A+
c → sc ) ∈ Σ+ where Σ+ ⊢ sc  s.

Σ+
s+
c s
s type
dom(Σ)

Above
Above
Given
By inversion on WfTypeSort

Σ+ sig
Given
Σ sig
Given
(c : Ac → sc ) ∈ Σ
By Lemma 12 (Constructor)
′′

s
Σ + ⊢ s+
c
c
′′
Σ + ⊢ A+
c ≤ Ac
intersect(Σ+ ⊢ A+
c ; p0 ) ≤trk intersect(Σ ⊢ Ac ; p0 ) By i.h.
′
Suppose (Γ+′ ⊢ B+
) ∈ intersect(Σ+ ⊢ A+
c ; p0 ).

38

(Γ ′ ⊢ B ′ ) ∈
≤trk
Σ+ ⊢
Σ ⊢

′
(Γ+′ ⊢ B+
)

intersect(Σ ⊢ Ac ; p0 )
(Γ ′ ⊢ B ′ )
Γ+′ ≤ctx Γ ′
′
B+
≤ B′

By above ≤trk
′′

By Definition 5
′′

Σ+ ⊢ Γ+′ ≤ctx Γ ′
Σ + ⊢ s+
c  sc
Σ + ⊢ s+
c ≤ sc

Above
Above
By ≤Data

′
Σ+ ⊢ (Γ+′ ⊢ s+
c ) ≤trk (Γ ⊢ sc ) By Definition 5

Weakening of the main judgments
Theorem 4 (Weakening).
If (Σ, Σ ′ ) sig, (Σ, Ω) sig, dom(Σ ′ ) ∩ dom(Ω) = ∅ and Σ, Ω, Σ ′ ⊢ Γ + ≤ctx Γ then
(1) If Σ, Σ ′ ; Γ ⊢ e : A then Σ, Ω, Σ ′ ; Γ + ⊢ e : A.
(2) If Σ, Σ ′ ; Γ ⊢ θ : Γ ′ then Σ, Ω, Σ ′; Γ + ⊢ θ : Γ ′ .
(3) If Σ, Σ ′ ; Γ ; p : A ⊢ ms : D then Σ, Ω, Σ ′ ; Γ + ; p : A ⊢ ms : D.
Proof. For each part, by induction on the height of the given derivation.
Part (1), expression typing:
– Var: apply Var.
– Sub: apply the i.h. (1) and Lemma 8 (Weakening (lowest level)) (iii).
– 1I, →I, →E, ∗I, DataI: straightforward. The DataI case uses Lemma 8 (Weakening (lowest level)) (iv).
– Case Σ, Σ ′ ; Γ ⊢ e : B
Σ, Σ ′ ; Γ ; : B ⊢ ms : A
DataE

Σ, Σ ′ ; Γ ⊢ (case e of ms) : A
Σ, Σ ′ ; Γ ⊢ e : B
Σ, Ω, Σ ′ ; Γ ⊢ e : B
Σ, Σ ′ ; Γ ;
Σ, Ω, Σ ′; Γ + ;

Subderivation
By i.h. (1)

: B ⊢ ms : A Subderivation
: B ⊢ ms : A By i.h. (3)

Σ, Σ ′ ; Γ ⊢ (case e of ms) : A By DataE
– Case (Σ, Σ ′ , Σ ′′ ) sig
Σ, Σ ′ ⊢ A type
Σ, Σ ′ , Σ ′′ ; Γ ⊢ e0 : A
Declare
Σ, Σ ′ ; Γ ⊢ (declare Σ ′′ in e0 ) : A
(Σ, Σ ′ , Σ ′′ ) sig
(Σ, Ω) sig
dom(Σ ′ ) ∩ dom(Ω)
dom(Σ ′′ ) ∩ dom(Ω)

′
dom(Σ ) ∪ dom(Σ ′′ ) ∩ dom(Ω)
dom(Σ ′ , Σ ′′ ) ∩ dom(Ω)

=
=
=
=

∅
∅
∅
∅

Subderivation
Given
Given
By renaming dom(Σ ′′ )
By set theory
By def. of dom(−)

39

(Σ, Ω, Σ ′ ) sig

1
2

By Theorem 3

Σ, Σ ′ ⊢ A type Subderivation
Σ, Ω, Σ ′ ⊢ A type By Lemma 8 (Weakening (lowest level)) (i)

Σ, Σ ′ , Σ ′′ ; Γ ⊢ e0 : A
3 Σ, Ω, Σ ′, Σ ′′ ; Γ ⊢ e0 : A

Subderivation
By i.h. (1)

Σ, Ω, Σ ′; Γ ⊢ (declare Σ ′′ in e0 ) : A By Declare on 1, 2, 3
Part (2), substitution typing: In the SubstVar case, use part (1).
Part (3), where a derivation of Σ, Σ ′ ; Γ ; p : B ⊢ ms : D is given:
– Case intersect(Σ, Σ ′ ⊢ A; p) = ∅
TypeMsEmpty
Σ, Σ ′ ; Γ ; p : A ⊢ ∅ : D
Suppose intersect(Σ, Ω, Σ ′ ⊢ A+ ; p) 6= ∅.
By Lemma 13 (Intersect strengthening), for each track in intersect(Σ, Ω, Σ ′ ⊢
A+ ; p) there exists a track in intersect(Σ, Σ ′ ⊢ A; p). But we have as a
premise that intersect(Σ, Σ ′ ⊢ A; p) = ∅, a contradiction.
Therefore intersect(Σ, Ω, Σ ′ ⊢ A+ ; p) = ∅.
The result follows by TypeMsEmpty.
– Case
′

Σ, Σ ⊢ A ❁ τ
U ⊢ p1 : τ

for all (Γ ′ ⊢ B)
∈ intersect(Σ ⊢ A; p ∩ p1 ):
Σ; Γ, Γ ′ ⊢ e1 : D

Σ, Σ ′ ; Γ ; (p ∩ ¬p1 ) : A ⊢ ms : D

TypeMs
Σ, Σ ′ ; Γ ; p : A ⊢ (p1 ⇒ e1 ) | ms : D

Σ, Σ ′ ⊢ A ❁ τ Subderivation
Σ, Ω, Σ ′ ⊢ A ❁ τ By Lemma 8 (Weakening (lowest level)) (vi)
U ⊢ p1 : τ Subderivation
(Σ, Ω, Σ ′) ≤sig (Σ, Σ ′ )
By Definition 3
′
+
Σ, Ω, Σ ⊢ Γ ≤ctx Γ Given
Σ, Σ ′ ⊢ A type
Given
By Lemma 13,
intersect(Σ, Ω, Σ ′ ⊢ A; p ∩ p1 ) ≤trk intersect(Σ, Σ ′ ⊢ A; p ∩ p1 )
By Definition 5, each track in intersect(Σ, Ω, Σ ′ ⊢ A; p ∩ p1 ) is stronger than
some track in intersect(Σ, Σ ′ ⊢ A; p ∩ p1 ).
That is, if (Γ0+ ⊢ B+ ) ∈ intersect(Σ, Ω, Σ ′ ⊢ A; p ∩ p1 ), then
Σ, Ω, Σ ′ ⊢ (Γ0+ ⊢ B+ ) ≤trk (Γ0 ⊢ B)
where (Γ0 ⊢ B) ∈ intersect(Σ, Σ ′ ⊢ A; p ∩ p1 ).

40

Σ, Σ ′ ; Γ, Γ0 ⊢ e1 : D

Subderivation

Σ, Ω, Σ ′ ⊢ Γ ≤ctx Γ
By Lemma 11 (i)
Σ, Ω, Σ ′ ⊢ Γ0+ ≤ctx Γ0
By above (Γ0+ ⊢ B+ ) ≤trk (Γ0 ⊢ B)
+
Σ, Ω, Σ ′ ⊢ (Γ, Γ0 ) ≤ctx (Γ, Γ0 ) By Lemma 11 (iii)
Σ, Ω, Σ ′; Γ, Γ0+ ⊢ e1 : D
By i.h.
Since the above holds for all tracks, this gives the necessary “for all” premises.
Then:
Σ, Σ ′ ; Γ ; (p ∩ ¬p1 ) : A ⊢ ms : D
Subderivation
Σ, Ω, Σ ′; Γ + ; (p ∩ ¬p1 ) : A ⊢ ms : D
By i.h.

Σ, Ω, Σ ′ ; Γ + ; p : A ⊢ (p1 ⇒ e1 ) | ms : D By TypeMs
Lemma 14 (Value substitution). Suppose Σ; ΓL , ΓR ⊢ v : A.
(i) If Σ; ΓL , x : A, ΓR ⊢ e : B then Σ; ΓL , ΓR ⊢ [v/x]e : B.
(ii) If Σ; ΓL , x : A, ΓR ; p : B ⊢ ms : D then Σ; ΓL , ΓR ; p : B ⊢ [v/x]ms : D.
Proof. In each part, by induction on the derivation specific to that part.
For part (i), in the Var case, we have Σ; ΓL , ΓR ⊢ v : A, and v = [v/x]x. In all
other cases, use the i.h. on each premise, then apply the same rule. (For DataE,
use part (ii).)
For part (ii), we have two cases:
– Case TypeMs: The intersect function does not depend on the typing context, so we get the same set of tracks. Apply the i.h. (i) to each typing
subderivation and the i.h. (ii) to the last subderivation.
– Case TypeMsEmpty: This rule does not depend on the typing context at
all, so we just apply it.
Lemma 15 (Multiple substitution).
If Σ; Γ, Γ ′ ⊢ e : B and Σ; Γ ⊢ θ : Γ ′ then Σ; Γ ⊢ [θ]e : B.
Proof. By induction on the derivation of Σ; Γ ⊢ θ : Γ ′ . In the SubstEmpty case,
apply the equality [θ]e = [·]e = e. In the SubstVar case, use the i.h. and Lemma
14 (Value substitution).
B.4

Value inversion

A value inversion (or canonical forms) lemma holds:
Lemma 16 (Inversion). Suppose Σ; · ⊢ v : B.
(1) If Σ ⊢ B ≤ s then there exist c and v ′ such that v = c(v ′ )
and (c : A → t) ∈ Σ and Σ ⊢ t  s and Σ; · ⊢ v ′ : A.
(2) If Σ ⊢ B ≤ (A1 → A2 )
then v = λx. e and Σ; ·, x : B1 ⊢ e : A2 where Σ ⊢ A1 ≤ B1 .
(3) If Σ ⊢ B ≤ 1 then v = ().

41

(4) If Σ ⊢ B ≤ (A1 ∗ A2 ) then v = (v1 , v2 ) where Σ; · ⊢ v1 : A1 and Σ; · ⊢ v2 : A2 .
Proof. By induction on the given derivation.
– Part (1):
We have Σ ⊢ B ≤ s. By inversion on subtyping, B has the form B∗ ::= t |
B∗1 ∧ B∗2 . Thus, the only possible cases are Sub, ∧I, and DataI.
(Declare is impossible because a declare is not a value.)
• Case Σ; · ⊢ v : B ′
Σ ⊢ B′ ≤ B
Sub
Σ; · ⊢ v : B
Σ
Σ; ·
Σ
Σ

⊢
⊢
⊢
⊢

B′ ≤ B
v : B′
B≤s
B′ ≤ s

Subderivation
Subderivation
Given
By Lemma 7 (Transitivity)

The result follows by i.h.
• Case Σ; · ⊢ v : B
Σ; · ⊢ v : B2
1
∧I
Σ; · ⊢ v : (B1 ∧ B2 )
Σ ⊢ (B1 ∧ B2 ) ≤ s Given
Σ ⊢ Bk ≤ s
By inversion (≤∧Lk )
Σ; · ⊢ v : Bk
Subderivation
The result follows by i.h.
• Case Σ ⊢ c : A → s
Σ; · ⊢ v ′ : A
0
DataI
′
Σ; · ⊢ c(v ) : s0
| {z }
v

v
Σ; ·
Σ
(c : A → t)
Σ
Σ
Σ
Σ

=
⊢
⊢
∈
⊢
⊢
⊢
⊢

′

c(v )
v′ : A
c : A → s0
Σ
t  s0
s0 ≤ s
s0  s
ts

Above
Subderivation
Subderivation
By inversion (ConArr)
′′

Given
By inversion (≤Data)
By Trans

– Part (2):
The only possible cases are Sub, ∧I, and →I.
• Cases Sub, ∧I: Similar to the respective cases for part (1).
• Case

Σ; Γ, x : B1 ⊢ e : B2
→I
Σ; Γ ⊢ λx.
| {z e} : (B1 → B2 )
v

42

Σ
Σ
Σ
Σ; Γ, x : B1
Σ; Γ, x : B1

⊢
⊢
⊢
⊢
⊢

(B1 → B2 ) ≤ (A1 → A2 )
A1 ≤ B1
B2 ≤ A2
e : B2
e : A2

Given
By inversion
′′

Subderivation
By Sub

– Part (3): Similar to part (2), but with 1I instead of →I.
– Part (4): Similar to part (2), but with ∗I instead of →I.
B.5

Operational semantics lemmas

Lemma 17. If e is a value then there exists no e ′ such that e 7→ e ′ .
Proof. By induction on e.

B.6

Type preservation and progress

Lemma 18 (Pattern intersection).
If p1 match v −→ θ1 and p2 match v −→ θ2 then p1 ∩ p2 match v −→ θ.
Proof. By mutual induction on p1 and p2 .
– Case p1 = ∅ or p2 = ∅: Impossible: ∅ match v −→ . . . is not derivable.
– Case p1 = or p2 = :
Consider the p1 =
case; the p2 =
case is similar. It is given that
p2 match v −→ θ2 . We have p1 ∩ p2 = ∩ p2 = p2 , so p1 ∩ p2 match v −→
θ (letting θ = θ2 ).
– Case p1 = p11 ⊔ p12 :
p11 ⊔ p12 match v −→ θ1 Given
By inversion (MatchOr), either p11 or p12 is matched. Suppose the former;
the latter is similar.
p11 match v −→ θ1
By inversion (MatchOr)
p11 ∩ p2 match v −→ θ
By i.h.
(p11 ∩ p2 ) ⊔ (p12 ∩ p2 ) match v −→ θ
By MatchOr
(p11 ⊔ p12 ) ∩ p2 = (p11 ∩ p2 ) ⊔ (p12 ∩ p2 ) By def. of ∩
p1 ∩ p2 match v −→ θ
By above equality
– Case p2 = p21 ⊔ p22 : Similar to the previous case.
– Case p1 = c(p1′ ):
By inversion on c(p1′ ) match v −→ θ1 , we have v = c(v ′ ) and p1′ match v ′ −→
θ1 .
We already dealt with the cases for p2 being ∅, or a ⊔. So by inversion on
p2 match c(v ′ ) −→ θ2 , we have p2 = c(p2′ ) and p2′ match v ′ −→ θ2 .
By the definition of ∩, we have c(p1′ ) ∩ c(p2′ ) = c(p1′ ∩ p2′ ). By i.h.,
p1′ ∩ p2′ match v ′ −→ θ ′ .
By MatchCon, c(p1′ ∩ p2′ ) match c(v ′ ) −→ θ ′ .

43

– Case p1 = (p11 , p12 ):
By inversion on (p11 , p12 ) match v −→ θ1 , we have v = (v1 , v2 ) and
p11 match v1 −→ θ11 and p12 match v2 −→ θ12 where θ1 = θ11 ◦ θ12 .
We already dealt with the cases for p2 being ∅,
or a ⊔. So by inversion on p2 match (v1 , v2 ) −→ θ2 , we have p21 match v1 −→ θ21 and
p22 match v2 −→ θ22 where θ2 = θ21 ◦ θ22 .
By the definition of ∩, we have (p11 , p12 ) ∩ (p21 , p22 )) = (p11 ∩ p21 , p21 ∩
p22 ).
By i.h., p11 ∩ p21 match v1 −→ θ1′ . By i.h., p12 ∩ p22 match v2 −→ θ2′ .
By MatchCon, (p11 ∩ p21 , p21 ∩ p22 ) match c(v ′ ) −→ θ1′ ◦ θ2′ .
Lemma 19 (Excluded middle for matching).
If p match v 6→ then there exists no θ s.t. p match v −→ θ.
Proof. By induction on the given derivation of p match v 6→.
In all cases, at most one match rule could plausibly be applied, e.g. for
NoMAs, only MatchAs has a conclusion of the right form. In the NoMWild case,
where p = ∅, no match rule has a conclusion of the right form.
– Case
∅ match v 6→

NoMWild

The match rules are directed by the syntax of the pattern, and there is no
match rule with ∅ in its conclusion.
– Case

p0 match v 6→
NoMAs
x as p0 match v 6→

The only possibly applicable rule is MatchAs, but by i.h., there exists no θ
such that p0 match v −→ θ.
– Case p match v 6→
p2 match v 6→
1
NoMOr
p1 ⊔ p2 match v 6→

By i.h., neither p1 match v 6→ θ1 nor p2 match v 6→ θ2 , so whether we choose
k = 1 or k = 2, we can’t apply MatchOr.
– Cases NoMConHead, NoMConInner, NoMUnit, NoMPairHead, NoMPairInner:
Straightforward, using the i.h. as needed.
Lemma 20 (Choice).
If Σ sig and U ⊢ p : τ and Σ; · ⊢ v : A and Σ ⊢ A ❁ τ
then either (1) p match v −→ θ or (2) p match v 6→ and ¬p match v −→ ·.
Proof. By structural induction on p.
– Case p-Wild:

By MatchWild, p match v −→ ·.

44

– Case p-As:
We have p = (x as p0 ). By i.h., either p0 match v −→ θ, or
p0 match v 6→ and ¬p0 match v −→ ·.
If p0 match v −→ θ, then by MatchAs, x as p0 match v −→ θ.
Otherwise, by NoMAs, x as p0 match v 6→. Above, we obtained ¬p0 match v −→
·; by the definition of ¬, we have ¬(x as p0 ) = ¬p0 , so ¬(x as p0 ) match v −→
·.
– Case p-Empty: By NoMWild, p match v 6→. By the definition of ¬, we have
¬∅ = .
By MatchWild, match v −→ ·.
– Case Σ ⊢ p : τ
Σ⊢p :τ
1

2

Σ ⊢ (p1 ⊔ p2 ) : τ

p-Or

If the i.h. gives p1 match v −→ θ, then by MatchOr, p1 ⊔ p2 match v −→ θ.
Otherwise, we have p1 match v 6→ and ¬p1 match v −→ θ1′ :
• If the i.h. on Σ ⊢ p2 : τ gives p2 match v −→ θ, then by MatchOr,
p1 ⊔ p2 match v −→ θ.
• Otherwise, we have p2 match v 6→ and ¬p2 match v −→ θ2′ .
By NoMOr, p1 ⊔ p2 match v 6→.
By the definition of ¬, we have ¬(p1 ⊔ p2 ) = (¬p1 ) ∩ (¬p2 ).
By Lemma 18 (Pattern intersection), (¬p1 ) ∩ (¬p2 ) match v −→ ·,
which was to be shown.
– Case p-Unit:
By Lemma 16 (Inversion) (3), v = ().
By MatchUnit, () match () −→ ·.
– Case p-Pair:
We have p = (p1 , p2 ) and τ = τ1 ∗ τ2 .
By Lemma 16 (Inversion) (4), v = (v1 , v2 ) and Σ; · ⊢ v1 : B1 and Σ; · ⊢ v2 : B2
where Σ ⊢ B1 ≤ A1 and Σ ⊢ B2 ≤ A2 .
If the i.h. gives (1), then we have p1 match v1 −→ θ1 :
• By i.h. (p2 ), we have either (1) p2 match v2 −→ θ2 or (2) p2 match v2 6→
and ¬p2 match v2 −→ θ2′ .
If (1), apply MatchPair.
If (2), then: By NoMPairInner, (p1 , p2 ) match v 6→.
By MatchWild and MatchPair, ( , ¬p2 ) match v −→ θ2′ . By MatchOr,
(¬p1 , ) ⊔ ( , ¬p2 ) match v −→ θ2′ . By the definition of ¬, this is
¬(p1 , p2 ) match (v1 , v2 ) −→ θ2′ .
Otherwise, we have p1 match v1 6→ and ¬p1 match v1 −→ θ1′ .
• By rule NoMPairInner, (p1 , p2 ) match v 6→.
By MatchWild and MatchPair, (¬p1 , ) match v −→ θ1′ .
By MatchOr, (¬p1 , ) ⊔ ( , ¬p2 ) match (v1 , v2 ) −→ θ1′ .
By the definition of ¬, this is ¬(p1 , p2 ) match (v1 , v2 ) −→ θ1′ .
– Case p-Con:
We have p = c(p0 ).
By Lemma 16 (Inversion) (1), v = c0 (v0 ) and Σ; · ⊢ v0 : A0 and (c0 :
A0 → s0 ) ∈ Σ and Σ ⊢ s0  s.

45

If c 6= c0 , then:
c(p0 ) match c0 (v0 ) 6→
match v0 −→ ·
c0 ( ) match c0 (v0 ) −→ ·
c(¬p0 ) ⊔ . . . ⊔ c0 ( ) ⊔ . . . match c0 (v0 ) −→ ·

¬ c(p0 ) match c0 (v0 ) −→ ·

By
By
By
By
By

NoMConHead
MatchWild
MatchCon
MatchOr
def. of ¬

If c = c0 , then:
U ⊢ p0 : τ 0
U ⊢ c : (τ0 → d)

1

Σ; ·
(c0 : A0 → s0 )
Σ
3
Σ
2

⊢
∈
⊢
⊢

By inversion on p-Con
′′

v0 : A0
Above
Σ
Above
c : A0 → s0 contype By inversion on Σ sig
A0 ❁ τ 0
By inversion on ContypeArr

By i.h. on (1, 2, 3), either:
• (1) p0 match v0 −→ θ:
c(p0 ) match c(v0 ) −→ θ By MatchCon
• (2) p0 match v0 6→ and ¬p0 match v0 −→ ·:
c(p0 ) match c(v0 ) 6→
c(¬p0 ) match c(v0 ) −→ ·

By NoMConInner
By MatchCon

c(¬p0 ) ⊔ c1 ( ) ⊔ . . . ⊔ cn ( ) match c(v0 ) −→ · By MatchOr

¬ c(p0 ) match c(v0 ) −→ · By def. of ¬
Theorem 5 (Intersect). If Σ sig and Σ; · ⊢ v : A and Σ ⊢ A type and p match v −→
θ and intersect(Σ ⊢ A; p) = B~∗ then there exists (Γ ′ ⊢ B) ∈ B~∗ s.t. Σ; · ⊢ v : B
and Σ; · ⊢ θ : Γ ′ where Σ ⊢ B type and Σ ⊢ B ≤ A.
Proof. By structural induction on p.
Case-analyze the clause of the definition of the intersect function:
– Case: p = :
match v −→ θ
θ = ·
B~∗ = {(·; · ⊢ A)}
Σ; · ⊢ v : A
Σ; · ⊢ v : B
· ⊢ · : Γ′
Σ ⊢ B≤A

Given
By inversion (MatchWild)
By def. of intersect
Given
B=A
By SubstEmpty (Γ ′ = ·)
By Lemma 6 (Reflexivity)

– Case: p = ∅:
We have ∅ match v −→ θ, which is not derivable: this case is impossible.

46

– Case: p = x as p0 :
x as p0 match v −→ θ Given
p0 match v −→ θ By inversion (MatchAs)
Σ; · ⊢ v : A
Given
intersect(Σ ⊢ A; x as p0 ) = B~∗

Given

Γ ′ = (Γ0′ , x : B) and (Γ0′ ⊢ B) ∈ intersect(Σ ⊢ A; p0 ) for all (Γ ′ ⊢ B) ∈ B~∗
By definition of intersect

(Γ0′

Σ; ·
⊢ B)
·
Σ

⊢
∈
⊢
⊢

v:B
B~∗
θ0 : Γ0′
B≤A

By i.h.
′′
′′
′′

·; · ⊢ (θ0 , v/x) : (Γ0′ , x : B) By SubstVar

– Case: p = p1 ⊔ p2 :
intersect(Σ ⊢ A; p1 ⊔ p2 ) = B~∗ Given
p1 ⊔ p2 match v −→ θ
Given
p1 match v −→ θ
By inversion (MatchOr) wlog
(Γ ′ ⊢ B) ∈ intersect(Σ ⊢ A; p1 ) By i.h.
′′
Σ; · ⊢ v : B
′′
Σ; · ⊢ θ : Γ ′
′′
Σ ⊢ B≤A

intersect(Σ ⊢ A; p1 ) ⊆ B~∗ By def. of intersect
(Γ ′ ⊢ B) ∈ B~∗ By a property of ∈

– Case: p = (p1 , p2 ):
Throughout this case, interpret k as universally quantified. For example,
Lemma 16 (Inversion) (4) shows both Σ; · ⊢ v1 : A1 and Σ; · ⊢ v2 : A2 .

47

(p1 , p2 ) match v −→ θ
v = (v1 , v2 )
θ = (θ1 , θ2 )
pk match vk −→ θk
Σ; · ⊢ (v1 , v2 ) : A1 ∗ A2
Σ; · ⊢ vk : Ak
(Γk ⊢ Bk )
Σ; ·
Σ; ·
Σ

∈
⊢
⊢
⊢

Given
By inversion (MatchPair)
′′
′′

Given
By Lemma 16 (Inversion) (4)

intersect(Σ ⊢ Ak ; pk )
vk : Bk
θk : Γ k
Bk ≤ Ak

By i.h.
′′
′′
′′

Σ; · ⊢ (v1 , v2 ) : B1 ∗ B2
By ∗I
Σ; · ⊢ (θ1 , θ2 ) : (Γ1 , Γ2 )
By properties of substitution
Σ ⊢ (B1 ∗ B2 ) ≤ (A1 ∗ A2 ) By ≤∗
– Case: p = c(p0 ):
c(p0 ) match v −→ θ
v = c(v0 )
p0 match v0 −→ θ
Σ; · ⊢ c(v0 ) : s
Σ; · ⊢ v0 : A0
(c : A0 → sc ) ∈ Σ
Σ ⊢ sc  s
intersect(Σ ⊢ s; c(p0 )) = B~∗
(Γ ′ ⊢ B0 )
Σ; ·
Σ; ·
Σ
Σ
Σ; Γ ′
(Γ ′ ⊢ sc )
Σ; ·
Σ; ·
Σ; ·

∈
⊢
⊢
⊢

∈
⊢
⊢
⊢
⊢
⊢

Given
By inversion (MatchCon)
′′

Given
By Lemma 16 (Inversion) (1)
′′
′′

intersect(Σ ⊢ A0 ; p0 )
v0 : B0
θ : Γ′
B0 type
B0 ≤ A0
v0 : A0

intersect(Σ ⊢ s; c(p0 ))
c(v0 ) : sc
c(v0 ) : s
θ : Γ′

Given
By def. of intersect
By i.h.
′′
′′

By ′′
By Sub

By def. of intersect
By DataI
By Sub
Above

Lemma 21 (Match preservation).
If Σ sig and Σ ⊢ A type and p match v −→ θ and Σ; ·; p : A ⊢ ms : D
and ms 7→ e ′
then Σ; · ⊢ e ′ : D.
Proof. By induction on the derivation of . . . ⊢ ms : D.
– Case TypeMsEmpty:

48

Σ; ·; p : A ⊢ ∅ : D
Given
intersect(Σ ⊢ A; p) = ∅
Subderivation
p match v −→ θ Given
By Theorem 5, there exists a track in intersect(Σ ⊢ A; p) such that certain
conditions hold. But intersect(Σ ⊢ A; p) = ∅, a contradiction. Thus, this case
is impossible.
– Case
Σ⊢A❁τ
U ⊢ p1 : τ

for all (Γ ′ ⊢ B)
∈ intersect(Σ ⊢ A; p ∩ p1 ):
Σ; ·, Γ ′ ⊢ e1 : D

Σ; ·; (p ∩ ¬p1 ) : A ⊢ ms ′ : D

TypeMs
Σ; ·; p : A ⊢ (p1 ⇒ e1 ) | ms ′ : D
{z
}
|
ms

Σ sig
U ⊢ p:τ
Σ; · ⊢ v : A
Σ ⊢ A❁τ

Given
Subderivation
Given
Subderivation

If the derivation of ms 7→ e ′ was concluded by StepMatch, then e ′ = [θ1 ]e1 .
Σ sig
Σ ⊢ v:A
Σ ⊢ A type
p match v −→ θ
p1 match v −→ θ1
(p ∩ p1 ) match v −→ θ ′
(Γ1 ⊢ B) ∈ intersect(Σ ⊢ A; p ∩ p1 )
Σ; · ⊢ v : B
Σ; · ⊢ θ ′ : Γ1

Given
Given
Given
Given
Subderivation of StepMatch
By Lemma 18 (Pattern intersection)
By Theorem 5
′′
′′

Σ; ·, Γ1 ⊢ e1 : D
Subderivation
′
Σ; · ⊢ [θ ]e1 : D By Lemma 15 (Multiple substitution)
Otherwise, the derivation was concluded by StepElse, where p1 match v 6→.
ms ′ 7→ e ′
Subderivation
Σ; ·; (p ∩ ¬p1 ) : A ⊢ ms ′ : D Subderivation
p match v −→ θ
¬p1 match v −→ ·
p ∩ (¬p1 ) match v −→ θ ′
Σ; · ⊢ e ′ : D

Given
Above
By Lemma 18 (Pattern intersection)
By i.h.

The preservation result allows for a longer signature, to model entering the
scope of a declare expression or the arms of a match. We implicitly assume that
throughout the given typing derivation, all types are well-formed under the local
signature: whenever we have a subderivation of Σ; Γ ⊢ e ′ : B, it is the case that
Σ ⊢ B type.

49

Theorem 6 (Preservation). If Σ sig and Σ; · ⊢ e : A and e 7→ e ′
then there exists Σ ′ such that Σ, Σ ′ ⊢ e ′ : A where (Σ, Σ ′ ) sig.
Proof. By induction on the derivation of Σ; · ⊢ e : A.
The rules Var, 1I, →I, and ∧I can only type values, which cannot step (Lemma
17), contradicting e 7→ e ′ : these cases are impossible.
In most cases, the conditions about Σ ′ follow directly from the i.h.
– Case →E:

We have e1 e2 7→ e ′ .

• If e1 7→ e1′ , use the i.h. on the first subderivation, Theorem 4 (v) on the
second subderivation, and apply →E.
• If e2 7→ e2′ , use the i.h. on the second subderivation, Theorem 4 (v) on
the first subderivation, then apply →E.
• If e1 = λx. e0 and e2 is a value, use Lemma 16 (Inversion) (2) on Σ; · ⊢
λx. e0 : (B → A) to get Σ; x : B ⊢ e0 : A.
Then use Lemma 14 (Value substitution) to get Σ; · ⊢ [e2 /x]e0 : A, which
was to be shown (letting Σ ′ = ·).

– Case ∗I:
Either e1 7→ e1′ or e2 7→ e2′ . Apply the i.h. to the appropriate
subderivation, use the weakening lemma on the other subderivation, and
apply ∗I.
– Case Σ; · ⊢ e : B
Σ⊢B≤A
Sub
Σ; · ⊢ e : A
Σ; ·
Σ, Σ ′ ; ·
Σ
Σ, Σ ′
Σ, Σ ′ ; ·

⊢
⊢
⊢
⊢
⊢

e:B
e′ : B
B≤A
B≤A
e′ : A

Subderivation
By i.h.
Subderivation
By Lemma 8 (Weakening (lowest level)) (iii)
By Sub

– Case Σ ⊢ c : B → s
Σ; · ⊢ e0 : B
DataI
Σ; · ⊢ c(e0 ) : |{z}
s
| {z }
e

A

By inversion on c(e0 ) 7→ e ′ we have e ′ = c(e0′ ) and e0 7→ e0′ .
Σ; · ⊢ e0 : B
Σ, Σ ′ ; · ⊢ e0′ : B

Subderivation
By i.h.

Σ ⊢ c : B → s Subderivation
Σ, Σ ′ ⊢ c : B → s By Lemma 8 (Weakening (lowest level)) (iv)
Σ, Σ ′ ⊢ c(e0′ ) : s

Subderivation

– Case Σ; · ⊢ e : B
Σ; ·; : B ⊢ ms : A
DataE
Σ; · ⊢ (case e of ms) : A

50

Σ sig
Σ ⊢ B type
match v −→ ·
Σ; ·; : B ⊢ ms : A
Σ; · ⊢ e ′ : A
case e of ms 7→ e ′

Given
By implicit assumption
By MatchWild
Subderivation
By Lemma 21 (Match preservation)
By StepCase

– Case (Σ, Σ ′ ) sig
Σ ⊢ A type
Σ, Σ ′ ; · ⊢ e0 : A
Declare
Σ; · ⊢ (declare Σ ′ in e0 ) : A
We have (declare Σ ′ in e0 ) 7→ e ′ . By inversion (StepDeclare), e ′ = e0 .
(Σ, Σ ′ ) sig
Premise
Σ, Σ ′ ; · ⊢ e0 : A Subderivation
Σ, Σ ′ ; · ⊢ e0 : A e ′ = e0

Lemma 22 (Match progress).
If Σ sig and p match v −→ θ and Σ; ·; p : A ⊢ ms : D then ms 7→ e ′ .

Proof. By induction on the derivation of . . . ⊢ ms : D.

– Case TypeMsEmpty:
By the same reasoning as in the TypeMsEmpty case of Lemma 21 (Match
preservation), this case is impossible.
– Case
Σ⊢A❁τ
U ⊢ p1 : τ

for all (Γ ′ ⊢ B)
∈ intersect(Σ ⊢ A; p ∩ p1 ):
Σ; ·, Γ ′ ⊢ e1 : D

Σ; ·; (p ∩ ¬p1 ) : A ⊢ ms ′ : D

TypeMs
Σ; ·; p : A ⊢ (p1 ⇒ e1 ) | ms ′ : D
{z
}
|
ms

Σ sig
Given
U ⊢ p:τ
Subderivation
Σ; · ⊢ v : A Given
Σ ⊢ A ❁ τ Subderivation
By Lemma 20 (Choice), either (1) p1 match v −→ θ1 , or (2) p1 match v 6→
and ¬p1 match v −→ ·.
For case (1), apply StepMatch.
For case (2), show p ∩ ¬p1 match v −→ θ ′ as in the proof of Lemma 21
(Match preservation), apply the i.h. to ms ′ , then apply StepElse.
Theorem 7 (Progress).
If Σ sig and Σ; · ⊢ e : A then e is a value or there exists e ′ such that e 7→ e ′ .
Proof. By induction on the given derivation.
– Case Var:
– Case Sub:

Impossible, because Γ is empty.
Follows by i.h. on the typing subderivation.

51

– Cases →I, ∧I, 1I: The rule requires that e is a value.
– Case →E: We have e = e1 e2 . By i.h. on the subderivation typing e1 , either
e1 steps or e1 is a value:
• If e1 steps, the result follows by StepContext.
• If e1 is a value, then by i.h. on the subderivation typing e2 , either e2
steps or e2 is a value.
In the former case, the result follows by StepContext.
In the latter case:
Σ; · ⊢ e1 : A ′ → A Subderivation
e1 is a value Above
e1 = (λx. e0 )
By Lemma 16 (Inversion) (2)
(λx. e0 ) e2 7→ [e2 /x]e0
By StepBeta

– Case ∗I: We have e = (e1 , e2 ).
By the i.h. on the subderivation typing e1 , either e1 steps or e1 is a value.
In the former case, the result follows by StepContext.
In the latter case, use the i.h. on the subderivation typing e2 . If e2 steps,
apply StepPairR. Otherwise, (e1 , e2 ) is a value.
– Case DataI: We have e = c(e0 ).
By the i.h. on the subderivation typing e0 , either e0 steps or e0 is a value.
In the former case, the result follows by StepContext.
In the latter case, c(e0 ) is a value.
– Case DataE:
We have e = case e0 of ms.
By the i.h. on the subderivation typing e0 , either e0 steps or e0 is a value.
In the former case, the result follows by StepContext.
In the latter case:
Σ sig
Given
match e0 −→ · By MatchWild
Σ; ·; : B ⊢ ms : A
Subderivation
case e0 of ms 7→ e ′
By Lemma 22 (Match progress)
– Case Declare: The result follows by StepDeclare.
B.7

Bidirectional typing: soundness and completeness

Theorem 8 (Bidirectional soundness). If Γ ⊢ e ⇐ A or Γ ⊢ e ⇒ A then
Γ ⊢ |e| : A where |e| is e with all annotations erased.
Proof. By induction on the given derivation.
In the SynAnno case, e = (e0 : As). Apply the i.h. to get Γ ⊢ |e0 | : A. Since
|(e0 : As)| = |e0 |, we have Γ ⊢ |(e0 : As)| : A, which was to be shown.
In all other cases, apply the i.h. to each subderivation and apply the type
assignment rule corresponding to the bidirectional rule (Var for SynVar, Sub for
ChkSub, and so on).
Theorem 9 (Annotatability).

If Γ ⊢ e : A then:

52

(1) There exists e⇐ such that |e⇐ | = e and Γ ⊢ e⇐ ⇐ A.
(2) There exists e⇒ such that |e⇒ | = e and Γ ⊢ e⇒ ⇒ A.
Proof. By induction on the given derivation.
For most cases: Use the i.h. on each subderivation and apply the corresponding bidirectional rule, using part (1) of the i.h. for checking premises and part
(2) for synthesizing premises. If the conclusion of the corresponding bidirectional
rule is a checking judgment, then part (1) has been shown; part (2) follows by
adding an annotation and using SynAnno. Otherwise, the conclusion of the corresponding rule is a synthesis judgment; part (2) has been shown, and applying
ChkSub gives part (1).
For the ∧I case of part (1), we have A = (A1 ∧ A2 ). The i.h. on the first
subderivation yields Γ ⊢ e1⇐ ⇐ A1 , and on the second subderivation it yields
12
2
1
Γ ⊢ e2⇐ ⇐ A2 . Let e⇐
be e with all annotations from e1⇐ and e⇐
. If e⇐
and
12
2
e⇐ have different annotations on the same subterm, then e⇐ has their union;
12
for example, if e1⇐ = (e0 : B1 ) and e2⇐ = (e0 : (B2 , B3 )) then let e⇐
= (e0 :
12
(B1 , B2 , B3 )). Applying Chk∧I gives Γ ⊢ e⇐ ⇐ (A1 ∧ A2 ), which was to be
shown.
For the ∧I case of part (2), follow part (1), then add an annotation, yielding

Γ ⊢ e12
⇐ : (A1 ∧ A2 ) ⇒ (A1 ∧ A2 )
B.8

Bidirectional typing: decidability

Lemma 23 (Decidability). Given instantiations of the meta-variables, the following judgments are decidable:
(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)

the refinement judgment Σ ⊢ A ❁ τ
the well-formedness judgments Σ ⊢ A type and Σ ⊢ c : C contype
the subsorting judgment Σ ⊢ s1  s2
the constructor typing judgment Σ ⊢ c : C
the subtyping judgment Σ ⊢ A ≤ B
the safe extension judgments Σ; ShKi ⊢ c : C safe at t and Σ; ShKi ⊢ Kelem safe
the signature well-formedness judgment Σ sig
the pattern type judgment U ⊢ p : τ
Moreover, the intersect function is computable.

Proof. For (1) and (2), the type gets smaller in every nontrivial premise.
For subsorting (3), construct the transitive closure.
The single rule for (4) depends only on (3).
For subtyping (5), at least one type gets smaller in each premise.
The rules for (6) are not genuinely inductive, using only previous judgments.
For (7), the signature gets smaller in the first premise.
For (8), the pattern gets smaller in each premise.
In the definition of intersect, the pattern gets smaller in each recursion.

53

Theorem 10 (Decidability).
Given a signature Σ, context Γ and expression e, the set of A such that Σ; Γ ⊢
e ⇒ A is decidable; and, given also a type B, the judgment Σ; Γ ⊢ e ⇐ B is
decidable.
Moreover, given a signature Σ, context Γ , pattern p, type A, matches ms and
type B, the judgment Σ; Γ ; : A ⊢ ms ⇐ B is decidable.
Proof. The auxiliary judgments, such as subtyping (ChkSub) and well-formedness
(ChkDeclare), are decidable by Lemma 23 (Decidability).
In each premise of each bidirectional typing rule, either
1. the expression gets smaller (SynAnno, Chk→I, Syn→E, Chk∗I, ChkDataI,
ChkDataE, ChkDeclare), or
2. the expression is the same; then, either
(a) the conclusion is checking, the premise is checking, and the type gets
smaller (Chk∧I), or
(b) the conclusion is checking, and the premise is synthesizing (ChkSub), or
(c) we are using Syn∧Ek .
That is, we can order the problems lexicographically, considering the expression first; then, we consider the synthesis problem smaller than the checking
problem. For the rules Syn∧E1 and Syn∧E2 , observe that, assuming the premise
has been derived, each rule enumerates one part of the intersection; since type
expressions are finite, only finitely many types can be so enumerated.

