${t}[{\alpha}\mapsto{t_{\alpha}}]$, on the other hand, _instantiates_ the type
variable $\alpha$ with the type $t_{\alpha}$ by strengthening refinement
predicates, as defined in fig. 6.3. Note that definition of
${s}[{\alpha}\mapsto{t}]$ is partial: it is not defined when
$s\equiv{\alpha}{{\\{{r}\\}}}$ for $r$ different than $\mathit{true}$ and $t$
is not a base type, to prevent unsoundness as described above.

$\textrm{{Subtyping}}\hfill\framebox{$\mathrm{\Gamma}\vdash
t_{1}\prec:t_{2}$}$

$\displaystyle\displaystyle{\hbox{\hskip
49.1476pt\vbox{\hbox{\hskip-49.14758pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{{\alpha_{1}}\\!:\\!{k}}\vdash
t_{1}\prec:{t_{2}}[\alpha_{2}:=\alpha_{1}]$}}}\vbox{}}}\over\hbox{\hskip
48.69836pt\vbox{\vbox{}\hbox{\hskip-48.69836pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\forall{{\alpha_{1}}\\!:\\!{k}}.{t_{1}}\prec:\forall{{\alpha_{2}}\\!:\\!{k}}.{t_{2}}$}}}}}}$Sub-
All

Figure 6.4: $\mathsf{\lambda_{\alpha}}$: Rules for Subtyping

_Subtyping_ The rule Sub-All shown in fig. 6.4 formalizes subtyping for
quantified types by renaming the type variables and checking that the types
being quantified over belong to the subtyping relation, in an environment
extended with the type variable. For example, the rule derives

$\emptyset\vdash\forall{{\alpha}\\!:\\!{k}}.{{{x}\\!:\\!{\alpha}}\rightarrow{{\alpha}{{{\\{{{\nu}\\!:\\!{\nu=x}}\\}}}}}}\prec:\forall{{\beta}\\!:\\!{k}}.{{{x}\\!:\\!{\beta}}\rightarrow{\beta}}$

because, after substituting $\beta$ with $\alpha$ the above reduces to

$\alpha\vdash{{x}\\!:\\!{\alpha}}\rightarrow{{\alpha}{{{\\{{{\nu}\\!:\\!{\nu=x}}\\}}}}}\prec:{{x}\\!:\\!{\alpha}}\rightarrow{\alpha}$

which follows from the rules Sub-Base and Sub-Fun.

_Checking_ The rule Chk-TLam in fig. 6.5 checks type-abstraction terms
$\Lambda{\alpha}\\!:\\!{k}.{e}$ against quantified types
$\forall{{\alpha}\\!:\\!{k}}.{t}$ by checking the inner expression $e$ against
the $t$ in an environment containing $\alpha$, and checking the well-
formedness of the polymorphic type.

Example: Implementation of max The specification and implementation of the max
function from section 6.1 are elaborated to:

$\displaystyle t_{\texttt{max}}$ $\displaystyle\doteq\
\forall{\alpha}\\!:\\!{B}.{{\alpha}\rightarrow{{\alpha}\rightarrow{\alpha}}}$
$\displaystyle e_{\texttt{max}}$ $\displaystyle\doteq\
\Lambda{\alpha}\\!:\\!{B}.{\lambda{x,y}.\
{\texttt{{if}}\;x<y\;\texttt{{then}}\;{y}\;\texttt{{else}}\;x}}$ The checking
rules for $\lambda$\- and branching terms establish that
$\displaystyle{\alpha}\\!:\\!{B}$ $\displaystyle\vdash\ \lambda{x,y}.\
{\texttt{{if}}\;x<y\;\texttt{{then}}\;{y}\;\texttt{{else}}\;x}\Leftarrow{\alpha}\rightarrow{{\alpha}\rightarrow{\alpha}}$

after which the rule Chk-TLam lets us conclude $\emptyset\vdash
e_{\texttt{max}}\Leftarrow t_{\texttt{max}}$. $\square$

_Synthesis_ The rule Syn-TApp in fig. 6.5 synthesizes the type for a type-
application term $e[\tau]$. Recall that the elaboration process inserts the
application annotations using one of many standard approaches, but the applied
type is _bare_ in that every refinement is a _hole_ ${\\{{\star}\\}}$ as a
standard elaborator is unaware of refinements. Instead, similar to the Chk-Rec
and Syn-Ann from fig. 5.3 which handle type annotations with holes, the rule
Syn-TApp first guesses a suitable instantiation $\tau\triangleright t$ such
that $t$ is well-formed in the given context. The rule then _substitutes_ the
concrete $t$ for the type variable $\alpha$ quantified over in the signature
for $e$. To prevent unsoundness, this substitution is partial: type synthesis
fails in cases that it is not defined.

Example: Uses of max The function application term $(\texttt{max}\ 0\ 5)$
inside client from section 6.1 is elaborated to
$(\texttt{max}[{\texttt{{int}}}{{\\{{\star}\\}}}]\ 0\ 5)$. In the context
$\mathrm{\Gamma}$ with the signature for max,

$\displaystyle\mathrm{\Gamma}\doteq\ $
$\displaystyle{\texttt{max}}\\!:\\!{t_{\texttt{max}}}$ we have
$\displaystyle\mathrm{\Gamma}\vdash\ $
$\displaystyle\texttt{max}\Rightarrow\forall{\alpha}\\!:\\!{B}.{{\alpha}\rightarrow{{\alpha}\rightarrow{\alpha}}}\quad\mbox{and}\quad{\texttt{{int}}}{{\\{{\star}\\}}}\triangleright\texttt{{nat}}\quad\mbox{and}\quad\mathrm{\Gamma}\vdash\texttt{{nat}}:B$
and so, using Syn-TApp we conclude that $\displaystyle\mathrm{\Gamma}\vdash\ $
$\displaystyle\texttt{max}[{\texttt{{int}}}{{\\{{\star}\\}}}]\Rightarrow{\texttt{{nat}}}\rightarrow{{\texttt{{nat}}}\rightarrow{\texttt{{nat}}}}$
after which the application rule Syn-App fig. 3.6 yields
$\displaystyle\mathrm{\Gamma}\vdash\ $
$\displaystyle{{\texttt{max}[{\texttt{{int}}}{{\\{{\star}\\}}}]}\;{0}}\;{5}\Rightarrow\texttt{{nat}}$

$\square$

$\textrm{{Type Checking}}\hfill\framebox{$\mathrm{\Gamma}\vdash e\Leftarrow
t$}$

$\displaystyle\displaystyle{\hbox{\hskip
65.21811pt\vbox{\hbox{\hskip-65.21811pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{{\alpha}\\!:\\!{k}}\vdash
e\Leftarrow
t\qquad\mathrm{\Gamma}\vdash\forall{{\alpha}\\!:\\!{k}}.{t}:\star$}}}\vbox{}}}\over\hbox{\hskip
44.03758pt\vbox{\vbox{}\hbox{\hskip-44.03758pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\Lambda{\alpha}\\!:\\!{k}.{e}\Leftarrow\forall{{\alpha}\\!:\\!{k}}.{t}$}}}}}}$Chk-
TLam

$\textrm{{Type Synthesis}}\hfill\framebox{$\mathrm{\Gamma}\vdash e\Rightarrow
t$}$

$\displaystyle\displaystyle{\hbox{\hskip
77.66014pt\vbox{\hbox{\hskip-77.66014pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
e\Rightarrow\forall{{\alpha}\\!:\\!{k}}.{s}\qquad\tau\triangleright
t\qquad\mathrm{\Gamma}\vdash t:k$}}}\vbox{}}}\over\hbox{\hskip
31.37558pt\vbox{\vbox{}\hbox{\hskip-31.37558pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
e[\tau]\Rightarrow{s}[{\alpha}\mapsto{t}]$}}}}}}$Syn-TApp

Figure 6.5: $\mathsf{\lambda_{\alpha}}$: Rules for Checking and Synthesis

###  6.4 Verification Conditions

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{sub}&:&(T\times T)\rightarrow
C\\\ \hline\cr\mathsf{sub}(\forall{{\alpha_{1}}\\!:\\!{k}}.{t_{1}},\
\forall{{\alpha_{2}}\\!:\\!{k}}.{t_{2}})&\doteq&\mathsf{sub}(t_{1},\
{t_{2}}[\alpha_{2}:=\alpha_{1}])\\\\[3.61371pt]
\hline\cr\hline\cr\mathsf{check}&:&(\mathrm{\Gamma}\times E\times
T)\rightarrow C\\\ \hline\cr\mathsf{check}(\mathrm{\Gamma},\
\Lambda{\alpha}\\!:\\!{k}.{e},\
\forall{{\alpha}\\!:\\!{k}}.{t})&\doteq&\mathsf{check}(\mathrm{\Gamma};{\alpha},\
e,\ t)\\\\[3.61371pt]
\hline\cr\hline\cr\mathsf{synth}&:&(\mathrm{\Gamma}\times
E)\rightarrow(C\times T)\\\ \hline\cr\mathsf{synth}(\mathrm{\Gamma},\
e[\tau])&\doteq&(c,{{s}[\alpha:=t]})\\\ \quad\mbox{where}&&\\\ \quad\quad(c,\
\forall{{\alpha}\\!:\\!{k}}.{s})&=&\mathsf{synth}(\mathrm{\Gamma},\ e)\\\
\quad\quad t&=&\mathsf{fresh}(\mathrm{\Gamma},\ \ \tau)\\\\[3.61371pt]
\hline\cr\hline\cr\end{array}$ Figure 6.6: Verification Conditions for
$\mathsf{\lambda_{\alpha}}$, extends cases of fig. 5.5

Figure 6.6 summarizes how we extend the Horn Verification Condition generation
algorithm to account for type polymorphism. In essence, we add new cases to
the procedures $\mathsf{sub}$, $\mathsf{check}$ and $\mathsf{synth}$ that
respectively generate Horn Constraint for the subtyping, checking and
synthesis modes to account for the new derivation rules shown in fig. 6.5.

_Subtyping_ The subtyping constraint for two polymorphic types is generated by
recursing on the underlying types, after unifying the type variables.

_Checking_ Similarly, to check a type abstraction, we recursively invoke
$\mathsf{check}$ on the inner expression using a suitably extended context. We
also check well-formedness of the provided type to ensure the kind given to
the abstracted type variable is correct.

_Synthesis_ The heavy lifting is done by $\mathsf{synth}$, which synthesizes a
type and a constraint for a type application term $e[\tau]$. However, we treat
this analogous to synthesizing the type of a type-annotation. Instead of
“guessing” a type as in the declarative Syn-TApp (fig. 6.5), we use $\tau$ to
generate a fresh _template_ for the instantiated $t$ and then substitute the
template $t$ for the type variable $\alpha$ to get the template for the
$e[\tau]$.

Example: client Let us see how the above works on client from section 6.1. Let

$\displaystyle\mathrm{\Gamma}$ $\displaystyle\doteq\
{\texttt{max}}\\!:\\!{\forall{{\alpha}\\!:\\!{k}}.{{\alpha}\rightarrow{{\alpha}\rightarrow{\alpha}}}}$
$\displaystyle e_{0}$ $\displaystyle\doteq\
\texttt{max}[{\texttt{{int}}}{{\\{{\star}\\}}}]$ $\displaystyle e_{1}$
$\displaystyle\doteq\ {{e_{0}}\;{0}}\;{5}$ $\displaystyle e_{2}$
$\displaystyle\doteq\
\texttt{{let}}\;\texttt{r}=e_{1}\;\texttt{{in}}\;\texttt{r}+1$

Now, it it easy to check that as it simply returns the type of max in
$\mathrm{\Gamma}$,

$\displaystyle\mathsf{synth}(\mathrm{\Gamma},\ \texttt{max})$
$\displaystyle\doteq\
(\mathit{true},\forall{{\alpha}\\!:\\!{k}}.{{\alpha}\rightarrow{{\alpha}\rightarrow{\alpha}}})$
Thus, the instance of max synthesizes the type
$\displaystyle\mathsf{synth}(\mathrm{\Gamma},\ e_{0})$ $\displaystyle\doteq\
(\mathit{true},{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}}\rightarrow{{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}}\rightarrow{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}}})$
by substituting all occurrences of $\alpha$ with the _fresh_ template
${\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}$ generated from
${\texttt{{int}}}{{\\{{\star}\\}}}$. Consequently, the subsequent applications
in $e_{1}$ synthesize the constraint and type
$\displaystyle\mathsf{synth}(\mathrm{\Gamma},\ e_{1})$ $\displaystyle\doteq\
(c_{1}\wedge c_{2},\
{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}})$ where the
synthesized type is the (instance) function’s _output_ and $c_{1}$ and $c_{2}$
are constrain $0$ and $5$ to be subtypes of the function’s _input_
$\displaystyle c_{1}$ $\displaystyle\doteq\ \forall\nu.\ \nu=0\Rightarrow\
\kappa({\nu})$ $\displaystyle c_{2}$ $\displaystyle\doteq\ \forall\nu.\
\nu=5\Rightarrow\ \kappa({\nu})$ The result, and hence, output type is bound
to r and so writing $\displaystyle\mathrm{\Gamma}^{\prime}$
$\displaystyle\doteq\
\mathrm{\Gamma};{{\texttt{r}}\\!:\\!{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}}}$
then we get $\mathsf{check}(\mathrm{\Gamma}^{\prime},\ \texttt{r}+1,\
{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{0<\nu}}\\}}}})\doteq\ c_{3}$ where
$\displaystyle c_{3}$ $\displaystyle\doteq\ \forall{r}.\ \kappa({{r}})\
\Rightarrow\ \forall\nu.\ \nu={r}+1\ \Rightarrow\ 0<\nu$

Hence, checking the body $e_{2}$ of client against its output type yields

$\mathsf{check}(\mathrm{\Gamma},\ e_{2},\
{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{0<\nu}}\\}}}})\ \doteq\ c_{1}\wedge
c_{2}\wedge c_{3}$

which is exactly the constraint (6.1). $\square$

###  6.5 Discussion

Thus, the mechanism for refinement inference introduced for
$\mathsf{\lambda_{\kappa}}$ chapter 5 makes using polymorphic functions very
pleasant. The main problem here is to figure out how to _instantiate_ a
polymorphic signature at a particular instantiation site. The key idea is to
_first_ use classical methods to instantiate the _unrefined_ (“bare”) part of
the type, leaving _holes_ for the unknown refinements, after which the Horn
constraint based method from $\mathsf{\lambda_{\kappa}}$ can be applied to
infer suitable refinements.

_Other approaches to Polymorphic Instantation_ There are several other
possible ways to account for type polymorphism.

  * •

_Annotations_ One approach is to have the programmer _explicitly specify_ the
instance refinements. However, this is most unpalatable as polymorphism is
ubiquitous in modern code [pierce-turner] and placing explicit annotations
would get tedious quickly.

  * •

_Defaults_ Another approach would be to _default_ to some refinement such as
$\mathit{true}$ as done in Refined Racket [RefinedRacket] or the Stainless
verifier [kuncak-stainless]. Sadly, this method is rather conservative, as it
precludes the verification of client as the type checker has no information
about the value returned by max other than it is _some_ int.

  * •

_Unification_ A third approach, deployed by the F* system [fstar], is to try
to _unify_ the types of the inputs or outputs to determine suitable instance
refinements. Unfortunately, the interaction with the refinement logic makes
unification brittle: for example, in client it is unclear how to unify the
types of the two inputs 0 and 5 to obtain the instance type
${{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{0\leq\nu}}\\}}}}}$.

_Polymorphism and HOFs_ Finally, support for type polymorphism is essential
for being able to easily use Higher-Order functions. For example, consider the
fold function below that accumulates some value over the integers between $0$
and $n$:

⬇

val fold : (’a => int => ’a) => ’a => int => ’a

let fold = (f, acc, n) => {

let rec loop = (i, acc) => {

if (i < n) {

loop(i+1, f(acc, i))

} else {

acc

}

};

loop(0, acc)

}

We can use fold to sum the integers from 0 to m as:

⬇

val sumTo: m:nat => nat

let sumTo = (m) => {

let add = (x, y) => {x + y};

fold(add, 0, 0, m)

}

Readers familiar with the classical Floyd-Hoare proof rule for loops might
notice its similarity to the type signature of fold:

$\forall{{\alpha}\\!:\\!{k}}.{{({\alpha}\rightarrow{{\texttt{{int}}}\rightarrow{\alpha}})}\rightarrow{{\alpha}\rightarrow{{\texttt{{int}}}\rightarrow{\alpha}}}}$

The type variable $\alpha$ is analagous to the loop _invariant_ ; the
accumulation function’s type
${\alpha}\rightarrow{{\texttt{{int}}}\rightarrow{\alpha}}$ says that it
_preserves_ the invariant, i.e. if the input accumulated value satisfies the
invariant then so does the output; the initial value of the accumulator must
satisfy the invariant $\alpha$; and hence, “by induction”, the final value,
regardless of how many accumulation steps is guaranteed to satisfy the
invariant $\alpha$. Hence, the VC generation mechanism of
$\mathsf{\lambda_{\alpha}}$ let the checker infer that within sumTo, the type
parameter $\alpha$ is instantiated to nat, i.e. that nat is an invariant of
the accumulator. Consequently, the value returned by fold, and hence, sumTo
must also be a nat.

This ability to automatically infer refinements in the presence of
polymorphism will prove especially useful with user-defined _data types_ , as
we shall see next.

##  Chapter 7 Data Types

There is only so much one can do with int and bool values: programs get much
more interesting once we start adding _data types_. Next, lets look at
$\mathsf{\lambda_{\delta}}$ which extends $\mathsf{\lambda_{\alpha}}$ with
support for precisely specifying and verifying properties of (algebraic)
_user-defined data types_.

###  7.1 Examples

As usual, lets begin with a bird’s eye view of the different kinds of
specifications we might write for data types.

####  7.1.1 Properties of Data

The simplest, but perhaps most ubiquitous and useful examples, pertain to
properties of the data stored within polymorphic _containers_ like the list
type defined as:

⬇

type list(’a) =

| Nil

| Cons(’a, list(’a))

The type declaration introduces the type list(’a) which has two constructors:

⬇

val Nil : list(’a)

val Cons : ’a => list(’a) => list(’a)

Lets use Nil and Cons to write a function range that returns the sequence of
int values between a lower bound lo and upper bound hi.

⬇

val range: lo:int => hi:int =>

list(int[v|lo <= v && v < hi])

let range = (lo, hi) => {

if (lo < hi) {

let rest = range(lo + 1, hi);

Cons(lo, rest)

} else {

Nil

}

}

The signature for range specifies that _every_ element in the output list is
in the interval between lo and hi.

####  7.1.2 Relationships between Data

The previous example showed how we can capture properties of _individual_
datum by refining the type parameter of list. What if we want to relate the
values of _multiple_ data across a structure? For example, here’s a data type
definition that specifies an _ordered list_ of non-decreasing values:

⬇

type olist(’a) =

| ONil

| OCons (x:’a, xs:olist(’a[v|x<=v]))

The type definition endows the constructors with refined signatures

⬇

val ONil : olist(’a)

val OCons: x:’a => olist(’a[v|x<=v]) => olist(’a)

The signature for OCons says that the head x must be smaller than _each_
element of the tail. Thus, the type checker will _accept_ the term

⬇

let okList = OCons(0, OCons(1, OCons(2, ONil)));

but will _reject_ the term

⬇

let badList = OCons(0, OCons(2, OCons(1, ONil)));

That is, the constructor’s signature ensures that _illegal_ values do not
_inhabit_ the type. More interestingly, we can specify and verify the function
in fig. 7.1 that inserts a value x into an ordered list ys. We can use insert
to implement an _insertion-sort_ function and verify that it always returns an
ordered list:

⬇

val isort : list(’a) => olist(’a)

let rec isort = (xs) => {

switch (xs){

| Nil => ONil

| Cons (h, t) => insert(h, isort(t))

}

};

⬇

val insert : ’a => olist(’a) => olist(’a)

let rec insert = (x, ys) => {

switch (ys) {

| ONil =>

let tl = ONil;

OCons(x, tl)

| OCons(y, ys’) =>

if (x <= y) {

let tl = OCons(y,ys’);

OCons(x,tl)

} else {

let tl = insert(x,ys’);

OCons(y,tl)

}

}

};

Figure 7.1: A function to insert a value x into an ordered list ys.

####  7.1.3 Properties of Structure

A third class of useful specifications are _aggregate_ properties of the
entire structure, for example, the _height_ of a tree, or the _multi-set_ of
elements of a list. Next, lets see how these can be specified by refining the
_output_ types of the constructors with _ghost_ functions that specify the
aggregate properties via two steps.

_1\. Defining Measures_ To specify the _length_ of a list, we introduce a
function such that $\texttt{len}({xs})$ represents the length of the list
${xs}$.

⬇

measure len: list(’a) => nat

To ensure decidable VC validity checking we ensure that len is _uninterpreted_
in the refinement logic, i.e. the SMT solver only knows that len satisfies the
_axiom of congruence_

$\forall{xs},{ys}.\ {xs}={ys}\ \Rightarrow\
\texttt{len}({xs})=\texttt{len}({ys})$

_2\. Refining Constructors_ We use measures to specify the structure’s
properties, by appropriately refining the type of the constructors’ output.

⬇

type list(’a) =

| Nil => [v|len(v) = 0]

| Cons(x:’a,xs:list(’a)) => [v|len(v) = 1+len(xs)]

In the definition above, the output for Nil says that it constructs a list of
length $0$; the output for Cons says that it constructs a list whose length is
one greater than the tail.

_3\. Using Measures_ We can now use len in refinements in various ways. First,
to specify pre-conditions on _partial_ functions. For example, refinement
checking ensures that due to the precondition — which will be checked at uses
of head — the assert(false) never fails at run-time:

⬇

val head : list(’a)[v|0 < len(v)] => ’a

let head = (xs) => {

switch(xs){

| Cons(h, t) => h

| Nil => assert(false)

}

};

Second, to specify post-conditions e.g. on the result of list concatenation

⬇

val append: xs:list(’a) => ys:list(’a) =>

list(’a)[v|len(v) = len(xs)+len(ys)]

let rec append = (xs, ys) => {

switch (xs) {

| Nil => ys

| Cons(h, t) => let rest = append(t, ys);

Cons(h, rest)

}

};

_Measures are Ghost Code_ Measures only exist at the level of the
_specification_ : they cannot be used in the implementation111Systems like
LiquidHaskell allow the programmer to specify the measure as a function that
satisfies certain syntactic constraints, and then automatically _generate_ the
constructor’s refined types. However, that is merely a convenience:
conceptually, a measure exists only for specification.. However, it is easy to
connect measures to run-time values, via functions like

⬇

val length: xs:list(’a) => int[v|v = len(xs)]

let rec length = (xs) => {

switch(xs){

| Nil => 0

| Cons(h, t) => 1 + length(t)

}

}

We can now use the result of length to determine whether it is safe to compute
the head of a list

⬇

val safeHead : ’a => list(’a) => ’a

let safeHead = (default, xs) => {

let nonEmpty = 0 < length(xs);

if (nonEmpty) { head(xs) } else { default }

};

Refinement typing establishes that when nonEmpty is true, we indeed have 0 <
len(xs) thereby verifying the call head(xs).

###  7.2 Types and Terms

From the examples in section 7.1 one might get the impression that
$\mathsf{\lambda_{\delta}}$ must have multiple extensions over
$\mathsf{\lambda_{\alpha}}$. In fact, all three flavors of specifications —
reasoning about individual data, about relationships between data, and
reasoning about structure — are supported by a single pillar: _refined data
constructors_. Thus, the only mechanisms we need are a way to “apply” the
refined type when _constructing_ new data and to “unapply” the type when
_destructing_ the data by pattern matching. Next, lets see how these two ideas
are formalized in $\mathsf{\lambda_{\delta}}$, whose syntactic additions are
summarized in Figure 7.2.

_Datatypes_ First, we assume there is a set of _type constructors_ $C$ (e.g.
list) and _data constructors_ $D$ (e.g. Nil, Cons). The _polarity_ $p$
captures the position that type variables appear in definitions of data types
and can be positive ($+$), negative ($-$), both ($\pm$), or neither
($\epsilon$). A _datatype_ $\delta$ is a triple
$\langle{C},\;{\overline{{\alpha}\\!:\\!{k}/{p}}},\;{\overline{{D}\\!:\\!{t}}}\rangle$
comprising a type constructor $C$, the list of type variables over which the
datatype is parameterized together with their kind and polarity
$\overline{{\alpha}\\!:\\!{k}/{p}}$, and a set of data constructors and their
refinement types $\overline{{D}\\!:\\!{t}}$.

Example: Ordered Lists Suppose we wrote the following ordered list type,
refined with a len measure tracking the list’s size

⬇

type ol(’a) =

| ON => [v|len(v)=0]

| OC(’a,xs:ol(’a[v|x<=v])) => [v|len(v)=1+len(xs)]

We would represent the above as
$\delta_{\texttt{OL}}\doteq\langle\texttt{OL},\ \\{{\alpha}\\!:\\!{B}/{+}\\},\
\\{{\texttt{ON}}\\!:\\!{t_{N}};{\texttt{OC}}\\!:\\!{t_{C}}\\}\rangle$ The type
variable $\alpha$ appears in one positive position and since $\alpha$ elements
are compared it is of base kind. The types of the “nil” and “cons”
constructors are respectively:

$\displaystyle t_{N}$ $\displaystyle\doteq\
\forall{\alpha}\\!:\\!{B}.{{{\texttt{OL}}[{\alpha}]}{{{\\{{{\nu}\\!:\\!{\texttt{len}({\nu})=0}}\\}}}}}$
$\displaystyle t_{C}$ $\displaystyle\doteq\
\forall{\alpha}\\!:\\!{B}.{{{x}\\!:\\!{\alpha}}\rightarrow{{{{xs}}\\!:\\!{{\texttt{OL}}[{{\alpha}{{{\\{{{\nu}\\!:\\!{x\leq\nu}}\\}}}}}]}}\rightarrow{{{\texttt{OL}}[{\alpha}]}{{{\\{{{\nu}\\!:\\!{\texttt{len}({\nu})=1+\texttt{len}({{xs}})}}\\}}}}}}}$
(7.1)

That is, the type $t_{N}$ says that “nil” returns an ordered list of length
$0$; and the type $t_{C}$ says that “cons” takes as input a head ${x}$ of type
$\alpha$ and a tail ${xs}$ _each_ of whose elements is an $\alpha$ larger than
${x}$, and returns an ordered list whose size is one more than that of the
tail ${xs}$. $\square$

_Environments_ We extend the environments to include all the data type
definitions $\delta$. For simplicity, we will assume that all the data type
definitions and measure names are _global_ , that is, they belong in the top-
level environment used for type checking and synthesis.

_Types_ As hinted in the discussion for constructors above, the language of
_basic_ types is extended to include a _type constructor application_ form
${C}[{\overline{t}}]$, where the type constructor $C$ is applied to the type
arguments $\overline{t}$. Intuitively one can think of the above as the type
obtained by instantiating the type parameters $\overline{\alpha}$ of $C$ with
the actual type arguments $\overline{t}$. As before, these basic types can be
refined, so
${{\texttt{OL}}[{\texttt{{nat}}}]}{{{\\{{{\nu}\\!:\\!{3\leq\texttt{len}({\nu})}}\\}}}}$
would correspond to the type of ordered lists of non-negative int values
comprising three or more elements.

_Alternatives_ Each _alternative_ ${D}({\overline{x}})\rightarrow{e}$
comprises a _pattern_ $D(\overline{x})$ and the term $e$ to be evaluated if
the scrutinee matches the pattern.

_Terms_ We add the data constructors $D$ to the language of terms so that
polymorphic instantiation $e[t]$ (from $\mathsf{\lambda_{\alpha}}$) and
function application ${e}\;{x}$ (from $\mathsf{\lambda}$) can be combined to
_construct_ values of user-defined types. To _destruct_ values of user-defined
types, we introduce a pattern-match form
$\texttt{{switch}}\;y\;\\{\overline{a}\\}$ where the value bound to $y$ is
_scrutinized_ by each of the alternatives in $\overline{a}$.

_Data Constructors_ | $D$ | $\vcentcolon\vcentcolon=$ | $D_{1},D_{2},D_{3},\ldots$ |
---|---|---|---|---
_Type Constructors_ | $C$ | $\vcentcolon\vcentcolon=$ | $C_{1},C_{2},C_{3},\ldots$ |
_Polarity_ | $p$ | $\vcentcolon\vcentcolon=$ |  $+$ $\ \mid\ $ $-$ $\ \mid\ $ $\pm$ $\ \mid\ $ $\epsilon$ |
_Datatypes_ | $\delta$ | $\vcentcolon\vcentcolon=$ | $\langle{C},\;{\overline{{\alpha}\\!:\\!{k}/{p}}},\;{\overline{{D}\\!:\\!{t}}}\rangle$ |
_Environments_ | $\mathrm{\Gamma}$ | $\vcentcolon\vcentcolon=$ | $\ldots$ | _from Fig. 6.1_
|  | $\ \mid\ $ | $\mathrm{\Gamma};{\delta}$ | _type definitions_
_Basic Types_ | $b$ | $\vcentcolon\vcentcolon=$ | $\ldots$ | _from Fig. 6.1_
|  | $\ \mid\ $ | ${C}[{\overline{t}}]$ | _datatypes_
_Alternatives_ | $a$ | $\vcentcolon\vcentcolon=$ | ${D}({\overline{x}})\rightarrow{e}$ | _switch alternative_
_Terms_ | $e$ | $\vcentcolon\vcentcolon=$ | $\ldots$ | _from Fig. 6.1_
|  | $\ \mid\ $ | $D$ | _data constructor_
|  | $\ \mid\ $ | $\texttt{{switch}}\;x\;\\{\overline{a}\\}$ | _data destructor_
Figure 7.2: $\mathsf{\lambda_{\delta}}$: Syntax of Types and Terms

###  7.3 Declarative Typing

Next, lets see how the rules for well-formedness, subtyping, checking and
synthesis are extended to account for constructors and destructors.

$\textrm{{Well-formedness}}\hfill\framebox{$\mathrm{\Gamma}\vdash t:k$}$

$\displaystyle\displaystyle{\hbox{\hskip
130.10626pt\vbox{\hbox{\hskip-130.10625pt\hbox{\hbox{$\displaystyle\displaystyle\overline{k}=\mathsf{kinds}(\delta,\
C)\quad\mathrm{\Gamma}\vdash t_{i}:k_{i}\ \mbox{for each}\ 1\leq
i\leq\mid\\!\overline{k}\\!\mid\quad\mathrm{\Gamma};{{x}\\!:\\!{{C}[{\overline{t}}]}}\vdash
p$}}}\vbox{}}}\over\hbox{\hskip
35.08401pt\vbox{\vbox{}\hbox{\hskip-35.084pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash{{C}[{\overline{t}}]}{{{\\{{{x}\\!:\\!{p}}\\}}}}:B$}}}}}}$Wf-
Data

Figure 7.3: $\mathsf{\lambda_{\delta}}$: Rule for Well-formedness

$\textrm{{Subtyping}}\hfill\framebox{$\mathrm{\Gamma}\vdash
t_{1}\prec:t_{2}$}$

$\displaystyle\displaystyle{\hbox{\hskip
141.78278pt\vbox{\hbox{\hskip-141.78278pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
s_{i}\prec:t_{i}\ \mbox{for each}\ i.p_{i}\in\\{+,\pm\\}$}\hskip
20.00003pt\hbox{\hskip-128.61375pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
t_{i}\prec:s_{i}\ \mbox{for each}\ i.p_{i}\in\\{-,\pm\\}$}\hskip
20.00003pt\hbox{\hskip-106.7202pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{{\nu_{1}}\\!:\\!{{{\\{{{{C}[{\overline{s}}]}\\!:\\!{p_{1}}}\\}}}}}\vdash{p_{2}}[\nu_{2}:=\nu_{1}]\qquad\overline{p}=\mathsf{polarities}(\delta,\
C)$}}}}}}}\vbox{\hbox{\hskip-128.61375pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
t_{i}\prec:s_{i}\ \mbox{for each}\ i.p_{i}\in\\{-,\pm\\}$}\hskip
20.00003pt\hbox{\hskip-106.7202pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{{\nu_{1}}\\!:\\!{{{\\{{{{C}[{\overline{s}}]}\\!:\\!{p_{1}}}\\}}}}}\vdash{p_{2}}[\nu_{2}:=\nu_{1}]\qquad\overline{p}=\mathsf{polarities}(\delta,\
C)$}}}}}\vbox{\hbox{\hskip-106.7202pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{{\nu_{1}}\\!:\\!{{{\\{{{{C}[{\overline{s}}]}\\!:\\!{p_{1}}}\\}}}}}\vdash{p_{2}}[\nu_{2}:=\nu_{1}]\qquad\overline{p}=\mathsf{polarities}(\delta,\
C)$}}}\vbox{}}}}}\over\hbox{\hskip
60.4475pt\vbox{\vbox{}\hbox{\hskip-60.4475pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash{{C}[{\overline{s}}]}{{{\\{{{\nu_{1}}\\!:\\!{p_{1}}}\\}}}}\prec:{{C}[{\overline{t}}]}{{{\\{{{\nu_{2}}\\!:\\!{p_{2}}}\\}}}}$}}}}}}$Sub-
Data

Figure 7.4: $\mathsf{\lambda_{\delta}}$: Rules for Subtyping

####  7.3.1 Well-formedness

The rule Wf-Data shown in fig. 7.3 formalizes well-formedness of datatypes.
The rule checkes that the refinement of the type is well-formed, that each of
the type arguments has the proper kind, and that the type constructor is fully
applied. The premises use the function $\mathsf{kinds}(\delta,\ C)$ that
retrieves the kinds of $C$ from the data environment $\delta$:

$\mathsf{kinds}(\delta,\ C)\doteq\overline{k}\quad\text{if}\
\langle{C},\;{\overline{{\alpha}\\!:\\!{k}/{p}}},\;{\overline{{D}\\!:\\!{t}}}\rangle\in\delta$

####  7.3.2 Subtyping

The rule Sub-Data shown in fig. 7.4 formalizes subtyping between datatypes. In
an environment $\mathrm{\Gamma}$, the type
${{C}[{\overline{s}}]}{{{\\{{{\nu_{1}}\\!:\\!{p_{1}}}\\}}}}$ is a subtype of
${{C}[{\overline{t}}]}{{{\\{{{\nu_{2}}\\!:\\!{p_{2}}}\\}}}}$, if the base
refinement $p_{1}$ entails $p_{2}$, and _each_ of the component types $s_{i}$
is a subtype of the corresponding component $t_{i}$. Subtyping of the
components is checked using $\mathsf{polarities}(\delta,\ C)$ which retrieves
the polarity information from the data environment $\delta$

$\mathsf{polarities}(\delta,\ C)=\overline{p}\ \text{if}\
\langle{C},\;{\overline{{\alpha}\\!:\\!{k}/{p}}},\;{\overline{{D}\\!:\\!{t}}}\rangle\in\delta$

For each component with positive polarity (resp. negative) polarity the rule
uses covariant (resp. contravariant) subtyping.

Example: Subtyping in insert Consider the environment

$\mathrm{\Gamma}^{\prime}_{\leq}\ \doteq\ {\alpha}\\!:\\!{B};\
{{x}}\\!:\\!{\alpha};\ {{y}}\\!:\\!{\alpha};\
{{ys^{\prime}}}\\!:\\!{{\texttt{OL}}[{{\alpha}{{{\\{{{\nu}\\!:\\!{y\leq\nu}}\\}}}}}]};\
{{ys}}\\!:\\!{{\texttt{OL}^{+}}[{\alpha,{ys^{\prime}}}]};\ {x}\leq{y}$

and the alias ${\texttt{OL}^{+}}[{\alpha,{z}}]$ that denotes ordered lists of
type $\alpha$ whose size is one more than that of ${z}$. As the following
entailment is valid

$\displaystyle\forall{x},{y},\nu.\ $ $\displaystyle{x}\leq{y}\ \Rightarrow\
{y}\leq\nu\ \Rightarrow\ {x}\leq\nu$ the rule Sub-Data lets us conclude
$\displaystyle\mathrm{\Gamma}^{\prime}_{\leq}$ $\displaystyle\ \vdash\
{\texttt{OL}}[{{\alpha}{{{\\{{{\nu}\\!:\\!{{y}\leq\nu}}\\}}}}}]\prec:\
{\texttt{OL}}[{{\alpha}{{{\\{{{\nu}\\!:\\!{{x}\leq\nu}}\\}}}}}]$ (7.2) As the
following entailment is valid $\displaystyle\forall{ys},\ {ys^{\prime}},\
{tl}.\ $ $\displaystyle\texttt{len}({{ys}})=1+\texttt{len}({{ys^{\prime}}})\
\Rightarrow\ \texttt{len}({{tl}})=1+\texttt{len}({{ys^{\prime}}})\
\Rightarrow$ $\displaystyle\texttt{len}({\nu})=1+\texttt{len}({{tl}})\
\Rightarrow\ \texttt{len}({\nu})=1+\texttt{len}({{ys}})$ the rule Sub-Data
lets us conclude
$\displaystyle\mathrm{\Gamma}^{\prime}_{\leq};{{tl}}\\!:\\!{t_{y}}$
$\displaystyle\ \vdash\ {\texttt{OL}^{+}}[{\alpha,{tl}}]\ \prec:\
{\texttt{OL}^{+}}[{\alpha,{ys}}]$ (7.3)

where $t_{y}\doteq{\texttt{OL}^{+}}[{\alpha_{x},{ys^{\prime}}}]$ $\square$

####  7.3.3 Checking

$\textrm{{Type Checking}}\hfill\framebox{$\mathrm{\Gamma}\vdash e\Leftarrow
t$}$

$\displaystyle\displaystyle{\hbox{\hskip
47.07204pt\vbox{\hbox{\hskip-47.07204pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\mid{y}\vdash
a_{i}\Leftarrow t\ \mbox{for each}\ i$}}}\vbox{}}}\over\hbox{\hskip
41.06131pt\vbox{\vbox{}\hbox{\hskip-41.06131pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\texttt{{switch}}\;y\;\\{\overline{a}\\}\Leftarrow
t$}}}}}}$Chk-Swt

$\textrm{{Checking Alternatives}}\hfill\framebox{$\mathrm{\Gamma}\mid{y}\vdash
a\Leftarrow t$}$

$\displaystyle\displaystyle{\hbox{\hskip
133.9429pt\vbox{\hbox{\hskip-133.9429pt\hbox{\hbox{$\displaystyle\displaystyle
s=\mathsf{ctor}(\mathrm{\Gamma},\ D,\
y)\qquad\mathrm{\Gamma}^{\prime}=\mathsf{unapply}(\mathrm{\Gamma},\ y,\
\overline{z},\ s)\qquad\mathrm{\Gamma}^{\prime}\vdash e\Leftarrow
t$}}}\vbox{}}}\over\hbox{\hskip
35.00128pt\vbox{\vbox{}\hbox{\hskip-35.00127pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\mid{y}\vdash{D}({\overline{z}})\rightarrow{e}\Leftarrow
t$}}}}}}$Chk-Alt

Figure 7.5: $\mathsf{\lambda_{\delta}}$: Rules for Type Checking
$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{unapply}&:&(\mathrm{\Gamma}\times
X\times X^{*}\times T)\rightarrow\mathrm{\Gamma}\\\
\hline\cr\mathsf{unapply}(\mathrm{\Gamma},\ y,\ z;\overline{z},\
{{x}\\!:\\!{s}}\rightarrow{t})&\doteq&\mathsf{unapply}(\mathrm{\Gamma};{{z}\\!:\\!{s}},\
y,\ \overline{z},\ {t}[x:=z])\\\\[3.61371pt]
\mathsf{unapply}(\mathrm{\Gamma},\ y,\ \emptyset,\
t)&\doteq&\mathrm{\Gamma};{{y}\\!:\\!{\mathsf{meet}(\mathrm{\Gamma}(y),t)}}\\\\[7.22743pt]
\hline\cr\hline\cr\mathsf{ctor}&:&(\mathrm{\Gamma}\times D\times X)\rightarrow
T\\\ \hline\cr\mathsf{ctor}(\mathrm{\Gamma},\ D,\
y)&\doteq&{s}[\overline{\alpha}:=\overline{t}]\\\ \quad\mbox{where}&&\\\
\quad\quad{C}[{\overline{t}}]&=&\mathrm{\Gamma}(y)\\\
\quad\quad\forall{{\overline{\alpha}}\\!:\\!{k}}.{s}&=&\mathrm{\Gamma}(D)\\\\[3.61371pt]
\hline\cr\hline\cr\end{array}$
Figure 7.6: Meta-functions for Type Checking Switch Alternatives
$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{meet}&:&(T\times T)\rightarrow
T\\\
\hline\cr\mathsf{meet}({b}{{{\\{{{\nu_{1}}\\!:\\!{p_{1}}}\\}}}},{b}{{{\\{{{\nu_{2}}\\!:\\!{p_{2}}}\\}}}})&\doteq&{b}{{{\\{{{\nu_{1}}\\!:\\!{p_{1}\wedge{p_{2}}[\nu_{2}:=\nu_{1}]}}\\}}}}\\\\[3.61371pt]
\mathsf{meet}({{x_{1}}\\!:\\!{s_{1}}}\rightarrow{t_{1}},{{x_{2}}\\!:\\!{s_{2}}}\rightarrow{t_{2}})&\doteq&{{x_{1}}\\!:\\!{\mathsf{meet}(s_{1},s_{2})}}\rightarrow{\mathsf{meet}(t_{1},{t_{2}}[x_{2}:=x_{1}])}\\\\[3.61371pt]
\mathsf{meet}(\forall{{\alpha_{1}}\\!:\\!{k}}.{t_{1}},\forall{{\alpha_{2}}\\!:\\!{k}}.{t_{2}})&\doteq&\forall{{\alpha_{1}}\\!:\\!{k}}.{\mathsf{meet}(t_{1},{t_{2}}[\alpha_{2}:=\alpha_{1}])}\\\\[3.61371pt]
\hline\cr\hline\cr\end{array}$ Figure 7.7: Conjoining Types

The rule Chk-Swt shown in fig. 7.5 describes how to _check_ that a switch
expression has a given type $t$, by checking that each alternative of the
switch produces a value of type $t$.

_Checking an Alternative_ The judgment
$\mathrm{\Gamma}\mid{y}\vdash{D}({\overline{z}})\rightarrow{e}\Leftarrow t$
states that in the _environment_ $\mathrm{\Gamma}$ when the _scrutinee_ $y$
matches the _pattern_ $D(\overline{z})$ the evaluated _result_ $e$ has type
$t$. The rule Chk-Alt establishes this judgment in three steps.

  1. 1.

We use $\mathsf{ctor}(\mathrm{\Gamma},\ D,\ y)$ summarized in fig. 7.6 to get
$s$, the monomorphic _instantiation_ of the polymorphic type of constructor
$D$. In other words, $s$ is the type of $D$ at _this_ particular match-
instance.

  2. 2.

We invoke $\mathsf{unapply}(\mathrm{\Gamma},\ y,\ \overline{z},\ s)$
summarized in fig. 7.6 to obtain the environment $\mathrm{\Gamma}^{\prime}$
which is $\mathrm{\Gamma}$ extended with the types for the pattern match
bindings $\overline{z}$ and also, with additional refinements for the
scrutinee $y$ that are revealed by matching against this particular pattern.

  3. 3.

We check that result $e$ has the type $t$ in environment
$\mathrm{\Gamma}^{\prime}$.

_Unapply_ At destruction sites we use $\mathsf{unapply}(\mathrm{\Gamma},\ y,\
\overline{z},\ s)$ summarized in fig. 7.6. The function $\mathsf{unapply}$ can
be viewed as the dual of function application Given the output type of the
constructed value ($s$), we want to (1) determine the types that the inputs
($\overline{z}$) must have had, and to then (2) add those bindings to get the
environment used to check the alternative’s body $e$. $\mathsf{unapply}$ does
so by recursively “zipping” together the match-binders $\overline{z}$ with the
input binders of the constructor’s (function) type $s$. If the sequence of
binders is _non-empty_ ($z;\overline{z}$) and the constructor type is
${{x}\\!:\\!{s}}\rightarrow{t}$ then we extend $\mathrm{\Gamma}$ with the
binding ${z}\\!:\\!{s}$, and recurse on the extended environment and the
remaining binders $\overline{z}$ and the “rest” of the constructor type, i.e.
its output $t$ after substituting the formal $x$ with the “actual” $z$. Once
the sequence of binders is _empty_ ($\emptyset$) then constructor type $t$ is
exactly the result of $D(\overline{z})$. Crucially, $t$ can have extra
information about the scrutinee $y$ that holds under this particular pattern
match, and so we _strengthen_ the type of $y$ by using $\mathsf{meet}$ to
conjoin the old type $\mathrm{\Gamma}(y)$ with the pattern-match result $t$,
and return the extended environment as the final result (that is used to check
the alternative’s body $e$.)

$\displaystyle\lambda{x},\ {ys}.\ $ $\displaystyle\texttt{{switch}}\ ({ys})$
$\displaystyle\quad\mid{\texttt{OC}}({{y},{ys^{\prime}}})\ \rightarrow$
$\displaystyle\quad\quad\texttt{{if}}\ {x}\leq{y}\ \texttt{{then}}$
$\displaystyle\quad\quad\quad\texttt{{let}}\
{tl}={{\texttt{OC}[\alpha_{{x}}]}\;{{y}}}\;{{ys^{\prime}}}\ \texttt{{in}}$
$\displaystyle\quad\quad\quad{{\texttt{OC}[\alpha]}\;{{x}}}\;{{tl}}$
$\displaystyle\quad\quad\texttt{{else}}\ \ldots$
$\displaystyle\quad\mid\texttt{ON}\ \rightarrow\ldots$ Figure 7.8: Definition
of insert (fig. 7.1) with elaborated type applications.

Example: Checking in insert Lets see how the declarative rules let us _check_
the implementation of the insert function from fig. 7.1. Suppose our goal is
to check that insert implements the type

${{{{x}}\\!:\\!{\alpha}}\rightarrow{{{{ys}}\\!:\\!{{\texttt{OL}}[{\alpha}]}}\rightarrow{{\texttt{OL}^{+}}[{\alpha,{ys}}]}}}$

i.e. that insert returns an ordered list with one more element than the input
list $ys$. The fig. 7.8 shows a fragment of the definition of insert
elaborated with explicit type applications at constructor application sites.
Rule Chk-Lam reduces type checking to the following judgment that checks the
body of insert against the specified output type in the context
$\mathrm{\Gamma}$ comprising the bindings for the inputs ${x}$ and ${ys}$:

$\displaystyle\mathrm{\Gamma}$ $\displaystyle\ \vdash\
\texttt{{switch}}\;{ys}\;\\{\
{\texttt{OC}}({{y},{ys^{\prime}}})\rightarrow{e^{\prime}}\ \mid\
\ldots\\}\Leftarrow\ {\texttt{OL}^{+}}[{\alpha,{ys}}]$ The rule Chk-Alt
reduces the above into obligations for each alternative. For the OC case, we
get: $\displaystyle\mathrm{\Gamma}\ \mid\ {ys}$ $\displaystyle\ \vdash\
{\texttt{OC}}({{y},{ys^{\prime}}})\rightarrow{e^{\prime}}\Leftarrow\
{\texttt{OL}^{+}}[{\alpha,{ys}}]$ By the definition of $\mathsf{unapply}$ the
above judgment reduces to $\displaystyle\mathrm{\Gamma}^{\prime}$
$\displaystyle\ \vdash\ e^{\prime}\Leftarrow\
{\texttt{OL}^{+}}[{\alpha,{ys}}]$ where $\mathrm{\Gamma}^{\prime}$ is
$\mathrm{\Gamma}$ extended with the bindings computed by $\mathsf{unapply}$
$\displaystyle\mathrm{\Gamma}^{\prime}$ $\displaystyle\ \doteq\
\mathrm{\Gamma};\ {{y}}\\!:\\!{\alpha};\
{{ys^{\prime}}}\\!:\\!{{\texttt{OL}}[{{\alpha}{{{\\{{{\nu}\\!:\\!{y\leq\nu}}\\}}}}}]};\
{{ys}}\\!:\\!{{\texttt{OL}^{+}}[{\alpha,{ys^{\prime}}}]}$ As $e^{\prime}$ is
$\texttt{{if}}\;{x}\leq{y}\;\texttt{{then}}\;{e^{\prime}_{\leq}}\;\texttt{{else}}\;\ldots$
by rule Chk-If, eliding the else-branch, and recalling that
$e^{\prime}_{\leq}\doteq\texttt{{let}}\;{tl}=e_{y}\;\texttt{{in}}\;e_{x}$
(fig. 7.9) the above judgment reduces to
$\displaystyle\mathrm{\Gamma}^{\prime};\ {x}\leq{y}$ $\displaystyle\ \vdash\
\texttt{{let}}\;{tl}=e_{y}\;\texttt{{in}}\;e_{x}\Leftarrow\
{\texttt{OL}^{+}}[{\alpha,{ys}}]$ (7.4) In the sequel, we will show how the
synthesis rules establish $\displaystyle\mathrm{\Gamma}^{\prime}_{\leq}$
$\displaystyle\ \vdash\ e_{{y}}\Rightarrow t_{{y}}$ (7.5)
$\displaystyle\mathrm{\Gamma}^{\prime}_{\leq};{{tl}}\\!:\\!{t_{y}}$
$\displaystyle\ \vdash\ e_{{x}}\Rightarrow{\texttt{OL}^{+}}[{\alpha,{tl}}]$
(7.6) which Chk-Let and Chk-Syn combine with the subtyping judgment
$\displaystyle\mathrm{\Gamma}^{\prime}_{\leq};{{tl}}\\!:\\!{t_{y}}$
$\displaystyle\ \vdash\ {\texttt{OL}^{+}}[{\alpha,{tl}}]\prec:\
{\texttt{OL}^{+}}[{\alpha,{ys}}]\quad\mbox{previously derived in
(\ref{eq:ins:seven})}$

to yield the goal (7.4). $\square$

$\begin{array}[]{lcl}t_{\texttt{ins}}&\doteq&{{{x}}\\!:\\!{\alpha}}\rightarrow{{{{ys}}\\!:\\!{{\texttt{OL}}[{\alpha}]}}\rightarrow{{\texttt{OL}^{+}}[{\alpha,{ys}}]}}\\\
{\texttt{OL}^{+}}[{\alpha,{z}}]&\doteq&{\texttt{OL}}[{\alpha}]{{{\\{{{\nu}\\!:\\!{\texttt{len}({\nu})=1+\texttt{len}({{z}})}}\\}}}}\\\
\mathrm{\Gamma}&\doteq&{\alpha}\\!:\\!{B};\
{\texttt{insert}}\\!:\\!{t_{{ins}}};\ {{x}}\\!:\\!{\alpha};\
{{ys}}\\!:\\!{{\texttt{OL}}[{\alpha}]}\\\
\mathrm{\Gamma}^{\prime}&\doteq&\mathrm{\Gamma};\ {{y}}\\!:\\!{\alpha};\
{{ys^{\prime}}}\\!:\\!{{\texttt{OL}}[{{\alpha}{{{\\{{{\nu}\\!:\\!{y\leq\nu}}\\}}}}}]};\
{{ys}}\\!:\\!{{\texttt{OL}^{+}}[{\alpha,{ys^{\prime}}}]}\\\
\mathrm{\Gamma}^{\prime}_{\leq}&\doteq&\mathrm{\Gamma}^{\prime};\
{x}\leq{y}\\\
e^{\prime}&\doteq&\texttt{{if}}\;{x}\leq{y}\;\texttt{{then}}\;{e^{C}_{\leq}}\;\texttt{{else}}\;\ldots\\\
e^{\prime}_{\leq}&\doteq&\texttt{{let}}\;{tl}=e_{y}\;\texttt{{in}}\;e_{x}\\\
e_{{y}}&\doteq&{{\texttt{OC}[\alpha_{{x}}]}\;{{y}}}\;{{ys^{\prime}}}\\\
e_{{x}}&\doteq&{{\texttt{OC}[\alpha]}\;{{x}}}\;{{tl}}\\\
\alpha_{{x}}&\doteq&{\alpha}{{{\\{{{\nu}\\!:\\!{{x}\leq\nu}}\\}}}}\\\
t_{y}&\doteq&{\texttt{OL}^{+}}[{\alpha_{x},{ys^{\prime}}}]\\\ \end{array}$
Figure 7.9: Definitions for checking and synthesizing types for insert fig.
7.1.

####  7.3.4 Synthesis

As we said at the outset, the key mechanism to supporting datatypes are
refined _data constructors_. Their types are applied at construction sites in
a manner identical to plain function application, where given the input type
we synthesize the output. Hence, to synthesize the types for constructor
applications we add the rule Syn-Data shown in fig. 7.5. The rule synthesizes
the type for a data constructor $D$ by looking up its type in the environment
$\mathrm{\Gamma}$; after this, the rules for application i.e. Syn-App from
fig. 3.5 suffice for constructor applications.

Example: Synthesis in insert Lets see how the synthesis rules let us establish
the judgments (7.5) and (7.6) that are needed to check the then branch of the
implementation of insert from fig. 7.1.

First, lets establish the type synthesized for the constructor application of
7.5 (where the abbreviations $\alpha_{x}$, $t_{y}$ are summarized in fig.
7.9):

$\displaystyle\mathrm{\Gamma}^{\prime}_{\leq}$ $\displaystyle\ \vdash\
{{\texttt{OC}[\alpha_{{x}}]}\;{{y}}}\;{{ys^{\prime}}}\Rightarrow{\texttt{OL}^{+}}[{\alpha_{x},{ys^{\prime}}}]$
Syn-Data synthesizes the polymorphic type of the constructor OC (7.1) and Syn-
TApp synthesizes its instantiation to yield
$\displaystyle\mathrm{\Gamma}^{\prime}_{\leq}$ $\displaystyle\ \vdash\
{\texttt{OC}[\alpha_{{x}}]}\Rightarrow{{{z}}\\!:\\!{\alpha_{{x}}}}\rightarrow{{{{zs}}\\!:\\!{{\texttt{OL}}[{{\alpha_{{x}}}{{{\\{{{\nu}\\!:\\!{{z}\leq\nu}}\\}}}}}]}}\rightarrow{{\texttt{OL}^{+}}[{\alpha_{x},{zs}}]}}$
(7.7)

The rule Syn-App requires that the types of the first and second arguments
${y}$ and ${ys^{\prime}}$ must be subtypes of the constructor’s respective
input types. The subtyping for the first argument $y$ follows from the
validity of the entailment

$\forall{x},{y},\nu.\ {x}\leq{y}\ \Rightarrow\ \nu={y}\ \Rightarrow\
{x}\leq\nu$

The subtyping for the second argument was established in (7.2). Hence, Syn-App
establishes (7.5).

Next, lets synthesize a type for the constructor application (7.6) in the
environment $\mathrm{\Gamma}^{\prime}_{\leq}$ extended by binding $t_{y}$
synthesized in (7.5) to ${tl}$:

$\displaystyle\mathrm{\Gamma}^{\prime}_{\leq};{{tl}}\\!:\\!{t_{y}}$
$\displaystyle\ \vdash\
{{\texttt{OC}[\alpha]}\;{{x}}}\;{{tl}}\Rightarrow{\texttt{OL}^{+}}[{\alpha,{tl}}]$
Again via Syn-Data and Syn-TApp the constructor’s instance type is
$\displaystyle\mathrm{\Gamma}^{\prime}_{\leq};{{tl}}\\!:\\!{t_{y}}$
$\displaystyle\ \vdash\
{\texttt{OC}[\alpha]}\Rightarrow{{{z}}\\!:\\!{\alpha}}\rightarrow{{{{zs}}\\!:\\!{{\texttt{OL}}[{{\alpha}{{{\\{{{\nu}\\!:\\!{{z}\leq\nu}}\\}}}}}]}}\rightarrow{{\texttt{OL}^{+}}[{\alpha,{zs}}]}}$
(7.8)

As $\mathrm{\Gamma}({x})=\alpha$ we trivially get that the first argument
${x}$ is a subtype of the first input type $\alpha$. Similarly from the
binding ${{tl}}\\!:\\!{t_{y}}$, the second argument ${tl}$ is a subtype of the
second input type
${\texttt{OL}}[{{\alpha}{{{\\{{{\nu}\\!:\\!{{x}\leq\nu}}\\}}}}}]$, after
substituting the parameter ${z}$ for the actual ${x}$. Hence, by Syn-App and
the type of the constructor (7.8), we arrive at our destination (7.6).
$\square$

$\textrm{{Type Synthesis}}\hfill\framebox{$\mathrm{\Gamma}\vdash e\Rightarrow
t$}$

$\displaystyle\displaystyle{\hbox{\hskip
19.76456pt\vbox{\hbox{\hskip-19.76454pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}(D)=t$}}}\vbox{}}}\over\hbox{\hskip
21.43117pt\vbox{\vbox{}\hbox{\hskip-21.43117pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
D\Rightarrow t$}}}}}}$Syn-Data

Figure 7.10: $\mathsf{\lambda_{\delta}}$: Rules for Type Synthesis

###  7.4 Verification Conditions

The declarative rules for checking destructor types and synthesizing
constructor types readily translate to an algorithm for verification condition
generation.

_Subtyping_ The subtyping constraint for two polymorphic datatypes types
follows the rule Sub-Data. As shown in fig. 7.11, the constraint is the
conjuction of the constraint generated by the top-level refinements of the
data types ($c_{o}$), the positive ($c_{p}$) and negative ($c_{n}$) type
components.

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{sub}&:&(T\times T)\rightarrow
C\\\
\hline\cr\mathsf{sub}({{C}[{\overline{s}}]}{{{\\{{{\nu_{1}}\\!:\\!{p_{1}}}\\}}}},\
{{C}[{\overline{t}}]}{{{\\{{{\nu_{2}}\\!:\\!{p_{2}}}\\}}}})&\doteq&c_{o}\wedge
c_{p}\wedge c_{n}\\\ \quad\mbox{where}&&\\\
\quad\quad\overline{p}&=&\mathsf{polarities}(\delta,\ C)\\\ \quad\quad
c_{o}&=&\forall{{\nu_{1}}\\!:\\!{b}}.\
{p_{1}}\Rightarrow{{p_{2}}[\nu_{2}:=\nu_{1}]}\\\ \quad\quad
c_{p}&=&\bigwedge_{\forall i.p_{i}\in\\{+,\pm\\}}\mathsf{sub}(s_{i},\
t_{i})\\\ \quad\quad c_{n}&=&\bigwedge_{\forall
i.p_{i}\in\\{-,\pm\\}}\mathsf{sub}(t_{i},\ s_{i})\\\\[3.61371pt]
\hline\cr\hline\cr\end{array}$ Figure 7.11: Subtyping Constraints for
$\mathsf{\lambda_{\delta}}$, extends cases of fig. 6.6

_Checking_ Recall that the $\mathsf{check}$ function takes an environment
$\mathrm{\Gamma}$, term $e$ and type $t$ and returns a Horn constraint $c$
whose satisfiability implies $\mathrm{\Gamma}\vdash e\Leftarrow t$ (3.4.3).
Figure 7.12 shows how we extend the function to account for destructor
(pattern-match) terms $\texttt{{switch}}\;y\;\\{\overline{a}\\}$ by invoking
$\mathsf{checkAlt}(\mathrm{\Gamma},\ y,\ a,\ t)$ which implements rule Chk-Swt
by computing the conjunction of the constraints for _each_ alternative. Thus,
the hard work is done by $\mathsf{checkAlt}(\mathrm{\Gamma},\ y,\
{D}({\overline{z}})\rightarrow{e},\ t)$ which implements rule Chk-Alt. To do
so, $\mathsf{checkAlt}$ first obtains the data constructor’s type $s$ at this
instance. Next, it uses $\mathsf{unapply}(\mathrm{\Gamma},\ y,\ \overline{z},\
s)$ to obtain the environment $\mathrm{\Gamma}^{\prime}$ extended with types
for the pattern binders. Finally, it recursively invokes
$\mathsf{check}(\mathrm{\Gamma}^{\prime},\ e,\ t)$ to recursively compute the
constraint for the pattern-expression under the extended environment.

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{check}&:&(\mathrm{\Gamma}\times
E\times T)\rightarrow C\\\ \hline\cr\mathsf{check}(\mathrm{\Gamma},\
\texttt{{switch}}\;y\;\\{\overline{a}\\},\
t)&\doteq&\bigwedge_{a\in\overline{a}}\ \mathsf{checkAlt}(\mathrm{\Gamma},\
y,\ a,\ t)\\\\[3.61371pt]
\hline\cr\hline\cr\mathsf{checkAlt}&:&(\mathrm{\Gamma}\times X\times A\times
T)\rightarrow C\\\ \hline\cr\mathsf{checkAlt}(\mathrm{\Gamma},\ y,\
{D}({\overline{z}})\rightarrow{e},\
t)&\doteq&({\overline{{z::s}}})\Rightarrow({{y::s^{\prime}}})\Rightarrow c\\\
\quad\mbox{where}&&\\\ \quad\quad
c&=&\mathsf{check}(\mathrm{\Gamma}^{\prime},\ e,\ t)\\\
\quad\quad\mathrm{\Gamma};{\overline{{z}\\!:\\!{s}};{y}\\!:\\!{s^{\prime}}}\
\mbox{as}\ \mathrm{\Gamma}^{\prime}&=&\mathsf{unapply}(\mathrm{\Gamma},\ y,\
\overline{z},\ s)\\\ \quad\quad s&=&\mathsf{ctor}(\mathrm{\Gamma},\ y,\
D)\\\\[3.61371pt] \hline\cr\hline\cr\mathsf{synth}&:&(\mathrm{\Gamma}\times
E)\rightarrow(C\times T)\\\ \hline\cr\mathsf{synth}(\mathrm{\Gamma},\
D)&\doteq&(\mathit{true},\ \mathrm{\Gamma}(D)=t)\\\\[3.61371pt]
\hline\cr\hline\cr\end{array}$ Figure 7.12: Verification Condition Generation
for $\mathsf{\lambda_{\delta}}$, extends cases of fig. 6.6

_Synthesis_ The function $\mathsf{synth}$, shown in fig. 7.12, implements rule
Syn-Data by returning the environment’s (polymorphic) type for the constructor
$D$. This lets us then handle constructor applications just like plain
function applications.

$\displaystyle c\ \doteq\ $ $\displaystyle\forall{x},\ {ys}.$
$\displaystyle\quad\forall{y},\ {ys^{\prime}}.\
\texttt{len}({{ys}})=1+\texttt{len}({{ys^{\prime}}})\ \Rightarrow$
$\displaystyle\quad\quad{x}\leq{y}\ \Rightarrow c_{y}\ \wedge$
$\displaystyle\quad\quad\quad\forall{tl}.\
\texttt{len}({{tl}})=1+\texttt{len}({{ys^{\prime}}})\ \Rightarrow\ c_{x}\
\wedge$ $\displaystyle\quad\quad\quad\quad\forall\nu.\
\texttt{len}({\nu})=1+\texttt{len}({{tl}})\Rightarrow\texttt{len}({\nu})=1+\texttt{len}({{ys}})$
$\displaystyle\quad\wedge{x}\not\leq{y}\ \Rightarrow\ \ldots\mbox{(constraint
for $\texttt{{else}}$ branch)}$ $\displaystyle\wedge\ldots\mbox{(constraint
for $\texttt{ON}$ case)}$ $\displaystyle c_{y}\ \doteq\ $
$\displaystyle\forall{\nu}.\ \nu={y}\ \Rightarrow\ \kappa_{y}({\nu})\ \wedge$
$\displaystyle\forall{\nu}.\ {y}\leq\nu\ \Rightarrow\
(\kappa_{y}({\nu})\wedge{y}\leq\nu)$ $\displaystyle c_{x}\ \doteq\ $
$\displaystyle\forall{\nu}.\ \nu={x}\ \Rightarrow\ \kappa_{x}({\nu})\ \wedge$
$\displaystyle\forall{\nu}.\ \kappa_{y}({\nu})\ \Rightarrow\
(\kappa_{x}({\nu})\wedge{x}\leq\nu)$ Figure 7.13: Verification Condition for
definition of insert (fig. 7.1).

Example: VC for insert Figure 7.13 shows a part of the VC generated by
invoking $\mathsf{check}$on the environment $\mathrm{\Gamma}$, the definition
of insert from fig. 7.8 – with the type applications replaced with holes
${\alpha}{{\\{{\star}\\}}}$ – and the goal type $t_{\texttt{ins}}$. (The
abbreviations $\mathrm{\Gamma}$ and $t_{\texttt{ins}}$ are shown in fig. 7.9.)
The VC generation recurses into the body, to generate two constraints for the
“cons” and “nil” cases respectively. The latter is elided for brevity. The
former adds the pattern match binders for $y$ and $ys^{\prime}$ and adds the
hypothesis that the size of $ys$ is one more than that of $ys^{\prime}$. We
then recurse into the if-expression: with one sub-constraint for the then
branch (with the hypothesis ${x}\leq{y}$) and a second for the else branch,
elided for brevity. Recall that the then-expression is

$\texttt{{let}}\;{tl}=e_{y}\;\texttt{{in}}\;e_{x}$

Where $e_{y}$ and $e_{x}$ are the two constructor applications in fig. 7.9.
The then-constraint has a sub-constraint $c_{y}$ that arises from calling
$\mathsf{synth}$ on $e_{y}$ and which also produces the hypothesis that the
size of $tl$ is one more than that of $ys^{\prime}$. Similarly, we then again
invoke $\mathsf{synth}$ on $e_{x}$ to get $c_{x}$ and the result type: a list
$\nu$ whose length is one more than ${tl}$ which must then imply the post-
condition, that the output $\nu$’s size is in fact, one greater than the input
$ys$.

Next, lets look at the constraint $c_{y}$ shown in fig. 7.13, returned by
$\mathsf{synth}$ on the constructor application term

$e_{{y}}\ \doteq\
{{\texttt{OC}[{\alpha}{{\\{{\star}\\}}}]}\;{{y}}}\;{{ys^{\prime}}}$

As described in section 6.4, we generate a fresh template
${\alpha}{{{\\{{{\nu}\\!:\\!{\kappa_{y}({\nu})}}\\}}}}$ for the hole, which
means that at this site, the constructor OC has the following type (analogous
to that shown in (7.7), except with $\kappa_{y}({\nu})$ instead of the to-be-
inferred refinement ${x}\leq\nu$:)

${{{z}}\\!:\\!{{\alpha}{{{\\{{{\nu}\\!:\\!{\kappa_{{y}}({\nu})}}\\}}}}}}\rightarrow{{{{zs}}\\!:\\!{{\texttt{OL}}[{{\alpha}{{{\\{{{\nu}\\!:\\!{\kappa_{{y}}({\nu})\wedge{z}\leq\nu}}\\}}}}}]}}\rightarrow{{\texttt{OL}^{+}}[{{{\alpha}{{{\\{{{\nu}\\!:\\!{\kappa_{{y}}({\nu})}}\\}}}}},{zs}}]}}$

Thus, $c_{y}$ has two conjuncts, one each for the subtyping obligations for
the inputs ${y}$, ${ys^{\prime}}$. The first conjunct ensures that the first
argument ${y}$ is indeed a subtype of the constructor’s first input. The
second conjunct checks that the second input ${ys^{\prime}}$ whose type, per
$\mathsf{unapply}$ is
${\texttt{OL}}[{{\alpha}{{{\\{{{\nu}\\!:\\!{{y}\leq\nu}}\\}}}}}]$ (as shown in
$\mathrm{\Gamma}^{\prime}_{\leq}$ in fig. 7.9) is a subtype of the second
input of the constructor.

Finally, lets consider the constraint $c_{x}$ shown in fig. 7.13 that is
returned by $\mathsf{synth}$ on the constructor application term

$e_{{x}}\ \doteq\ {{\texttt{OC}[{\alpha}{{\\{{\star}\\}}}]}\;{{x}}}\;{{tl}}$

Again, we generate a fresh template for the hole
${\alpha}{{{\\{{{\nu}\\!:\\!{\kappa_{x}({\nu})}}\\}}}}$ which means that at
this site, the constructor OC has the type

${{{z}}\\!:\\!{{\alpha}{{{\\{{{\nu}\\!:\\!{\kappa_{{x}}({\nu})}}\\}}}}}}\rightarrow{{{{zs}}\\!:\\!{{\texttt{OL}}[{{\alpha}{{{\\{{{\nu}\\!:\\!{\kappa_{{x}}({\nu})\wedge{z}\leq\nu}}\\}}}}}]}}\rightarrow{{\texttt{OL}^{+}}[{{{\alpha}{{{\\{{{\nu}\\!:\\!{\kappa_{{x}}({\nu})}}\\}}}}},{zs}}]}}$

Hence, the constructor application yields the constraint $c_{{x}}$ with one
conjunct for each of the input arguments $x$ and $tl$. As the output type of
the _first_ constructor application, and so the type of $tl$ is
${{\texttt{OL}^{+}}[{{{\alpha}{{{\\{{{\nu}\\!:\\!{\kappa_{{y}}({\nu})}}\\}}}}},{ys^{\prime}}}]}$
the second conjunct of $c_{{x}}$ – which represents the subtyping obligation
for the input argument $tl$ – has the antecedent $\kappa_{{y}}({\nu})$.

_Solution_ We encourage the reader to verify that the assignment

$\displaystyle\kappa_{{y}}({\nu})$ $\displaystyle\ \doteq\ {x}\leq\nu$
$\displaystyle\kappa_{{x}}({\nu})$ $\displaystyle\ \doteq\ \mathit{true}$

satisfies the Horn constraint in fig. 7.13, by yielding, after substitution, a
valid VC, thereby verifying that insert implements $t_{\texttt{ins}}$.
$\square$

###  7.5 Discussion

To sum up, in this chapter we saw how to extend the language to support
refinements on user defined algebraic data-types. We saw how to encode three
classes of properties – invariants of individual datum, properties relating
multiple data, and properties of the structure itself – using a single
mechanism: a refined type for the data constructors. This approach lets us
reuse the rules for function _application_ to _generalize_ properties when
_constructing_ the structure. Dually, it lets us define a notion of _un-
application_ to let us _instantiate_ properties when _destructing_ the
structure.

_Refinements on Data vs. Type Constructors_ Our approach is using refinements
of data constructors. An alternative approach would be to refine type
constructors. For example, the ordered lists of section 7.1.2 could be
alternatively defined as list int {l: isOrdered l}, where isOrdered is a
boolean function that checks is the input list is ordered. [Igarashi15]
compare the two alternative approaches and conclude that refinements of type
constructors are easier for the programmer to _specify_ , but refinements on
data constructors are much easier to (automatically) _verify_.

_Types as a Decision Procedure_ The ease of verification arises from the fact
that refined data constructors give rise to a simple syntax-directed approach
to establish invariants of complex heap-allocated data structures. Crucially,
this approach does not require the expensive blur and materialize mechanisms
of shape analysis [SagivRepsWilhelm02j], or the undecidable (universal)
quantifier-based reasoning used by Floyd-Hoare logic based deductive verifiers
like Dafny [dafny]. Instead, _subtyping_ provides a syntactic proof system for
checking entailment between quantfied assertions. Subtyping lets us prove the
(quantified) assertion that if every element of a list is positive then every
element is non-negative, by proving the (quantifier-free) assertion that if
$\nu$ is positive then $\nu$ is non-negative. Similarly, the constructor
application is a syntactic heuristic for generalizing facts about individual
elements into facts about the whole structures: e.g. if x is a nat and xs is a
list(nat), then Cons(x, xs) is a list(nat). Finally, the destructor sites
provide a syntactic heuristic for instantiating quantified facts about the
whole structure: e.g. if xs is a list(nat) and is destructed to Cons(x, xs’)
then x is a nat.

_Refinements for Pointer-based Structures_ While this chapter develops this
ideas for a purely functional language, related ideas have been proposed for
imperative languages. Notable examples include [Madhu2013] which introduces
the idea of “Natural Proofs” which shows how separation-logic based verifiers
need only fold and unfold recursive predicates (which encode the same
information as our recursive types) at the equivalent of constructor
application and destruction sites, and [Bakst16] which shows how to add
refinements to an alias type system [AliasTypesRec] that precisely tracks
locations and aliasing, yielding an expressive and automated way to reason
about invariants of pointer-based data structures.

##  Chapter 8 Refinement Polymorphism

Modern programming languages allow code and data to abstract over the concrete
types that they work with. For example, it is commonplace to define
polymorphic arrays or hash-tables that can, e.g. hold int or string or other
values, and to write type-agnostic functions that operate over these
structures. In § 6 we saw how polymorphic types could be instantiated at
different use-sites to precisely track invariants in a context-sensitive
manner.

However, we also often write monomorphic functions and data that nevertheless
abstract over the refinements satisfied by the data they manipulate. This
abstraction is often implicit, i.e. not captured in the function’s type
specification, which makes it hard to establish the invariants at usage sites.
Hence, next, lets develop a means for specifying signatures that abstract over
the refinements, see how to automatically verify these signatures, and learn
how to instantiate them automatically at client sites, all while keeping
verification efficiently decidable.

###  8.1 Examples

Lets crack our knuckles with some illustrative examples.

####  8.1.1 Problem: Picking the Right Specification

Consider maxI(x,y) which returns the larger of x and y.

⬇

val maxI : int => int => int

let maxI = (x, y) => {

if (x < y) { y } else { x }

};

Suppose that we want to verify that maxI(a, b) must be non-negative if a and b
are non-negative.

⬇

val bigger: nat => nat => nat

let bigger = (a, b) => { maxI(a, b) };

Unfortunately, the above bigger will _fail_ as the specified type is silent
about what properties hold of the int returned by maxI!

_Premature Specialization_ We could try to type maxI as

⬇

val maxI : nat => nat => nat

This signature would let us verify bigger but would prematurely restrict maxI
to non-negative values. For example, if we had a refinement for valid 8-bit
ints

⬇

type int8 = int[v|0 <= v && v < 256]

we would end up _rejecting_ the perfectly correct

⬇

val brighter : int8 => int8 => int8

let brighter = (c1, c2) => {

maxI(c1, c2)

}

Instead, we might specify that the output

⬇

val maxI: x:int => y:int => int[v|v=x || v=y]

This would let us verify bigger and brighter. This approach suffices when
there are just two int inputs but does not scale up to unbounded collections,
as in maxL which computes the largest element of a _list_

⬇

let rec maxL = (default, xs) => {

fold_right(maxI, default, xs)

};

Since the list is unbounded we have no way to say the output is _one of_ the
elements of xs. We could use an _existential quantifier_ but that would lead
to verification conditions that are outside the boundaries of decidable SMT
based validity checking. Now suppose we use maxL with different kinds of
values, for example:

⬇

val biggerL : list(nat) => nat

let biggerL = (xs) => { maxL(0, xs) }

val brighterL : list(int8) => int8

let brighterL = (xs) => { maxL(0, xs) }

How can we verify that maxList returns a nat or int8 values when invoked with
lists of nat and int8 values respectively?

####  8.1.2 Solution: Abstracting Over Refinements

If we take a step back, we might notice that the fact that maxI returns _one
of_ its two inputs x and y can be rephrased as follows: if there is some
property $p$ that _both_ inputs satisfy, then the output must also satisfy
$p$. That is, we can make the refinement $p$ itself be a _parameter_ in the
specification of maxI

⬇

val maxI: int[v|p v] => int[v|p v] => int[v|p v]

The above specification says that _for any_ predicate p over int values, maxI
takes two inputs x and y which respectively satisfy p x and p y and returns an
output v that satisfies p v.

It is only useful to parameterize over refinements if there is some convenient
way to _instantiate_ the parameters. We will extend the machinery for
inferring refinements for holes ${\\{{\star}\\}}$ to automatically instantiate
the refinement parameters at the usage-sites — e.g. in bigger and brighter —
where p will be instantiated to the concrete refinements

$\displaystyle p_{\texttt{nat}}$ $\displaystyle\doteq\ \lambda\nu.\ 0\leq\nu$
(8.1) $\displaystyle p_{\texttt{int8}}$ $\displaystyle\doteq\ \lambda\nu.\
0\leq\nu\wedge\nu<256$ (8.2)

thereby verifying those two client functions.

The above method scales up to unbounded lists. We can specify

⬇

val maxL: int[v|p v] => list(int[v|p v]) => int[v|p v]

which says that when maxL is given a _default_ int and a list(int) all of
which satisfy the predicate p, the output is also an int that satisfies p.
Once again, we can verify the clients biggerL and brighterL by instantiating p
as $p_{\texttt{nat}}$ and $p_{\texttt{int8}}$ at the respective call-sites.

_Preserving Decidability_ At first glance, it may appear that these abstract
predicate variables p have taken us into the realm of higher-order logics, and
that we must leave decidable SMT based checking at the door. Fortunately, that
is not the case. We will see how to encode abstract refinements p as
_uninterpreted functions_ in the refinement logic, which will allow us to
continue with SMT based Horn VC checking.

####  8.1.3 Abstracting Refinements over Data Types

Refinement parameters are a natural fit for _datatype_ definitions.

_Dependent Pairs_ For example, we can specify a pair datatype where there is
some relationship between the first and second component, by parameterizing
the datatype definition with a refinement parameter p:

⬇

type pair(’a, ’b)(p : ’a => ’b => bool) =

| MkPair(x:’a, y:’b[v|p x v])

The definition is parameterized by a binary predicate p that relates the two
elements of the pair. Hence, we can define the set of int pairs where the
second component exceeds the first as:

⬇

type incPair = pair(int,int)((x, y) => x < y)

The refinement parameter is _asserted_ when the pair is _constructed_. Hence,
okPair will verify but badPair will be rejected:

⬇

val okPair: n:int => incPair

let okPair = (n) => { MkPair(n, n+1) };

val badPair: x:int => incPair

let badPair = (n) => { MkPair(n, n-1) };

Dually, the refinement is _assumed_ when the pair is _destructed_ , and so the
below verifies:

⬇

val chkPair : incPair => nat

let chkPair = (p) => {

switch (p) {

MkPair(x1, x2) => x2 - x1

}

};

_Abstracting Refinements over Lists_ The combination of recursion and
refinement parameters allows us to compactly specify various interesting
properties of collections without baking them into the datatype’s definition.
Recall the definition of ordered lists of non-decreasing values from section
7.1

⬇

type olist(’a) =

| ONil

| OCons (x:’a, xs:olist(’a[v|x<=v]))

Order is established by the signature for OCons that requires that every
element of the tail xs is greater than the head x. Refinement parameters let
us abstract the particular relation: we can specify a generic list as

⬇

type list(’a)(p:’a =>’a => bool) =

| Nil

| Cons(x:’a, xs:list(’a[v|p x v])((y,z) => p y z))

The definition is parameterized by a binary predicate p that relates _every_
element of the tail with the head x at each application of the constructor
Cons. That is, the specification says that if

$\texttt{Cons}(x_{1},\texttt{Cons}(x_{2},\ldots\texttt{Cons}(x_{n},\texttt{Nil}))):\texttt{list}{(\alpha)}(p)$

then for each $1\leq i<j\leq n$ we have $p(x_{i},x_{j})$.

_Ordered Lists_ We can now specify non-decreasing lists by instantiating the
refinement parameter p appropriately:

⬇

type incList(’a) = list(’a)((x1, x2) => x1<=x2)

val checkInc : (int) => incList(int)

let checkInc = (x) => {

Cons(x, Cons(x+1, Cons(x+2, Nil)))

};

Similarly, we can define non-increasing lists

⬇

type decList(’a) = list(’a)((x1,x2) => x1>=x2)

val checkDec : (int) => decList(int)

let checkDec = (x) => {

Cons(x+2, Cons(x+1, Cons(x, Nil)))

};

or _duplicate-free_ lists, simply by changing the relation:

⬇

type uniqList(’a) = list(’a)((x1,x2) => x1!=x2)

val checkUnique : (int) => uniqList(int)

let checkUnique = (x) => {

Cons(x+2, Cons(x, Cons(x+1, Nil)))

};

We can omit the refinement instantiation to write just list(’a) to denote the
trivially (un)refined instance list(’a)((x1,x2) => true). Now, the machinery
developed for reasoning about datatypes in section 7.1 lets us verify
properties of code manipulating (abstractly) refined lists, e.g. that the
following insertion-sort produces ordered lists

⬇

val isort : list(’a) => incList(’a)

let isort = (xs) => {

foldr(insert, Nil, xs);

};

###  8.2 Types and Terms

Figure 8.1 summarizes how we extend the language of types to include
abstraction over refinements, and the language of terms to include
instantiation of refinement variables.

_Refinement Variables_ We write $\rho$ to denote refinement variables that
abstract over concrete or specific refinements. Refinement variables $\rho$
are of the form ${\kappa}\\!:\\!{{\overline{b}}\rightarrow{\texttt{bool}}}$,
i.e. represent a bool valued _predicates_ over some (non-empty) sequence of
base types.

_Abstracting over Refinements_ We abstract over refinements either in function
signatures of the form $\forall{\rho}.\ {t}$ or in data type definitions
$\langle{C},\;\overline{{\alpha}\\!:\\!{k}/{p}},\;\overline{{\rho}/{p}},\;{\overline{{D}\\!:\\!{t}}}\rangle$
which are now parameterized by a (possibly empty) sequence of refinement
variables and their respective polarities in addition to type variables from
Figure 7.2. For example, we might assign maxI the type

$t_{\texttt{maxI}}\ \doteq\
\forall{{\kappa}\\!:\\!{{\texttt{{int}}}\rightarrow{\texttt{bool}}}}.\
{{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}}\rightarrow{{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}}\rightarrow{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}}}}$
(8.3)

which captures the intuition that when given two
${\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}$ inputs, the
function is guaranteed to return an
${\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}$ output, for any
refinement $\kappa$ on int values. In the sequel, we will elide the refinement
variables’ sort when it is clear from the context.

_Implicit Refinement Application_ We instantiate refinements either in
_refinement application_ terms of the form $e[\star]$ or in _type-constructor
application_ types of the form ${C}[{\overline{t}}](\overline{\varphi})$,
where $\varphi$ is a _concrete refinement_
$\lambda{\overline{{x}\\!:\\!{b}}}.\ {p}$ which is a boolean valued predicate
over a set of variables $\overline{{x}\\!:\\!{b}}$. We leave the refinement
instances _implicit_ for terms (denoted by $\star$) as, like type instances,
these are ubiquitous, and hence, should be automatically synthesized. For
example, brighter is defined via the following term in which the refinement
variable in the signature of maxI is implicitly instantiated at the usage
site:

$\texttt{{let}}\ \texttt{brighter}\ =\ \lambda{x,y}.\ {\
{{\texttt{maxI}[\star]}\;{x}}\;{y}}$ (8.4)

_Explicit Refinement Application_ However, we allow _explicit_ refinement
instances for data types as we often want to specify signatures where the
constructor is refined with a particular concrete refinement. For example, the
definitions of incPair, incList, and decList from section 8.1 are,
respectively:

typeincPair
$\displaystyle=\texttt{pair}{(\texttt{{int}},\texttt{{int}})}(\lambda{x_{1},x_{2}}.\
{x_{1}<x_{2}})$ (8.5) typeincList
$\displaystyle=\texttt{list}{(\texttt{{int}})}(\lambda{x_{1},x_{2}}.\
{x_{1}\leq x_{2}})$ (8.6) typedecList
$\displaystyle=\texttt{list}{(\texttt{{int}})}(\lambda{x_{1},x_{2}}.\
{x_{1}\geq x_{2}})$ (8.7)

_Ref. Var._ | $\rho$ | $\vcentcolon\vcentcolon=$ | ${\kappa}\\!:\\!{{\overline{b}}\rightarrow{\texttt{bool}}}$ |
---|---|---|---|---
_Abs. Refine._ | $\varphi$ | $\vcentcolon\vcentcolon=$ | $\lambda{\overline{{x}\\!:\\!{b}}}.\ {p}$ |
_Datatypes_ | $\delta$ | $\vcentcolon\vcentcolon=$ | $\langle{C},\;\overline{{\alpha}\\!:\\!{k}/{p}},\;\overline{{\rho}/{p}},\;{\overline{{D}\\!:\\!{t}}}\rangle$ |
_Basic Types_ | $b$ | $\vcentcolon\vcentcolon=$ | $\ldots$ | _from Fig. 7.2_
|  | $\ \mid\ $ | ${C}[{\overline{t}}](\overline{\varphi})$ | _datatypes_
_Types_ | $t$ | $\vcentcolon\vcentcolon=$ | … | _from $\mathsf{\lambda_{\delta}}$ Fig. 7.2_
|  | $\ \mid\ $ | $\forall{\rho}.\ {t}$ | _ref. polymorphism_
_Terms_ | $e$ | $\vcentcolon\vcentcolon=$ | $\ldots$ | _from $\mathsf{\lambda_{\delta}}$ Fig. 7.2_
|  | $\ \mid\ $ | $e[\star]$ | _refinement application_
Figure 8.1: $\mathsf{\lambda_{\delta}}$: Syntax of Types and Terms

###  8.3 Declarative Typing

Next, lets look at how the declarative typing rules are extended to accomodate
abstract refinements.

####  8.3.1 Well-formedness

$\textrm{{Well-formedness}}\hfill\framebox{$\mathrm{\Gamma}\vdash t:k$}$

$\displaystyle\displaystyle{\hbox{\hskip
37.51616pt\vbox{\hbox{\hskip-37.51616pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{{\kappa}\\!:\\!{{\overline{b}}\rightarrow{\texttt{bool}}}}\vdash
t:k$}}}\vbox{}}}\over\hbox{\hskip
40.58914pt\vbox{\vbox{}\hbox{\hskip-40.58913pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\forall{{\kappa}\\!:\\!{{\overline{b}}\rightarrow{\texttt{bool}}}}.\
{t}:\star$}}}}}}$Wf-RAbs

Figure 8.2: $\mathsf{\lambda_{\rho}}$: Rules for Well-formedness

Rule Wf-RAbs shown in fig. 8.2 states that a refinement polymorphic type is
well-formed with kind $\star$, if the underlying (quantified) type is also
well-formed.

####  8.3.2 Subtyping

$\textrm{{Abs. Refinement
Implication}}\hfill\framebox{$\mathrm{\Gamma}\vdash\varphi_{1}\prec:\varphi_{2}$}$

$\displaystyle\displaystyle{\hbox{\hskip
37.34518pt\vbox{\hbox{\hskip-37.34517pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{\overline{{x_{1}}\\!:\\!{b}}}\vdash
p_{1}\Rightarrow{p_{2}}[\overline{x_{2}}:=\overline{x_{1}}]$}}}\vbox{}}}\over\hbox{\hskip
42.34511pt\vbox{\vbox{}\hbox{\hskip-42.34511pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\lambda{\overline{{x_{1}}\\!:\\!{b}}}.\
{p_{1}}\prec:\lambda{\overline{{x_{2}}\\!:\\!{b}}}.\ {p_{2}}$}}}}}}$Sub-CRef

$\textrm{{Subtyping}}\hfill\framebox{$\mathrm{\Gamma}\vdash
t_{1}\prec:t_{2}$}$

$\displaystyle\displaystyle{\hbox{\hskip
153.19324pt\vbox{\hbox{\hskip-153.19322pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
s_{i}\prec:t_{i}\ \mbox{for each}\ i.p_{i}\in\\{+,\pm\\}$}\hskip
20.00003pt\hbox{\hskip-151.43466pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
t_{i}\prec:s_{i}\ \mbox{for each}\ i.p_{i}\in\\{-,\pm\\}$}\hskip
20.00003pt\hbox{\hskip-152.36201pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\phi_{i}\prec:\varphi_{i}\
\mbox{for each}\ i.p_{ri}\in\\{+,\pm\\}$}\hskip
20.00003pt\hbox{\hskip-142.88881pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\varphi_{i}\prec:\phi_{i}\
\mbox{for each}\ i.p_{ri}\in\\{-,\pm\\}$}\hskip
20.00003pt\hbox{\hskip-128.38687pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{{\nu_{1}}\\!:\\!{{{\\{{{{C}[{\overline{s}}]}\\!:\\!{p_{1}}}\\}}}}}\vdash{p_{2}}[\nu_{2}:=\nu_{1}]\qquad(\overline{p},\overline{p_{r}})=\mathsf{polarities}(\delta,\
C)$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\
$}}}}}}}}}}}}\vbox{\hbox{\hskip-151.43466pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
t_{i}\prec:s_{i}\ \mbox{for each}\ i.p_{i}\in\\{-,\pm\\}$}\hskip
20.00003pt\hbox{\hskip-152.36201pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\phi_{i}\prec:\varphi_{i}\
\mbox{for each}\ i.p_{ri}\in\\{+,\pm\\}$}\hskip
20.00003pt\hbox{\hskip-142.88881pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\varphi_{i}\prec:\phi_{i}\
\mbox{for each}\ i.p_{ri}\in\\{-,\pm\\}$}\hskip
20.00003pt\hbox{\hskip-128.38687pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{{\nu_{1}}\\!:\\!{{{\\{{{{C}[{\overline{s}}]}\\!:\\!{p_{1}}}\\}}}}}\vdash{p_{2}}[\nu_{2}:=\nu_{1}]\qquad(\overline{p},\overline{p_{r}})=\mathsf{polarities}(\delta,\
C)$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\
$}}}}}}}}}}\vbox{\hbox{\hskip-152.36201pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\phi_{i}\prec:\varphi_{i}\
\mbox{for each}\ i.p_{ri}\in\\{+,\pm\\}$}\hskip
20.00003pt\hbox{\hskip-142.88881pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\varphi_{i}\prec:\phi_{i}\
\mbox{for each}\ i.p_{ri}\in\\{-,\pm\\}$}\hskip
20.00003pt\hbox{\hskip-128.38687pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{{\nu_{1}}\\!:\\!{{{\\{{{{C}[{\overline{s}}]}\\!:\\!{p_{1}}}\\}}}}}\vdash{p_{2}}[\nu_{2}:=\nu_{1}]\qquad(\overline{p},\overline{p_{r}})=\mathsf{polarities}(\delta,\
C)$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\
$}}}}}}}}\vbox{\hbox{\hskip-142.88881pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\varphi_{i}\prec:\phi_{i}\
\mbox{for each}\ i.p_{ri}\in\\{-,\pm\\}$}\hskip
20.00003pt\hbox{\hskip-128.38687pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{{\nu_{1}}\\!:\\!{{{\\{{{{C}[{\overline{s}}]}\\!:\\!{p_{1}}}\\}}}}}\vdash{p_{2}}[\nu_{2}:=\nu_{1}]\qquad(\overline{p},\overline{p_{r}})=\mathsf{polarities}(\delta,\
C)$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\
$}}}}}}\vbox{\hbox{\hskip-128.38687pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{{\nu_{1}}\\!:\\!{{{\\{{{{C}[{\overline{s}}]}\\!:\\!{p_{1}}}\\}}}}}\vdash{p_{2}}[\nu_{2}:=\nu_{1}]\qquad(\overline{p},\overline{p_{r}})=\mathsf{polarities}(\delta,\
C)$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\
$}}}}\vbox{}}}}}}}\over\hbox{\hskip
73.22531pt\vbox{\vbox{}\hbox{\hskip-73.22531pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash{{C}[{\overline{s}}](\overline{\phi})}{{{\\{{{\nu_{1}}\\!:\\!{p_{1}}}\\}}}}\prec:{{C}[{\overline{t}}](\overline{\varphi})}{{{\\{{{\nu_{2}}\\!:\\!{p_{2}}}\\}}}}$}}}}}}$Sub-
Con

Figure 8.3: $\mathsf{\lambda_{\rho}}$: Rules for Subtyping

Figure 8.3 summarizes the new rules for subtyping. The rule Sub-CRef shows the
rule for checking subsumption between two concrete refinements
$\lambda{\overline{{x_{1}}\\!:\\!{b}}}.\ {p_{1}}$ and
$\lambda{\overline{{x_{2}}\\!:\\!{b}}}.\ {p_{2}}$, by checking that $p_{1}$ is
subsumed by $p_{2}$ after suitably renaming the bound variables. The second
rule Sub-Con shows how to extend the rule for checking subtyping between two
refined instances
${{C}[{\overline{s}}](\overline{\phi})}{{{\\{{{\nu_{1}}\\!:\\!{p_{1}}}\\}}}}$
and
${{C}[{\overline{t}}](\overline{\varphi})}{{{\\{{{\nu_{2}}\\!:\\!{p_{2}}}\\}}}}$
of a type constructor $C$, by checking the subsumption holds between the
corresponding concrete refinements $\phi$ and $\varphi$ of the two instances
according to their polarity using Sub-CRef, and checking the subsumption of
the base refinements $p_{1}$ and $p_{2}$ and type components as before.

Example: Subtyping in incPair As an example, let

$\displaystyle\mathrm{\Gamma}$
$\displaystyle\stackrel{{\scriptstyle\cdot}}{{=}}\ {a}\\!:\\!{\texttt{{int}}}$
$\displaystyle\varphi$ $\displaystyle\stackrel{{\scriptstyle\cdot}}{{=}}\
\lambda{x,y}.\ {x=a\wedge y=a+1}$ $\displaystyle\phi$
$\displaystyle\stackrel{{\scriptstyle\cdot}}{{=}}\ \lambda{x,y}.\ {x<y}$ and
consider the subtyping obligation $\displaystyle\mathrm{\Gamma}$
$\displaystyle\vdash\
{\texttt{pair}{(\texttt{{int}},\texttt{{int}})}(\varphi)}\ \prec:\
{\texttt{pair}{(\texttt{{int}},\texttt{{int}})}(\phi)}$ that could arise in
the course of checking that $\displaystyle\mathrm{\Gamma}$
$\displaystyle\vdash\ \texttt{MkPair}(a,a+1)\Leftarrow\texttt{incPair}$ where
incPair is defined in 8.5. Rule Sub-Con reduces the subtyping obligation to
the following concrete refinement subsumption $\displaystyle\mathrm{\Gamma}$
$\displaystyle\vdash\ \varphi\ \prec:\ \phi$ and then Sub-CRef reduces the
above to the entailment
$\displaystyle\mathrm{\Gamma},{x,y}\\!:\\!{\texttt{{int}}}$
$\displaystyle\vdash\ (x=a\wedge y=a+1)\ \Rightarrow\ (x<y)$

that is readily validated by the SMT solver. $\square$

####  8.3.3 Checking

$\textrm{{Type Checking}}\hfill\framebox{$\mathrm{\Gamma}\vdash e\Leftarrow
t$}$

$\displaystyle\displaystyle{\hbox{\hskip
147.30519pt\vbox{\hbox{\hskip-147.30519pt\hbox{\hbox{$\displaystyle\displaystyle\rho={\kappa}\\!:\\!{{\overline{b}}\rightarrow{\texttt{bool}}}\quad\varphi=\lambda{\overline{x}}.\
{f_{\kappa}(\overline{x})}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{{f_{\kappa}}\\!:\\!{{\overline{b}}\rightarrow{\texttt{bool}}}}\vdash{e}[\rho:=\varphi]\Leftarrow{s}[\rho:=\varphi]$}}}}\vbox{}}}\over\hbox{\hskip
30.1041pt\vbox{\vbox{}\hbox{\hskip-30.10408pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
e\Leftarrow\forall{\rho}.\ {s}$}}}}}}$Chk-RAbs

Figure 8.4: $\mathsf{\lambda_{\rho}}$: Rules for Type Checking

The rule Chk-RAbs checks that a term $e$ implements the abstractly refined
signature $\forall{\rho}.\ {s}$. The key idea is to use the refinement
variable $\rho={\kappa}\\!:\\!{{\overline{b}}\rightarrow{\texttt{bool}}}$ to
(1) generate a fresh _uninterpreted function symbol_ $f_{\kappa}$, (2)
substitute all occurrences of $\kappa$ with $f_{\kappa}$ in the term $e$ and
the type $s$, to respectively obtain ${e}[\kappa:=f_{\kappa}]$ and
${s}[\kappa:=f_{\kappa}]$ and then (3) perform the check on the substituted
type and term, in an environment extended with a binding for the uninterpreted
function $f_{\kappa}$.

_Refinement Instantiation_ We replace all occurences of the refinement
variable $\rho\doteq{\kappa}\\!:\\!{\cdot}$ with an uninterpreted function
$f_{\kappa}$ via an operation ${s}[\rho:=\varphi]$ shown in fig. 8.6 which
_instantiates_ (or _substitutes_) a concrete refinement $\varphi$ for a
refinement variable $\rho$ in a signature $s$. The operation traverses $s$ to
replace all occurences of $\kappa({\overline{x}})$ with
${p}[\overline{y}:=\overline{x}]$ when $\rho\doteq{\kappa}\\!:\\!{\cdot}$ and
$\varphi\doteq\lambda{\overline{y}}.\ {p}$, i.e. we replace the _parameters_
of the refinement ($\overline{y}$) with the _arguments_ ($\overline{x}$) in
the concrete refinement $p$.

Example: Checking maxI Recall the implementation and specification of maxI (§
8.1)

$\displaystyle e_{\texttt{maxI}}$ $\displaystyle\doteq\ \lambda{x,y}.\
{\texttt{{if}}\;x<y\;\texttt{{then}}\;{y}\;\texttt{{else}}\;x}$ (8.8)
$\displaystyle t_{\texttt{maxI}}$ $\displaystyle\doteq\ \forall{\kappa}.\
{{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}}\rightarrow{{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}}\rightarrow{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}}}}$
(8.9)

Lets consider the goal of verifying that the above implementation checks
against its specification (8.3)

$\emptyset\vdash\ e_{\texttt{maxI}}\Leftarrow t_{\texttt{maxI}}\\\ $ (8.10)

The rule Chk-RAbs reduces the above to

$\displaystyle\emptyset$ $\displaystyle\vdash\
e_{\texttt{maxI}}\Leftarrow{{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{f_{\kappa}(\nu)}}\\}}}}}\rightarrow{{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{f_{\kappa}(\nu)}}\\}}}}}\rightarrow{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{f_{\kappa}(\nu)}}\\}}}}}}}$
which rules Chk-Lam, Chk-If and Syn-Var reduce to two goals
$\displaystyle\mathrm{\Gamma}$ $\displaystyle\vdash\
{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\nu=x}}\\}}}}\ \prec:\
{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{f_{\kappa}(\nu)}}\\}}}}$
$\displaystyle\mathrm{\Gamma}$ $\displaystyle\vdash\
{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\nu=y}}\\}}}}\ \prec:\
{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{f_{\kappa}(\nu)}}\\}}}}$ where
$\mathrm{\Gamma}$ has bindings for the refinement and value parameters
$\displaystyle\mathrm{\Gamma}$ $\displaystyle\doteq\
{f_{\kappa}}\\!:\\!{{\texttt{{int}}}\rightarrow{\texttt{bool}}},{x}\\!:\\!{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{f_{\kappa}(\nu)}}\\}}}}},{y}\\!:\\!{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{f_{\kappa}(\nu)}}\\}}}}}$
The two goals above check that the specified output type is indeed returned in
each branch. Both the above reduce to the entailment
$\displaystyle\mathrm{\Gamma},{\nu}\\!:\\!{\texttt{{int}}}$
$\displaystyle\vdash\ \nu=y\ \Rightarrow\ f_{\kappa}(\nu)$

that is easily confirmed by the SMT solver. $\square$

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{ctor}&:&(\mathrm{\Gamma}\times
D\times X)\rightarrow T\\\ \hline\cr\mathsf{ctor}(\mathrm{\Gamma},\ D,\
y)&\doteq&{{s}[\overline{\alpha}:=\overline{t}]}[\overline{\rho}:=\overline{\varphi}]\\\\[3.61371pt]
\quad\mbox{where}&&\\\
\quad\quad{C}[{\overline{t}}](\overline{\varphi})&=&\mathrm{\Gamma}(y)\\\
\quad\quad\forall{{\overline{\alpha}}\\!:\\!{k}}.{\forall{\overline{\rho}}.\
{s}}&=&\mathrm{\Gamma}(D)\\\\[3.61371pt] \hline\cr\hline\cr\end{array}$ Figure
8.5: Meta-functions for Checking Alternatives; $\mathsf{unapply}$ as in Figure
7.6
$\begin{array}[]{rrcl}\textbf{\emph{\mbox{Predicates}}}&{\kappa({\overline{x}})}[\rho:=\varphi]&\doteq&{p}[\overline{y}:=\overline{x}]\
\mbox{if}\ \rho={\kappa}\\!:\\!{\cdot},\ \varphi=\lambda{\overline{y}}.\
{p}\\\ &{p_{1}\bowtie
p_{2}}[\rho:=\varphi]&\doteq&{p_{1}}[\rho:=\varphi]\bowtie{p_{2}}[\rho:=\varphi]\\\
&{p}[\rho:=\varphi]&\doteq&p\\\\[7.22743pt] \textbf{\emph{Abstr.
Refs}}&{(\lambda{\overline{{x}\\!:\\!{b}}}.\
{p})}[\rho:=\varphi]&\doteq&\lambda{\overline{{x}\\!:\\!{b}}}.\
{({p}[\rho:=\varphi])}\\\\[7.22743pt] \textbf{\emph{Base
Types}}&{{C}[{\overline{t}}](\overline{\phi})}[\rho:=\varphi]&\doteq&{C}[{\overline{{t}[\rho:=\varphi]}}](\overline{{\phi}[\rho:=\varphi]})\\\
&{b}[\rho:=\varphi]&\doteq&b\\\\[7.22743pt]
\textbf{\emph{Types}}&{{b}{{{\\{{{\nu}\\!:\\!{p}}\\}}}}}[\rho:=\varphi]&\doteq&{{b}[\rho:=\varphi]}{{{\\{{{\nu}\\!:\\!{{p}[\rho:=\varphi]}}\\}}}}\\\
&{({{x}\\!:\\!{s}}\rightarrow{t})}[\rho:=\varphi]&\doteq&{{x}\\!:\\!{{s}[\rho:=\varphi]}}\rightarrow{{t}[\rho:=\varphi]}\\\\[7.22743pt]
\end{array}$ Figure 8.6: Instantiating a refinement variable $\rho$ with a
concrete refinement $\varphi$.

_Checking Case Alternatives_ We continue to check case alternatives using Chk-
Alt from fig. 7.5. However, we must extend the definition of
$\mathsf{ctor}(\mathrm{\Gamma},\ D,\ y)$ — which defines the monomorphic
instantiation of the polymorphic type of the data constructor $D$
corresponding the case-scrutinee $y$ — to also account for refinement
polymorphism. This extension is summarized by the definition in fig. 8.5,
where we obtain both the monomorphic types $\overline{t}$ and additionally the
concrete refinements $\overline{\varphi}$ from the environment
$\mathrm{\Gamma}$ signature of $y$, and use those to respectively instantiate
the type ($\overline{\alpha}$) and refinement ($\overline{\rho}$) variables in
the signature of the data constructor $D$, where the latter is done via the
refinement instantiation mechanism described above.

Example: Checking chkPair Recall chkPair from § 8.1

$\displaystyle e$ $\displaystyle\doteq\ \lambda{p}.\
{\texttt{{switch}}\;p\;\\{{\texttt{MkPair}}({x,y})\rightarrow y-x\\}}$ Lets
see how the rules establish that $\displaystyle\emptyset$
$\displaystyle\vdash\
e\Leftarrow{\texttt{incPair}}\rightarrow{\texttt{{nat}}}$ First, Chk-Lam
reduces the above to $\displaystyle{p}\\!:\\!{\texttt{incPair}}$
$\displaystyle\vdash\
\texttt{{switch}}\;p\;\\{{\texttt{MkPair}}({x,y})\rightarrow
y-x\\}\Leftarrow\texttt{{nat}}$ Via Chk-Alt (fig. 7.5) we extend the
environment with the pattern-binders derived from $s\doteq\
\mathsf{ctor}({p}\\!:\\!{\texttt{incPair}},\ \texttt{MkPair},\ p)$ i.e. the
type of MkPair _at_ this instance. As MkPair $\displaystyle::\
\forall{{\alpha,\beta}\\!:\\!{k}}.{\forall{\kappa}.\
{{{a}\\!:\\!{\alpha}}\rightarrow{{{b}\\!:\\!{{\beta}{{\\{{\kappa(a,b)}\\}}}}}\rightarrow{{\texttt{pair}}[{\alpha,\beta}](\lambda{a,b}.\
{\kappa(a,b)})}}}}$ as ${p}\\!:\\!{\texttt{incPair}}$, we get $\displaystyle
s$ $\displaystyle\doteq\
{{a}\\!:\\!{\texttt{{int}}}}\rightarrow{{{b}\\!:\\!{{\texttt{{int}}}{{\\{{a<b}\\}}}}}\rightarrow{{\texttt{pair}}[{\texttt{{int}},\texttt{{int}}}](\lambda{a,b}.\
{a<b})}}$ Thus, $\mathsf{unapply}$ (fig. 7.6) extends the environment with
pattern binders $\displaystyle\mathrm{\Gamma}^{\prime}$ $\displaystyle\doteq\
\mathrm{\Gamma},\ {x}\\!:\\!{\texttt{{int}}},\
{y}\\!:\\!{{\texttt{{int}}}{{\\{{x<y}\\}}}}$ to obtain the goal for the case-
alternative $\displaystyle\mathrm{\Gamma}^{\prime}$ $\displaystyle\vdash\
y-x\Leftarrow\texttt{{nat}}$

which, Syn-Var and Syn-App reduce to the entailment

$\mathrm{\Gamma},{x,y,\nu}\\!:\\!{\texttt{{int}}}\vdash\
(x<y)\Rightarrow(\nu=y-x)\rightarrow(0\leq v)$

that is readily verified by the SMT solver. $\square$

####  8.3.4 Synthesis

$\textrm{{Type Synthesis}}\hfill\framebox{$\mathrm{\Gamma}\vdash e\Rightarrow
t$}$

$\displaystyle\displaystyle{\hbox{\hskip
142.62375pt\vbox{\hbox{\hskip-142.62373pt\hbox{\hbox{$\displaystyle\displaystyle\rho={\kappa}\\!:\\!{{\overline{b},b}\rightarrow{\texttt{bool}}}\quad\mathrm{\Gamma}\vdash
e\Rightarrow\forall{\rho}.\ {s}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{b}{{\\{{\star}\\}}}\triangleright{b}{{{\\{{{x}\\!:\\!{p}}\\}}}}\quad\mathrm{\Gamma};\overline{{x}\\!:\\!{b}}\vdash{b}{{{\\{{{x}\\!:\\!{p}}\\}}}}:B$}}}}\vbox{}}}\over\hbox{\hskip
55.53987pt\vbox{\vbox{}\hbox{\hskip-55.53986pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
e[\star]\Rightarrow{s}[\rho:=\lambda\overline{{x}\\!:\\!{b}},{x}\\!:\\!{b}.{p}]$}}}}}}$Syn-
RApp

Figure 8.7: $\mathsf{\lambda_{\rho}}$: Rules for Type Synthesis

To make refinement polymorphism ergonomic, we need a way to automatically
synthesize appropriate concrete refinements for each term $e[\star]$
corresponding to _uses_ of terms $e$ whose types abstract over the
refinements. Otherwise, the programmer would have to bear the burden of
writing concrete refinements at the ubiquitous usage sites, and worse, the
resulting code would be very difficult to read! Thus, refinement synthesis is
analogous to how we usually want to relieve the programmer of the burden of
providing (monomorphic) instances at uses of a polymorphic signature. Next,
lets see how this instantiation can be achieved by the refinement synthesis
machinery introduced in $\mathsf{\lambda_{\kappa}}$ (§ 5).

_Instantiating Refinement Variables_ The rule Syn-RApp shown in fig. 8.7 shows
how to synthesize types at refinement application sites $e[\star]$. The rule
says if we synthesize for $e$ a type $\forall{\rho}.\ {s}$ which uses an
abstract refinement variable
$\rho\equiv{\kappa}\\!:\\!{{\overline{b},b}\rightarrow{\texttt{bool}}}$ then
we can _instantiate_ $\rho$ in $s$ with any _well-formed_ concrete refinement
$\lambda{\overline{{x}\\!:\\!{b}},{x}\\!:\\!{b}}.\ {p}$ whose sort is
compatible with that of $\rho$, i.e. that is parameterized by the sorts
compatible with the inputs of $\kappa$.

Observe that Syn-RApp mimics Chk-Rec from fig. 5.3 which uses the hole
instantiation judgment $s\triangleright t$ from fig. 5.2 to declaratively
_guess_ a suitable way to replace the holes ${\\{{\star}\\}}$ in $s$ with
concrete refinements. In essence, Syn-RApp views the refinement variable
$\rho\equiv{\kappa}\\!:\\!{{\overline{b},b}\rightarrow{\texttt{bool}}}$ which
denotes a relation over values of types $\overline{b},b$ as an _unknown_
refinement over the base type ${b}{{\\{{\star}\\}}}$ and requires that we fill
the hole with any concrete refinement $p$ that is well-formed under an
environment extended with (i.e. can refer to) binders $\overline{x}$ for the
other parameters $\overline{b}$.

Example: Synthesis in brighter Lets use Syn-RApp to verify brighter from §
8.4. Let

int8 $\displaystyle\doteq\
{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{0\leq\nu<256}}\\}}}}$
$\displaystyle\mathrm{\Gamma}$ $\displaystyle\doteq\
{\texttt{maxI}}\\!:\\!{t_{\texttt{maxI}}},{x}\\!:\\!{\texttt{int8}},{y}\\!:\\!{\texttt{int8}}$
where $t_{\texttt{maxI}}$ is from (8.3). Using Syn-Var we have
$\displaystyle\mathrm{\Gamma}$ $\displaystyle\vdash\ \texttt{maxI}\Rightarrow
t_{\texttt{maxI}}$ Hence, as
${\texttt{{int}}}{{\\{{\star}\\}}}\triangleright\texttt{int8}$ and
$\mathrm{\Gamma}\vdash\texttt{int8}:B$ Syn-RApp lets us instantiate the
refinement variable $\kappa$ quantifying the signature of $t_{\texttt{maxI}}$
with the concrete refinement $\lambda{x}.\ {0\leq x<256}$ to obtain
$\displaystyle\mathrm{\Gamma}$ $\displaystyle\doteq\
\texttt{maxI}[\star]\Rightarrow{\texttt{int8}}\rightarrow{{\texttt{int8}}\rightarrow{\texttt{int8}}}$
Now, the function application rule Syn-App lets us establish
$\displaystyle\mathrm{\Gamma}$ $\displaystyle\doteq\
{{{\texttt{maxI}[\star]}\;{x}}\;{y}}\Rightarrow\texttt{int8}$

which, via rules Chk-Syn and Chk-Lam establishes that the implementation of
brighter $\lambda{x,y}.\ {{{\texttt{maxI}[\star]}\;{x}}\;{y}}$ indeed checks
against its specified type
${\texttt{int8}}\rightarrow{{\texttt{int8}}\rightarrow{\texttt{int8}}}$.
$\square$

###  8.4 Verification Conditions

The declarative rules simply guess suitable concrete refinements at each
instantiation site. Next, lets see how to implement those rules via the method
of Horn constraints introduced in § 5, as summarized in fig. 8.8.

_Checking_ To extend the $\mathsf{check}$ function to implement Chk-RAbs we
add a case for checking a term $e$ against a type of form $\forall{\rho}.\
{s}$ under environment $\mathrm{\Gamma}$. To this end, we substitute the
refinement variable $\rho$ with a concrete refinement $\varphi$ corresponding
to an uninterpreted function application $\lambda{\overline{x}}.\
{f_{\kappa}(\overline{x})}$ and then return the Horn constraint $c$
corresponding to the VC for checking the (substituted) term $e^{\prime}$
against the (substituted) type $s^{\prime}$.

Example: VC for maxI Lets see the VC $\mathsf{check}(\emptyset,\
e_{\texttt{maxI}},\ t_{\texttt{maxI}})$ generated to verify that the
implementation (8.8) of maxI adheres to its specification (8.9). The VC is
obtained by substituting the refinement variable $\kappa$ with the
uninterpreted function symbol $f_{\kappa}$ and then recursively invoking
$\mathsf{check}$ on the substituted body and signature, which produces the VC:

$\forall f_{\kappa},{x},{y},\nu.\ f_{\kappa}({x})\Rightarrow
f_{\kappa}({y})\Rightarrow((\nu={x}\Rightarrow
f_{\kappa}(\nu))\wedge(\nu={y}\Rightarrow f_{\kappa}(\nu)))$

which mirrors the entailments for the checking judgment (8.10). $\square$

_Synthesis_ Finally, in fig. 8.8 we extend $\mathsf{synth}$ to account for
refinement instantiation terms $e[\star]$ via an algorithmic implementation of
Syn-RApp. First, we recursively invoke $\mathsf{synth}$ to As in the
declarative rule, we recursively invoke $\mathsf{synth}$ to synthesize the
refinement-polymorphic signature $\forall{\rho}.\ {s}$ for $e$. Next, as in
fig. 5.5 we implement the declarative
${b}{{\\{{\star}\\}}}\triangleright{b}{{{\\{{{x}\\!:\\!{p}}\\}}}}$ by using
$\mathsf{fresh}(\mathrm{\Gamma};\overline{{x}\\!:\\!{b}},\
{b}{{\\{{\star}\\}}})$ to obtain a new _template_
${b}{{{\\{{{x}\\!:\\!{p}}\\}}}}$ where $p$ contains refinement (Horn)
variables for the unknown concrete refinements to be used for instantiation.
We use $p$ to build a concrete refinement that is substituted for $\rho$ in
$s$ to return the synthesized type for $e[\star]$, together with the VC $c$
obtained for $e$.

Example: Checking of brighter Lets see how the above procedure computes a Horn
constraint (VC) whose satisfiability implies that brighter (8.4) implements
the specification
${\texttt{int8}}\rightarrow{{\texttt{int8}}\rightarrow{\texttt{int8}}}$. Let

$\displaystyle\mathrm{\Gamma}$ $\displaystyle\doteq\
{\texttt{maxI}}\\!:\\!{t_{\texttt{maxI}}}$ $\displaystyle e_{\texttt{br}}$
$\displaystyle\doteq\ \lambda{x,y}.\ {\ {{\texttt{maxI}[\star]}\;{x}}\;{y}}$
$\displaystyle t_{\texttt{br}}$ $\displaystyle\doteq\
{\texttt{int8}}\rightarrow{{\texttt{int8}}\rightarrow{\texttt{int8}}}$
respectively be the environment, implementation and specification for
brighter, where $t_{\texttt{maxI}}$ is from (8.3). Let
$\displaystyle\mathrm{\Gamma}^{\prime}$ $\displaystyle\doteq\
\mathrm{\Gamma},\ {x}\\!:\\!{\texttt{int8}},\ {y}\\!:\\!{\texttt{int8}}$ By
consulting $\mathrm{\Gamma}^{\prime}$,
$\mathsf{synth}(\mathrm{\Gamma}^{\prime},\ \texttt{maxI})$ returns
$(\mathit{true},\ t_{\texttt{maxI}})$ where $\displaystyle t_{\texttt{maxI}}$
$\displaystyle\doteq\ \forall{\kappa}.\
{{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}}\rightarrow{{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}}\rightarrow{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa({\nu})}}\\}}}}}}})$
Hence, we invoke
$\mathsf{fresh}(\mathrm{\Gamma},{\texttt{{int}}}{{\\{{\star}\\}}},\ $) to
obtain the template
${\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa_{\texttt{br}}({\nu})}}\\}}}}$ with
a new Horn variable $\kappa_{\texttt{br}}$ denoting the unknown concrete
refinement at this instantiation site. Upon substituting the corresponding
concrete refinement for the refinement variable we get the template (eliding
the trivial Horn constraint $\mathit{true}$)
$\displaystyle\mathsf{synth}(\mathrm{\Gamma}^{\prime},\ \texttt{maxI}[\star])$
$\displaystyle\doteq{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa_{\texttt{br}}({\nu})}}\\}}}}}\rightarrow{{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa_{\texttt{br}}({\nu})}}\\}}}}}\rightarrow{{\texttt{{int}}}{{{\\{{{\nu}\\!:\\!{\kappa_{\texttt{br}}({\nu})}}\\}}}}}}$

Then, via the usual cases for function application, we get the VC

$\begin{array}[]{rcll}\mathsf{check}(\mathrm{\Gamma},\ e_{\texttt{br}},\
t_{\texttt{br}})&\doteq&\lx@intercol\forall x.(0\leq
x<256)\Rightarrow\hfil\lx@intercol\\\ &&\lx@intercol\quad\forall y.(0\leq
y<256)\Rightarrow\hfil\lx@intercol\\\
&.&&\forall\nu.(\nu=x)\Rightarrow\kappa_{\texttt{br}}({\nu})\\\
&&\quad\quad\wedge&\forall\nu.(\nu=y)\Rightarrow\kappa_{\texttt{br}}({\nu})\\\
&&\quad\quad\wedge&\forall\nu.\kappa_{\texttt{br}}({\nu})\Rightarrow(0\leq
v<256)\end{array}$

The first two conjuncts check that the arguments $x$ and $y$ respectively
satisfy the input types (preconditions) of $\texttt{maxI}[\star]$, and the
last conjunct stipulates that the output type (postcondition) of the call is a
valid int8 value, all assuming the values $x$ and $y$ inhabit int8 as
specified by the input type of brighter. The above VC can be satisfied by
assigning $\kappa_{\texttt{br}}\doteq\lambda{a}.\ {0\leq a<256}$, and hence we
verify that brighter correctly implements its specification. $\square$

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{check}&:&(\mathrm{\Gamma}\times
E\times T)\rightarrow C\\\ \hline\cr\mathsf{check}(\mathrm{\Gamma},\ e,\
\forall{\rho}.\
{s})&\doteq&({{f_{\kappa}::{\overline{t}}\rightarrow{\texttt{bool}}}})\Rightarrow
c\\\ \quad\mbox{where}&&\\\ \quad\quad
c&=&\mathsf{check}(\mathrm{\Gamma}^{\prime},\ {e}[\rho:=\varphi],\
{s}[\rho:=\varphi])\\\
\quad\quad\mathrm{\Gamma}^{\prime}&=&\mathrm{\Gamma};{{f_{\kappa}}\\!:\\!{{\overline{t}}\rightarrow{\texttt{bool}}}}\\\
\quad\quad\varphi&=&\lambda{\overline{x}}.\ {f_{\kappa}(\overline{x})}\\\
\quad\quad{\kappa}\\!:\\!{{\overline{t}}\rightarrow{\texttt{bool}}}&=&\rho\\\\[3.61371pt]
\hline\cr\hline\cr\mathsf{synth}&:&(\mathrm{\Gamma}\times
E)\rightarrow(C\times T)\\\ \hline\cr\mathsf{synth}(\mathrm{\Gamma},\
e[\star])&\doteq&(c,{s}[\rho:={\lambda\overline{{x}\\!:\\!{b}},{x}\\!:\\!{b}.{p}}])\\\\[3.61371pt]
\quad\mbox{where}&&\\\ \quad\quad(c,\forall{\rho}.\
{s})&=&\mathsf{synth}(\mathrm{\Gamma},\ e)\\\
\quad\quad{\kappa}\\!:\\!{{\overline{b},b}\rightarrow{\texttt{bool}}}&=&\rho\\\
\quad\quad\overline{x}&=&\mbox{fresh variables of sort}\ $$\overline{b}$$\\\
\quad\quad{b}{{{\\{{{x}\\!:\\!{p}}\\}}}}&=&\mathsf{fresh}(\mathrm{\Gamma};\overline{{x}\\!:\\!{b}},\
{b}{{\\{{\star}\\}}})\\\\[3.61371pt] \hline\cr\hline\cr\end{array}$ Figure
8.8: Algorithmic Checking for $\mathsf{\lambda_{\rho}}$, extends cases of fig.
7.12

###  8.5 Discussion

In $\mathsf{\lambda_{\rho}}$ we saw how we often want to specify signatures
that abstract over refinements, how these signatures can be checked using
uninterpreted functions, and how we can extend the Horn-constraint based
inference method from § 5 to automatically instantiate abstract refinements at
usage sites. The method was introduced by [Vazou13] who illustrated a variety
of applications in establishing invariants of data structures. [Gordon17]
demonstrated that abstract refinements could be used to encode a form of
concurrent rely-guarantee reasoning, enabling the verification of
implementations of lock-free data structures. Subsequent work by
[polikarpova16] showed how refinement polymorphism allows writing compact
specifications from which implementations can be automatically _synthesized_.

_Bounded Quantification_ The abstract refinements in $\mathsf{\lambda_{\rho}}$
were completely unconstrained. However, we could imagine a form of _bounded
quantification_ for refinement variables analogous to type variables
[fbounded], which would restrict instantiating refinements to those satisfying
particular conditions. Such an extension was explored by [Vazou15] who showed
how the programmer can use Horn constraints to express bounds which allow
specifying expressive signatures whilst preserving decidable and automatic
verification. These extensions enable, for example, encoding a monadic
information flow control (IFC) mechanism, purely within refinement types
[liftyICFP20] enabling the construction of web applications adhering to
expressive data-sensitive security policies [binah].

##  Chapter 9 Termination

The problem of verifying that the execution of a certain piece of code always
terminates is perhaps one of the oldest in computing, going back all the way
to [Turing36]’s work on the undecidability of the Halting Problem. Of course,
just because a problem is undecidable, doesn’t mean that it goes away! Indeed,
as [rice53] pointed out _all_ non-trivial semantic properties of programs are
undecidable. That is, it is just as undecidable to guarantee that, e.g. a
program will not attempt to add int and bool values. Yet, we have developed
syntactic disciplines that have turned verifying the absence of errors like
adding int and bool values into into a routine part of compiling code. Next,
lets see how refinements allow us to develop a simple and practical discipline
for verifying, at compile time, that functions always terminate.

###  9.1 Examples

Lets see some examples that illustrate how to verify termination.

_Well-founded Metrics_ Consider the function sum which adds up the numbers
from 0 to n:

⬇

val sum : n:nat => nat

let rec sum = (n) => {

if (n < 1) {

0

} else {

n + sum(n-1)

}

}

Why _does_ sum n terminate? First, notice that sum will not terminate if
invoked on a negative number, e.g. sum(-3) will diverge. We eliminate this
possibility by requiring the precondition that n:nat i.e. the inputs be non-
negative. Now, when n equals zero, the procedure simply returns the result 0.
Otherwise, it recurses on a _strictly_ smaller input, until, ultimately, it
reaches 0, at which point it terminates.

_Proving Termination by Induction_ Thus we can, somewhat more formally, prove
termination _by induction_ on n.

  * •

_Base case_ sum terminates for inputs $k=$ 0.

  * •

_Induction Hypothesis_ Assume sum terminates on all $k\leq$ n.

  * •

_Inductive Step_ Check that sum(n+1) only recursively invokes sum(n) which
satisfies the induction hypothesis and hence terminates.

This reasoning suffices to convince ourselves that sum(n) terminates for every
non-negative n. That is, we have shown that sum terminates because a _well-
founded_ metric: here the non-negative n is _strictly decreasing_ at each
recursive call.

_Proving Termination with Types_ We can capture the above reasoning via the
type system as follows. First we require that sum only be called with non-
negative nat values, which were defined as

⬇

type nat = int[v|0 <= v]

Second, we to ensure that the recursion is on _strictly smaller_ values, we
need only typecheck the _implementation_ of sum in an environment that
requires sum only be called with inputs smaller than n, i.e. we check the body
in a environment of the form

$\mathrm{\Gamma}_{\texttt{sum}}\ \doteq\ {n}\\!:\\!{\texttt{{nat}}},\
{\texttt{sum}}\\!:\\!{{{n^{\prime}}\\!:\\!{{\texttt{{int}}}{{\\{{0\leq
n^{\prime}<n}\\}}}}}\rightarrow{\texttt{{nat}}}}$

The above ensures that any (recursive) call in the body only calls sum with
inputs smaller than the “current” parameter n. Notice that if we had not
required n to be non-negative, then the parameter n-1 passed in at the
recursive call would be smaller than n but would not be non-negative, and
hence, would fail the strengthened precondition for sum, as indeed it should,
as such a computation does not terminate!

_Recursion on Multiple Parameters_ The above method works even when there are
multiple parameters, as long as there is _some_ nat-valued parameter that is
used to limit the recursion. Consider the following tail-recursive variant of
sum

⬇

let rec sumT = (total, n) => {

if (n == 0) {

total

} else {

sumT(total + n, n - 1)

}

}

The function sumT(total, n) takes two parameters: n as before, and total which
holds the accumulated summation of the “previously seen” seen. That is,
sumT(0,3) evaluates as follows:

⬇

sumT(0,3) $\dashrightarrow$ sumT(3,2) $\dashrightarrow$ sumT(5,1)
$\dashrightarrow$ sumT(6,0) $\dashrightarrow$ 6

_Specifying Termination Metrics_ The accumulation parameter total is not
strictly decreasing. However, the parameter n _is_ decreasing and non-negative
and serves to witness that sumT always terminates. But how might the type-
checker _guess_ that it should use n instead of total? While one can imagine a
variety of pragmatic and effective heuristics to make such guesses, for our
purposes, we shall simply give the type checker an explicit _termination
metric_

⬇

val sumT: total:nat => n:nat => nat / n

In the above, we end the type signature for sumT with / n to denote that the
value n should be used as the termination metric. The typechecker will verify
that the value of the metric n is indeed well-founded: i.e. non-negative and
strictly decreasing at each recursive call, and if so, will deem the function
terminating.

_Metric Expressions_ Metrics generalize to situations where no single
parameter is decreasing, but some _expression_ over the parameters is. For
example, consider the function range(i, j) which returns the list of integers
between i and j

⬇

val range : i:int => j:int => list(int) / j - i

let rec range = (i, j) => {

if (i < j) {

Cons(i, range(i+1, j))

} else {

Nil

}

}

In the above, neither argument is decreasing: i _increases_ at each call, and
j is unchanged. Nevertheless, the function terminates as the _gap_ between i
and j diminishes at each recursive call, and the function terminates when that
gap reaches 0. We can make this intuition precise via the termination metric /
j-i. Armed with this information, the type checker ensures that at each
recursive call in the body, the value of j-i is decreasing and non-negative.
That is, we will check the implementation of range in an environment

$\mathrm{\Gamma}_{\texttt{range}}\ \doteq\ {i,j}\\!:\\!{\texttt{{int}}},\
{\texttt{range}}\\!:\\!{{{i^{\prime}}\\!:\\!{\texttt{{int}}}}\rightarrow{{{j^{\prime}}\\!:\\!{{\texttt{{int}}}{{\\{{0\leq
j^{\prime}-i^{\prime}<j-i}\\}}}}}\rightarrow{\texttt{{int}}}}}$ (9.1)

that stipulates that recursive calls to range must have strictly smaller, non-
negative gaps, to verify that range indeed always terminates.

_Lexicographic Metrics_ Sometimes, it is convenient to split up the
termination metric across _multiple_ smaller metrics. For example consider
Ackermann’s function

⬇

val ack : m:nat => n:nat => nat / m, n

let rec ack = (m, n) => {

if (m == 0) { n + 1 } else {

if (n == 0) { ack (m - 1, 1) } else {

ack (m - 1, ack (m, n - 1))

}

}

}

Why does ack terminate? At each iteration either the _first_ parameter m
decreases, or m remains the same and the _second_ parameter n decreases. Each
time that n reaches 0, it cannot decrease further so m must decrease. Hence, m
will eventually reach 0 and ack will terminate. In other words, the _pair_ (m,
n) decreases in the _lexicographic order_ on pairs, which is a well-ordering
that has no infinite descending chains [NipkowRewriting].

_Specifying Lexicographic Orders via Types_ We can extend our notion of
metrics to account for lexicographic orders by allowing the user to write a
_sequence_ of metrics. For example, we type ack with the signature with the
termination metric / m, n and then we will use the sequence to check the
implementation of ack in environment $\mathrm{\Gamma}_{\texttt{ack}}$

${m,n}\\!:\\!{\texttt{{nat}}},\
{\texttt{ack}}\\!:\\!{{{m^{\prime}}\\!:\\!{\texttt{{nat}}}}\rightarrow{{{n^{\prime}}\\!:\\!{{\texttt{{nat}}}{{\\{{m^{\prime}<m\vee(m^{\prime}=m\wedge
n^{\prime}<n)}\\}}}}}\rightarrow{\texttt{{nat}}}}}$

The signature for ack limits recursive uses of ack to parameters that satisfy
the lexicographic ordering to ensure that ack terminates.

_Structural Recursion_ Often the recursion is over the elements of a datatype
like a list or a tree. For example, consider the function that appends two
lists xs and ys

⬇

val append : xs:list(’a) => ys:list(’a) => list(’a)

/ len(xs)

let rec append = (xs, ys) => {

switch (xs) {

| Nil => ys

| Cons (x, xs’) => Cons (x, append (xs’, ys))

}

}

The function append recurses on the _tail_ of the first list xs and stops when
that list is empty i.e. equal to Nil. This is a form of _structural recursion_
where each recursive call is over sub-structures (e.g. the tail) of some input
parameter. We can verify the termination of structurally recursive functions
by using _measures_ to specify suitable metrics. For append we specify the
metric / len(xs) which tells the type checker to limit recursive calls in the
implementation of append to lists whose length is smaller than xs. That is, we
check the implementation of append in an environment where
${xs,ys}\\!:\\!{\texttt{list}{(\alpha)}}$, and append is limited to

${{xs^{\prime}}\\!:\\!{{\texttt{list}{(\alpha)}}{{\\{{\texttt{len}(xs^{\prime})<\texttt{len}(xs)}\\}}}}}\rightarrow{{{ys^{\prime}}\\!:\\!{\texttt{list}{(\alpha)}}}\rightarrow{\texttt{list}{(\alpha)}}}$

_Non-Structural Recursion_ Finally, the notion of metrics over measures scales
up to account for more general scenarios where the recursion over the
datatypes is not structural. For example, consider the function braid which
takes two lists $x_{1},\ldots$ and $y_{1},\ldots$ and returns the list
$x_{1},y_{1},\ldots$

⬇

val braid : xs:list(’a) => ys:list(’a) => list(’a)

/ len(xs) + len(ys)

let rec braid = (xs, ys) => {

switch (xs) {

| Nil => ys

| Cons (x, xs’) => Cons(x, braid(ys, xs’))

}

}

The recursion in braid is not structural: the recursive call flips the order
of the lists to ensure the values alternate in the output. However, in this
case, the _sum_ of the lengths of the two input lists shrinks. We specify this
via the metric / len(xs) + len(ys) which tells the type checker to check the
body of braid under the following environment

${xs,\ ys}\\!:\\!{\texttt{list}{(\alpha)}},\
{\texttt{braid}}\\!:\\!{{{xs^{\prime}}\\!:\\!{\texttt{list}{(\alpha)}}}\rightarrow{{{ys^{\prime}}\\!:\\!{{\texttt{list}{(\alpha)}}{{\\{{p}\\}}}}}\rightarrow{\texttt{list}{(\alpha)}}}}$

where the refinement

$p\ \doteq\
0\leq\texttt{len}(xs^{\prime})+\texttt{len}(ys^{\prime})<\texttt{len}(xs)+\texttt{len}(ys)$

limits recursive calls to parameters the sum of whose lengths are decreasing,
to verify that braid terminates.

###  9.2 Types and Terms

_Metric_ | $m$ | $\vcentcolon\vcentcolon=$ | $p$ | _decreasing expression_
---|---|---|---|---
|  | $\ \mid\ $ |  $p$, $m$ | _lexicographic metric_
_Terms_ | $e$ | $\vcentcolon\vcentcolon=$ | $\ldots$ | _from Fig. 8.1_
|  | $\ \mid\ $ | $\texttt{{rec}}\;x={e_{1}}\\!:\\!{t/m}\;\texttt{{in}}\;e_{2}$ | _recursive binder_
Figure 9.1: $\mathsf{\lambda_{\tau}}$: Syntax of Types and Terms

As demonstrated by the examples, $\mathsf{\lambda_{\tau}}$ requires two small
extensions to its syntax: a way to specify termination metrics, and a means of
specifying metrics in type signatures, as summarized in fig. 9.1.

_Metrics_ A _termination metric_ (or just metric in brief) is either a single
_decreasing expression_ $p$ which is an int-sorted term from the refinement
logic (fig. 2.1), or a _lexicographic metric_ comprising a sequence of
decreasing expressions.

_Recursive Signatures_ In $\mathsf{\lambda_{\tau}}$ we require that recursive
rec binders be annotated with signatures that also specify a termination
metric $m$. For example, we would type ack as

$\texttt{{rec}}\;\texttt{ack}={\lambda{m,n}.\
{e_{\texttt{ack}}}}\\!:\\!{t_{\texttt{ack}}}\;\texttt{{in}}\;\ldots$

where the signature $t_{\texttt{ack}}$ specifies the lexicographic metric with
the sequence of decreasing expressions $m,n$

$t_{\texttt{ack}}\ \doteq\
{{m}\\!:\\!{\texttt{{nat}}}}\rightarrow{{{n}\\!:\\!{\texttt{{nat}}}}\rightarrow{\texttt{{nat}}}}\leavevmode\nobreak\
/\leavevmode\nobreak\ m,n$ (9.2)

###  9.3 Declarative Typing

$\textrm{{Metric Well-formedness}}\hfill\framebox{$\mathrm{\Gamma}\vdash m$}$

$\displaystyle\displaystyle{\hbox{\hskip
18.83504pt\vbox{\hbox{\hskip-18.83502pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
p:\texttt{{int}}$}}}\vbox{}}}\over\hbox{\hskip
10.08505pt\vbox{\vbox{}\hbox{\hskip-10.08504pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
p$}}}}}}$Wfm-Base $\displaystyle\displaystyle{\hbox{\hskip
27.04454pt\vbox{\hbox{\hskip-27.04454pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
p\quad\mathrm{\Gamma}\vdash m$}}}\vbox{}}}\over\hbox{\hskip
16.69733pt\vbox{\vbox{}\hbox{\hskip-16.69731pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
p,m$}}}}}}$Wfm-Lex

Figure 9.2: Rules for Checking Metric Well-formedness

As we saw with the examples in section 9.1 termination checking reduces quite
directly to plain refinement checking after _limiting_ recursive applications
within the implementation to types that are strengthened with special
refinements that ensure that the recursion is _well-founded_.

_Metric Well-formedness_ The judgment $\mathrm{\Gamma}\vdash m$ says that a
termination metric $m$ is _well-formed_ in an environment $\mathrm{\Gamma}$.
The judgment is established by the rules Wfm-Base and Wfm-Lex which, in
concert, check that each decreasing expression in the metric can be typed as
an int-valued term under $\mathrm{\Gamma}$.

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{wfr}&:&(M\times M)\rightarrow
P\\\ \hline\cr\mathsf{wfr}(p^{*},p^{\prime})&\doteq&0\leq p^{\prime}\wedge
p^{\prime}<p^{*}\\\\[3.61371pt]
\mathsf{wfr}(p^{*};m^{*},p^{\prime};m^{\prime})&\doteq&0\leq
p^{\prime}\wedge(p^{\prime}<p^{*}\vee r)\\\ \quad\mbox{where}&&\\\ \quad\quad
r&=&p^{\prime}=p^{*}\wedge\mathsf{wfr}(m^{*},m^{\prime})\\\\[3.61371pt]
\hline\cr\hline\cr\end{array}$ Figure 9.3: Computing Well-foundedness
Refinements

_Well-foundedness Refinements_ The procedure $\mathsf{wfr}(m^{*},m^{\prime})$
shown in fig. 9.3 takes as input two termination metrics, and returns as
output a predicate that guarantees the metric demonstrates well-founded
(terminating) recursion. The inputs $m^{*}$ and $m^{\prime}$ respectively
denote the values of a function’s termination metric over the _original_ and
_recursive_ call parameters. The output is a _well-foundedness refinement_
corresponding to the precondition that must hold at each recursive call in
order for the metric to demonstrate the function terminating.

For range, we would use the termination metric $/\leavevmode\nobreak\ j-i$ to
compute the well-foundedness refinement

$\mathsf{wfr}(j^{\prime}-i^{\prime},j-i)\doteq 0\leq
j^{\prime}-i^{\prime}<j-i$ (9.3)

Similarly, for ack, we would use the termination metric $/\leavevmode\nobreak\
m,n$ to compute a well-foundedness refinement

$\mathsf{wfr}((m^{\prime},n^{\prime}),(m,n))\doteq 0\leq
m^{\prime}\wedge(m^{\prime}<m\vee(m^{\prime}=m\wedge 0\leq n^{\prime}<n))$
(9.4)

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{lim}&:&(\mathrm{\Gamma}\times
M\times T)\rightarrow T\\\
\hline\cr\mathsf{lim}(\mathrm{\Gamma},m,t)&\doteq&\mathsf{lim^{*}}(\mathrm{\Gamma},m,m,t)\\\\[7.22743pt]
\hline\cr\mathsf{lim^{*}}&:&(\mathrm{\Gamma}\times M\times M\times
T)\rightarrow T\\\\[3.61371pt]
\mathsf{lim^{*}}(\mathrm{\Gamma},m^{*},m,{{x}\\!:\\!{{b}{{\\{{p}\\}}}}}\rightarrow{t})&&\\\
\quad\mid\mathrm{\Gamma};{{x}\\!:\\!{b}}\vdash
m&\doteq&{{x^{\prime}}\\!:\\!{{b}{{\\{{p^{\prime}}\\}}}}}\rightarrow{t^{\prime}}\\\
\quad\mbox{where}&&\\\ \quad\quad
p^{\prime}&=&{p}[x:=x^{\prime}]\wedge\mathsf{wfr}(m^{*},m^{\prime})\\\
\quad\quad m^{\prime}&=&{m}[x:=x^{\prime}]\\\ \quad\quad
t^{\prime}&=&{t}[x:=x^{\prime}]\\\\[3.61371pt]
\mathsf{lim^{*}}(\mathrm{\Gamma},m^{*},m,{{x}\\!:\\!{s}}\rightarrow{t})&\doteq&{{x^{\prime}}\\!:\\!{s^{\prime}}}\rightarrow{t^{\prime\prime}}\\\
\quad\mbox{where}&&\\\ \quad\quad
t^{\prime\prime}&=&\mathsf{lim^{*}}(\mathrm{\Gamma};{{x}\\!:\\!{s}},m^{*},m^{\prime},t^{\prime})\\\
\quad\quad m^{\prime}&=&{m}[x:=x^{\prime}]\\\ \quad\quad
s^{\prime}&=&{s}[x:=x^{\prime}]\\\ \quad\quad
t^{\prime}&=&{t}[x:=x^{\prime}]\\\\[3.61371pt]
\mathsf{lim^{*}}(\mathrm{\Gamma},m^{*},m,\forall{{\alpha}\\!:\\!{k}}.{t})&\doteq&\forall{{\alpha}\\!:\\!{k}}.{\mathsf{lim^{*}}(\mathrm{\Gamma},m^{*},m,t)}\\\
\hline\cr\hline\cr\end{array}$ Figure 9.4: Checking termination by type
limiting

_Type Limiting_ The procedure $\mathsf{lim}(\mathrm{\Gamma},m,t)$ shown in
fig. 9.4 computes a type $t^{\prime}$ which strengthens the input types
(preconditions) to require that all (recursive) calls be _limited_ to values
that are allowed by the metric $m$. The real work is done by the helper
$\mathsf{lim^{*}}(\mathrm{\Gamma},m^{*},m,t)$ which takes the _original_
metric $m^{*}$ and the _recursive_ metric $m$ where all the input binders
($x$) are replaced with “primed” versions ($x^{\prime}$) and returns a version
of $t$ where (1) the inputs are renamed with their primed variants and (2) the
well-foundedness refinement is used to strengthen the first input refinement
where it is well-formed, i.e. where all the binders appearing in the
refinement are in scope. To this end, the procedure recurses over the
structure of the (function) type $t$, adding the binders to $\mathrm{\Gamma}$
and renaming the inputs $m$ with their primed versions, _until_ it has added
enough binders to $\mathrm{\Gamma}$ for $m^{*}$ to be well-formed, at which
point, it strengthens the current parameter’s refinement $p$ with the well-
foundedness refinement $\mathsf{wfr}(m^{*},m^{\prime})$.

For simplicity, the definition of $\mathsf{lim^{*}}$ and the rule Chk-Term do
not support refinement polymorphism. It is straightforward to remove this
restriction by extending the definitions to allow for types abstracted over
refinements.

Example: Type of range Recall that range has type

$t_{\texttt{range}}\doteq{{i}\\!:\\!{\texttt{{int}}}}\rightarrow{{{j}\\!:\\!{\texttt{{int}}}}\rightarrow{\texttt{list}{(\texttt{{int}})}}}\leavevmode\nobreak\
/\leavevmode\nobreak\ j-i$ (9.5)

We will check its body with the metric limited type

$\displaystyle\ \mathsf{lim}(\emptyset,\ j-i,\
{{i}\\!:\\!{\texttt{{int}}}}\rightarrow{{{j}\\!:\\!{\texttt{{int}}}}\rightarrow{\texttt{list}{(\texttt{{int}})}}})$
which is defined as $\displaystyle=$ $\displaystyle\
\mathsf{lim^{*}}(\emptyset,\ j-i,\ j-i,\
{{i}\\!:\\!{\texttt{{int}}}}\rightarrow{{{j}\\!:\\!{\texttt{{int}}}}\rightarrow{\texttt{list}{(\texttt{{int}})}}})$
as the metric $j-i$ is not well-formed, we rename $i$ to $i^{\prime}$ and
recurse $\displaystyle=$ $\displaystyle\
{{i^{\prime}}\\!:\\!{\texttt{{int}}}}\rightarrow{\mathsf{lim^{*}}({i}\\!:\\!{\texttt{{int}}},\
j-i,\ j-i^{\prime},\
{{j}\\!:\\!{\texttt{{int}}}}\rightarrow{\texttt{list}{(\texttt{{int}})}})}$
now, since ${i}\\!:\\!{\texttt{{int}}},{j}\\!:\\!{\texttt{{int}}}\vdash j-i$
the above is $\displaystyle=$ $\displaystyle\
{{i^{\prime}}\\!:\\!{\texttt{{int}}}}\rightarrow{{{j^{\prime}}\\!:\\!{{\texttt{{int}}}{{\\{{\mathsf{wfr}(j-i,j^{\prime}-i^{\prime})}\\}}}}}\rightarrow{\texttt{list}{(\texttt{{int}})}}}$
which, after substituting the well-foundedness refinement (eq. 9.3)
$\displaystyle=$ $\displaystyle\
{{i^{\prime}}\\!:\\!{\texttt{{int}}}}\rightarrow{{{j^{\prime}}\\!:\\!{{\texttt{{int}}}{{\\{{0\leq
j^{\prime}-i^{\prime}<j-i}\\}}}}}\rightarrow{\texttt{list}{(\texttt{{int}})}}}$

$\square$

$\textrm{{Termination Checking}}\hfill\framebox{$\mathrm{\Gamma}\vdash
x=e:s/m\triangleright t$}$

$\displaystyle\displaystyle{\hbox{\hskip
171.14098pt\vbox{\hbox{\hskip-171.14098pt\hbox{\hbox{$\displaystyle\displaystyle
t=\mathsf{fresh}(\mathrm{\Gamma},\
s)=\forall{{\overline{\alpha}}\\!:\\!{k}}.{{\overline{{y}\\!:\\!{s}}}\rightarrow{t^{*}}}\quad
e=\Lambda{\overline{\alpha}}\\!:\\!{k}.{\lambda{\overline{y}}.\
{e^{*}}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma};{\overline{{\alpha}\\!:\\!{k}};\overline{{y}\\!:\\!{s}};{x}\\!:\\!{\mathsf{lim}(\mathrm{\Gamma},m,t)}}\vdash
e^{*}\Leftarrow t^{*}$}}}}\vbox{}}}\over\hbox{\hskip
41.57213pt\vbox{\vbox{}\hbox{\hskip-41.57213pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
x=e:s/m\triangleright t$}}}}}}$Chk-Term

$\textrm{{Type Checking}}\hfill\framebox{$\mathrm{\Gamma}\vdash e\Leftarrow
t$}$

$\displaystyle\displaystyle{\hbox{\hskip
84.11626pt\vbox{\hbox{\hskip-84.11624pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash
x=e_{1}:s_{1}/m\triangleright
t_{1}\qquad\mathrm{\Gamma};{{x}\\!:\\!{t_{1}}}\vdash e_{2}\Leftarrow
t_{2}$}}}\vbox{}}}\over\hbox{\hskip
60.34756pt\vbox{\vbox{}\hbox{\hskip-60.34755pt\hbox{\hbox{$\displaystyle\displaystyle\mathrm{\Gamma}\vdash\texttt{{rec}}\;x={e_{1}}\\!:\\!{s_{1}/m}\;\texttt{{in}}\;e_{2}\Leftarrow
t_{2}$}}}}}}$Chk-Rec

Figure 9.5: Bidirectional Checking: Other rules from $\mathsf{\lambda_{\rho}}$
(Fig. 8.4)

_Termination Checking_ We introduce a new _termination checking_ judgment
$\mathrm{\Gamma}\vdash x=e:s/m\triangleright t$ which _guarantees_ that in an
environment $\mathrm{\Gamma}$, the (recursive) definition $x=e$ is terminating
with the metric $m$, and that downstream definitions can _assume_ that $x$
behaves as $t$. The rule Chk-Term shown in fig. 9.5 establishes this judgment
by

  1. 1.

_Instantiating_ the _holes_ in $s$ to obtain the complete signature $t$,

  2. 2.

_Splitting_ the definition $e$ into its input _binders_
$\overline{{y}\\!:\\!{s}}$ and _body_ $e^{*}$,

  3. 3.

_Checking_ the body $e^{*}$ in an environment containing the input binders
$\overline{{y}\\!:\\!{s}}$ which name the _current_ input, _and_ where $x$ is
bound to its _metric limited type_ $\mathsf{lim}(\mathrm{\Gamma},m,t)$.

That is, the key change is to check the body of the recursive binder in an
environment that limits the recursion using the specified metric.

_Checking Recursive Definitions_ We can now use the termination checking
judgment in the updated rule Chk-Rec shown in fig. 9.5. To check that
$\texttt{{rec}}\;x={e_{1}}\\!:\\!{s_{1}/m}\;\texttt{{in}}\;e_{2}$ has type
$t_{2}$, the new rule requires that the binder $x$ terminates with $m$, and
then, (as before), checks $e_{2}$ against $t_{2}$ in the environment extended
with $x$.

Example: Checking range Lets see how Chk-Term checks the term

$\displaystyle e_{\texttt{r}}$ $\displaystyle\ \doteq\
\texttt{{rec}}\;\texttt{range}={(\lambda{i,j}.\
{e_{\texttt{range}}})}\\!:\\!{\ t_{\texttt{range}}}\;\texttt{{in}}\;\ldots$
(9.6) where $\displaystyle e_{\texttt{range}}$ $\displaystyle\ \doteq\
\texttt{{if}}\;i<j\;\texttt{{then}}\;{\texttt{Cons}[\texttt{{int}}]\ i\
(\texttt{range}\ (i+i)\ j)}\;\texttt{{else}}\;\texttt{Nil}[\texttt{{int}}]$
$\displaystyle t_{\texttt{range}}$ $\displaystyle\
\doteq{{i}\\!:\\!{\texttt{{int}}}}\rightarrow{{{j}\\!:\\!{\texttt{{int}}}}\rightarrow{\texttt{list}{(\texttt{{int}})}}}\leavevmode\nobreak\
/\leavevmode\nobreak\ j-i$

Chk-Term stipulates that we use the metric to limit the type and check the
body $e_{\texttt{range}}$ against the specified output
$\texttt{list}{(\texttt{{int}})}$ in environment
$\mathrm{\Gamma}_{\texttt{range}}$ from eq. 9.1

$\displaystyle\mathrm{\Gamma}_{\texttt{range}}$ $\displaystyle\ \vdash\
e_{\texttt{range}}\Leftarrow\texttt{list}{(\texttt{{int}})}$ Rule Chk-If
reduces the above to checks on each branch. Eliding the trivial else case, we
get $\displaystyle\mathrm{\Gamma}_{\texttt{range}};i<j$ $\displaystyle\
\vdash\ {\texttt{Cons}[\texttt{{int}}]\ i\ (\texttt{range}\ (i+i)\
j)}\Leftarrow\texttt{list}{(\texttt{{int}})}$ which Syn-App splits into a
check that $\displaystyle\mathrm{\Gamma}_{\texttt{range}};i<j$ $\displaystyle\
\vdash\ \texttt{range}\ (i+i)\ j\Leftarrow\texttt{list}{(\texttt{{int}})}$
Again, Syn-App splits the above into checks that ensure each _input_ to range
satisfies the environment’s (limited) input type
$\displaystyle\mathrm{\Gamma}_{\texttt{range}};i<j$ $\displaystyle\ \vdash\
{\texttt{{int}}}{{{\\{{{i^{\prime}}\\!:\\!{i^{\prime}=i+1}}\\}}}}\ \prec:\
\texttt{{int}}$
$\displaystyle\mathrm{\Gamma}_{\texttt{range}};i<j;{i^{\prime}}\\!:\\!{{\\{{i^{\prime}=i+1}\\}}}$
$\displaystyle\ \vdash\
{\texttt{{int}}}{{{\\{{{j^{\prime}}\\!:\\!{j^{\prime}=j}}\\}}}}\ \prec:\
{\texttt{{int}}}{{{\\{{{j^{\prime}}\\!:\\!{0\leq
j^{\prime}-i^{\prime}<j-i}}\\}}}}$ the first of those is trivial; the second
reduces to the entailment $\displaystyle i<j;i^{\prime}=i+1;j^{\prime}=j$
$\displaystyle\ \vdash\ 0\leq j^{\prime}-i^{\prime}<j-i$

that is readily verified by the SMT solver. $\square$

###  9.4 Verification Conditions

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{checkT}&:&(\mathrm{\Gamma}\times
x\times E\times T\times M)\rightarrow(T\times C)\\\
\hline\cr\mathsf{checkT}(\mathrm{\Gamma},\ x,\ e,\ s,\ m)&\doteq&(t,\
({\overline{{y::s}}})\Rightarrow({{x::t^{\prime}}})\Rightarrow c)\\\
\quad\mbox{where}&&\\\ \quad\quad
c&=&\mathsf{check}(\mathrm{\Gamma};{\overline{\alpha};\overline{{y}\\!:\\!{s}};{x}\\!:\\!{t^{\prime}}},\
e^{*},\ t^{*})\\\ \quad\quad t^{\prime}&=&\mathsf{lim}(\mathrm{\Gamma},m,t)\\\
\quad\quad\forall{{\overline{\alpha}}\\!:\\!{k}}.{{\overline{{y}\\!:\\!{s}}}\rightarrow{t^{*}}}\
\mbox{as}\ t&=&\mathsf{fresh}(\mathrm{\Gamma},\ s)\\\
\quad\quad\Lambda{\overline{\alpha}}\\!:\\!{k}.{\lambda{\overline{y}}.\
{e^{*}}}&=&e\\\\[3.61371pt] \hline\cr\hline\cr\end{array}$ Figure 9.6:
Algorithmic Termination Checking

The algorithmic VC generation procedure for $\mathsf{\lambda_{\tau}}$ extends
how $\mathsf{check}$ generates Horn constraints for
$\texttt{{rec}}\;x={e_{1}}\\!:\\!{s_{1}}\;\texttt{{in}}\;e_{2}$, as summarized
in fig. 9.7. The implementation mirrors the declarative formulation Chk-Rec,
where we first check that the recursive definition $e_{1}$ is terminating, and
then use its type $t_{1}$ to check $e_{2}$.

_Algorithmic Termination Checking_ We implement the termination checking
judgment with a procedure $\mathsf{checkT}$ summarized in fig. 9.6, which
takes as input a recursive definition $x=e$ and the type $s$ and metric $m$
ascribed to the definition and returns as output a pair comprising the Horn VC
$c$ whose satisfiability indicates that the definition is well-typed and
terminating, and the type $t$ that subsequent binders can assume for $x$.
First, (as in fig. 5.5) we use $\mathsf{fresh}$ to instantiate the holes in
the specification $s$ with new Horn variables. Second, we obtain the body
$e^{*}$ and input binders $\overline{{y}\\!:\\!{s}}$. Finally, we invoke
$\mathsf{check}$ to compute the VC $c$ for the body in an environment
containing the input binders and the metric-limited type $t^{\prime}$. The
following states the correspondence between the algorithmic and declarative
versions of termination checking:

######  Proposition 9.4.1.

If $\mathsf{checkT}(\mathrm{\Gamma},\ x,\ e,\ s,\ m)=(t,c)$ and $c$ is Horn
satisfiable then $\mathrm{\Gamma}\vdash x=e:s/m\triangleright t$.

Following the same reasoning as the declarative checking, i.e. generating a VC
for the body in the metric-limited environment, $\mathsf{check}(\emptyset,\
e_{\texttt{r}},\ \ldots)$ generates the following VC for the term from eq.
9.6:

$\forall{i,j,i^{\prime},j^{\prime}}\\!:\\!{\texttt{{int}}}.\ i<j\Rightarrow
i^{\prime}=i+1\Rightarrow j^{\prime}=j\Rightarrow 0\leq
j^{\prime}-i^{\prime}<j-i$

The above VC is valid, which proves that range terminates.

$\begin{array}[]{lcl}\hline\cr\hline\cr\mathsf{check}&:&(\mathrm{\Gamma}\times
E\times T)\rightarrow C\\\ \hline\cr\mathsf{check}(\mathrm{\Gamma},\
\texttt{{rec}}\;x={e_{1}}\\!:\\!{s_{1}/m}\;\texttt{{in}}\;e_{2},\
t_{2})&\doteq&c_{1}\wedge({{x::t_{1}}})\Rightarrow c_{2}\\\
\quad\mbox{where}&&\\\
\quad\quad(t_{1},c_{1})&=&\mathsf{checkT}(\mathrm{\Gamma},\ x,\ e_{1},\
s_{1},\ m)\\\ \quad\quad
c_{2}&=&\mathsf{check}(\mathrm{\Gamma};{{x}\\!:\\!{t_{1}}},\ e_{2},\
t_{2})\\\\[3.61371pt] \hline\cr\hline\cr\end{array}$ Figure 9.7: Algorithmic
Checking for $\mathsf{\lambda_{\tau}}$, extends cases of fig. 8.8

###  9.5 Discussion

To recap, in $\mathsf{\lambda_{\tau}}$ we saw how to extend the type system to
also check that (recursive) functions terminate. We started with functions
like sum and sumT that recurse on some natural number n that directly
demonstrates termination. Then, we saw how to generalize the above idea to
decreasing expressions like the one that we used to demonstrate range
terminates. We saw how the idea of expressions can be generalized to sequences
to yield termination metrics which demonstrate termination via well-founded
lexicographic ordering. Finally, we saw how the notion of measures generalizes
the above to functions that work on datatypes. The key idea in all of the
above, is simply to check the body of the recursive call with a strengthened
type that limits (recursive) inputs to be well-founded, thereby enforcing
termination.

_Incompleteness_ Of course, thanks to the Halting problem there are
terminating functions that cannot be proven terminating via the approach shown
above, because there is no algorithmic procedure to find termination metrics,
and because the metrics themselves may, in general, fall outside the SMT
solver’s decidable theories. For example, it would be a major result to find a
suitable terminating metric for the collatz function [collatzWiki].

_Termination in Practice_ Nevertheless, there is evidence that the mechanisms
shown here with simple extensions, e.g. to account for mutually recursive