Introduction

Conventions

When defining a term for the first time, it will be displayed in italics.

Basic ideas

Expressive, safe, fast, in that order.
Compile time "reference counting", leading to a borrow-checked system.
Expression blocks. loan and take.
Algebraic types. Inductive propositions. Subtypes.
No universe polymorphism, but still a universe hierarchy.
Quantitative type system. Usages correspond to the ideal storage mechanisms at runtime (given sufficient monomorphisation capabilities).
Monomorphisation is optional. Types at runtime; no decidable properties (what about sizeof?), so fully erasable. Function objects.
Reference tracking is inconsistent with quotients, as this would let us forget about a resource (e.g. function extensionality between a function that uses a resource and one that doesn't).

Feather syntax

Basic definitions

In the following, we assume familiarity with basic set theory.

Common sets

We define

\( \mathbb B = \{ \bot, \top \} \) is the two-element Boolean set, where \( \top \) represents truth and \( \bot \) represents falsity.
\( \mathbb N = \{ 0, 1, 2, \dots \} \) is the set of natural numbers, including zero.

Binary operations

A binary operation \( \otimes \) on a set \( X \) is a function \( X \times X \to X \). Such a binary operation is called

associative, if for all \( x, y, z \in X \), \( (x \otimes y) \otimes z = x \otimes (y \otimes z) \);
commutative, if for all \( x, y \in X \), \( x \otimes y = y \otimes x \).

Semirings

A semiring is a set \( R \) with elements \( 0, 1 \in R \) equipped with binary operations denoted \( + \) and \( \cdot \) such that

\( + \) is associative and commutative;
\( \cdot \) is associative and commutative;
additive identity: for all \( x \in R \), \( x + 0 = x \);
multiplicative identity: for all \( x \in R \), \( x \cdot 0 = 0 \) and \( x \cdot 1 = x \);
distributivity: for all \( x, y, z \in R \), \( (x + y) \cdot z = x \cdot z + y \cdot z \).

We write \( x y \) for \( x \cdot y \). We also assume that semirings satisfy the following two laws.

positivity: for \( x, y \in R \), \( x + y = 0 \) implies \( x = 0 \) and \( y = 0 \).
integrality: for \( x, y \in R \), \( xy = 0 \) implies either \( x = 0 \) or \( y = 0 \).

We define the semiring \( R_\omega = \{ 0, 1, \omega \} \) with operations given by

\( 1 + 1 = \omega \);
\( 1 + \omega = \omega \);
\( \omega + \omega = \omega \);
\( \omega \cdot \omega = \omega \).

One can check that this structure is indeed a semiring, and satisfies positivity and integrality.

Precontexts and preterms are defined as syntax adhering to a particular grammar. See Syntax and Semantics of Quantitative Type Theory (Atkey, 2018) for more information. Before defining these grammars, we make a few initial definitions.

Usages

An extended usage, to be interpreted as an element of the semiring \( R_\omega \), is of the form \[ \pi ::= 0 \mid 1 \mid \omega \] A (binary) usage, to be interpreted as either the element \( 0 \) or \( 1 \) in \( R_\omega \), is of the form \[ \sigma ::= 0 \mid 1 \] In our theory, terms all have an annotated binary usage. Variables in contexts, however, may be annotated with \( 0, 1 \) or \( \omega \) usage. The usage \( \omega \) records the fact that a resource was used multiple times; a context in which this occurs cannot typically be used in a derivation for a closed term. There is an exception, however, in the form of copyable types. The copying rule, seen later, roughly means that if we can derive a judgment under the assumption \( x \overset\omega : \alpha \), and \( \alpha \) is a copyable type, then we can derive the same consequent under the weaker assumption \( x \overset 1 : \alpha \).

Names

A name, denoted \( x, y, z \), is a nonempty sequence of Unicode code points in the following Unicode character categories:

L* Letters
N* Numbers
S* Symbols

A qualified name, denoted \( Q \), is of the form \[ Q ::= x \mid Q :: x \]

Universes

A universe, interpreted as an element of the set of natural numbers \( \mathbb N \), is of the form \[ u, v, w ::= \{0, 1, 2, \dots \} \] We define the operations of maximum and impredicative maximum by \[ \mathsf{max}(u,v) = \begin{cases} u & \text{if } u > v \\ v & \text{otherwise} \end{cases};\quad \mathsf{imax}(u,v) = \begin{cases} 0 & \text{if } v = 0 \\ \mathsf{max}(u,v) & \text{otherwise} \end{cases} \]

Preterms

A preterm, denoted \( a, b, c, \alpha, \beta, \gamma \), is given by one of the following syntactic introduction rules.

Functional rules

The basic introduction rules of functional programming are:

a local variable \( x \);
an application \( a\ b \);
an abstraction (or \( \lambda \)-abstraction) \( \lambda (x \overset\sigma : \alpha).\, a \);
a function type (or \( \Pi \)-type) \( (x \overset\sigma : \alpha) \to \beta \);
a let expression \( \mathsf{let}\ x = a;\; b \);
a sort \( \mathsf{Sort}\ u \).

Note that the arguments in \( \lambda \)-abstractions and \( \Pi \)-types are annotated with a binary usage, stating whether the argument has runtime presence or not. Importantly, there is no way for a function to consume \( \omega \) copies of an argument.

We write \( \mathsf{Prop} = \mathsf{Sort}\ 0 \) and \( \mathsf{Type}\ u = \mathsf{Sort}\ (u + 1) \).

Environmental rules

The introduction rules relating to declarations in the environment, such as algebraic types, are:

an instantiate expression (or inst expression) \( \mathsf{inst}\ Q \);
an intro expression \( \mathsf{intro}\ Q\ a_1\ \dots\ a_r\ \mathsf{variant}\ x\ \mathsf{with}\ z_1 \mapsto c_1, \dots, z_n \mapsto c_n \);
a match expression \( \mathsf{match}\ a\ \mathsf{return}\ \alpha\ \mathsf{with}\ y_1 \mapsto b_1, \dots, y_n \mapsto b_n \);
a fix expression \( \mathsf{fix}\ (x \overset\sigma : \alpha)\ \mathsf{return}\ \beta\ \mathsf{with}\ y.\, a \).

In a match expression, since the type we return could depend on the value of the major premise \( a \), we explicitly specify the type \( \alpha \) to return.

Borrowing rules

The introduction rules relating to borrowing are:

a reference type or borrowed type \( \mathsf{ref}\ \alpha \);
a dereference expression \( *a \);
a loan expression \( \mathsf{loan}\ x\ \mathsf{as}\ y\ \mathsf{with}\ z;\; b \);
a take expression \( \mathsf{take}\ x\ \mathsf{with}\ y_1 \mapsto a_1, \dots, y_n \mapsto a_n;\; b \);
an in expression \( a\ \mathsf{in}\ b \).

In a loan expression, \( x \) is a local variable to be loaned, \( y \) is the name to assign to the borrow, and \( z \) is a local variable which will store a proof of the proposition \( *y = x \). In the surface-level Quill syntax, a new name is not bound when loaning a variable, but it can be addressed using the syntax \( \&x \).

In a take expression, \( x \) is the name of a local variable that was loaned earlier; this expression should be in some subexpression of the right hand side of a \( \mathsf{loan} \) expression. Each \( y_i \) is intended to be the name of a local variable in the current context, but not in the context at the time of loaning, and the \( a_i \) is a proof that nothing depending on the memory containing \( x \) occurs in the value assigned to \( y_i \).

Precontexts

A precontext is of the form \[ \Gamma ::= \diamond \mid \Gamma, x \overset\pi : \alpha \] We suppress the syntax "\( \diamond, \)" at the beginning of the expression for a precontext. We identify precontexts that are equal up to reordering, so for example, \( x \overset{\pi_1} : \alpha, y \overset{\pi_2} : \beta \) is considered equal to \( y \overset{\pi_2} : \beta, x \overset{\pi_1} : \alpha \). Formally, a precontext is given by the multiset of its entries.

We can define scaling of precontexts by \[ \pi(\diamond) = \diamond;\quad \pi(\Gamma, x \overset{\pi'} : \alpha) = \pi(\Gamma), x \overset{\pi\pi'} : \alpha \] If \( 0\Gamma_1 = 0\Gamma_2 \), then \( \Gamma_1 \) and \( \Gamma_2 \) contain the same variables with the same types, but possibly with different usage annotations. In this case, we define addition of precontexts by \[ \diamond + \diamond = \diamond;\quad (\Gamma_1, x \overset{\pi_1} : \alpha) + (\Gamma_2, x \overset{\pi_2} : \alpha) = (\Gamma_1 + \Gamma_2), x \overset{\pi_1 + \pi_2} : \alpha \]

Pre-environments

Pre-datatypes

Feather's algebraic types are defined as follows.

A field is of the form \[ F ::= z \overset\sigma : \gamma \] A variant is of the form \[ V ::= \varepsilon \mid F,V \] A pre-datatype is \[ T ::= \mathsf{data}\ u\ (x_1 : \alpha_1), \dots, (x_r : \alpha_r) \Rightarrow y_1 \mapsto V_1; \dots; y_n \mapsto V_n \]

Fields represent the objects contained within an algebraic data type. Each field is tagged with a (binary) usage \( \sigma \), describing whether the field is to be stored at runtime.

The variants of a datatype are interpreted as a partition of the data type into disjoint sets. Each variant in a datatype is tagged with its name.

A datatype has a universe level \( u \) in which the type lives, then a list of parameters \( \alpha_1, \dots, \alpha_r \), and finally a list of possible variants. No usage information is attached to the parameters, as no resources are required for type creation. In this way, an algebraic datatype is a "sum of product types".

Pre-propositions

Feather's type theory features an impredicative, proof-irrelevant universe of propositions. We separate propositions and datatypes in order to simplify runtime code; propositions can be entirely erased, so the runtime does not need to know about the additional flexibility offered by proposition types.

A propositional field is of the form \[ F^P ::= z : \gamma \] A propositional variant is of the form \[ V^P ::= \varepsilon \mid F^P,V^P \] A pre-proposition is \[ \begin{aligned} P ::=\mathsf{prop}\ &(x_1 : \alpha_1), \dots, (x_r : \alpha_r) \mid \beta_1, \dots, \beta_s \Rightarrow \\ & y_1 \mapsto V^P_1 : b_{11}, \dots, b_{1s}; \dots; y_n \mapsto V^P_n : b_{n1}, \dots, b_{ns} \end{aligned} \]

Pre-propositions are like pre-datatypes, but have more expressive flexibility. They always have multiplicity 0. The \( \alpha_i \) are called the global parameters, and the \( \beta_j \) are called the index parameters. Each variant \( v \) specifies the index parameters \( b_{v1} : \beta_1, \dots, b_{vs} : \beta_s \) associated to it.

Pre-definitions

A pre-definition is of the form \[ D ::= \mathsf{def}\ a \overset\sigma : \alpha \]

Pre-environments

Pre-environments store named datatypes, propositions, and definitions. Formally, a pre-environment is of the form \[ \Pi ::= \diamond \mid \Pi, Q = T \mid \Pi, Q = P \mid \Pi, Q = D \] As with precontexts, we suppress the "\( \diamond, \)" syntax, and we consider two pre-environments identical if they agree up to reordering. There is no scaling operation defined on pre-environments.

Judgments

We distinguish preterms from terms, precontexts from contexts, and pre-environments from environments. In order to do this, we make use of several judgments expressed in the form of natural deduction.

The judgment \( \Pi\ \mathsf{env} \) states that the pre-environment \( \Pi \) is an environment.
The judgment \( \Pi \vdash \Gamma\ \mathsf{ctx} \) states that the precontext \( \Gamma \) is a context in the environment \( \Pi \).
The judgment \( \Pi \mid \Gamma \vdash a \overset\sigma : \alpha \) states that the preterm \( a \) is a term of binary usage \( \sigma \) and type \( \alpha \) in the environment \( \Pi \) and context \( \Gamma \).
The judgment \( \Pi \mid \Gamma \vdash a \equiv b \) states that the preterms \( a \) and \( b \) are definitionally equal.

Admissible rules

We construct our theory in such a way that the following rules are admissible. \[ \frac{\Pi \mid \Gamma \vdash a \overset\sigma : \alpha}{\Pi \vdash \Gamma\ \mathsf{ctx}};\quad \frac{\Pi \mid \Gamma \vdash a \equiv b}{\Pi \vdash \Gamma\ \mathsf{ctx}};\quad \frac{\Pi \vdash \Gamma\ \mathsf{ctx}}{\Pi\ \mathsf{env}} \] \[ \frac{\Pi \vdash \Gamma_1\ \mathsf{ctx} \quad 0\Gamma_1 = 0\Gamma_2}{\Pi \vdash \Gamma_2\ \mathsf{ctx}};\quad \frac{\Pi \mid \Gamma \vdash a \overset\sigma : \alpha}{\Pi \mid 0\Gamma \vdash a \overset 0 : \alpha} \]

Contexts

We stipulate the rules \[ \frac{\Pi\ \mathsf{env}}{\Pi \vdash \diamond\ \mathsf{ctx}};\quad \frac{\Pi \vdash \Gamma\ \mathsf{ctx} \quad \Pi \vdash 0\Gamma \vdash \alpha \overset 0 : \mathsf{Sort}\ u}{\Pi \vdash \Gamma, x \overset\pi : \alpha\ \mathsf{ctx}} \]

Functional typing rules

We present typing rules for each of the functional expression types.

Local variables

We can obtain a local variable from a context. \[ \frac{\Pi \vdash 0\Gamma, x \overset\sigma : \alpha \ \mathsf{ctx}}{\Pi \mid 0\Gamma, x \overset\sigma : \alpha \vdash x \overset\sigma : \alpha} \] The use of \( 0\Gamma \) implies that the resources in the context are not used in the construction of the term \( x \).

Applications

\[ \frac{\Pi \mid \Gamma_1 \vdash a \overset{\sigma_1} : (x \overset{\sigma_2} : \alpha) \to \beta \quad \Pi \mid \Gamma_2 \vdash b \overset{\sigma_1 \sigma_2} : \alpha \quad 0\Gamma_1 = 0\Gamma_2}{\Pi \mid \Gamma_1 + \Gamma_2 \vdash a\ b \overset{\sigma_1} : \beta[b/x]} \]

Note that unless \( \sigma_1 = \sigma_2 = 1 \), we used no resources to construct \( b \), due to the "zero needs nothing" rule. (TODO: Describe this rule.) The context in the conclusion of this rule can therefore be reduced from the standard QTT form of \( \Gamma_1 + \sigma_2 \Gamma_2 \) to just \( \Gamma_1 + \Gamma_2 \). This observation simplifies our presentation of the function application rule somewhat. In quantitative type theory more generally, the usage \( \sigma_2 \) could be any element of an arbitrary semiring \( R \), so the same modification cannot be made there.

We describe the interpretations of each instance of this rule.

\( \sigma_1 = 0, \sigma_2 = 0 \). We consume and produce no resources. This is a function application rule that ignores usage labels.
\( \sigma_1 = 0, \sigma_2 = 1 \). The function expects that its parameter is a resource. But since the function is erased, the computation is not executed at runtime, so the resource is not needed. The conclusion of the judgment is therefore \( \Pi \mid \Gamma_1 + 0\Gamma_2 \vdash a\ b \overset 0 : \beta[b/x] \).
\( \sigma_1 = 1, \sigma_2 = 0 \). In this case, the function is a resource, and its argument is erased. We can evaluate the function on an erased argument.
\( \sigma_1 = 1, \sigma_2 = 1 \). This is the standard function application rule from linear logic. The function and its argument are used exactly once.

Abstractions

\[ \frac{\Pi \mid \Gamma, x \overset{\sigma_1\sigma_2} : \alpha \vdash b \overset{\sigma_1} : \beta}{\Pi \mid \Gamma \vdash \lambda(x \overset{\sigma_2} : \alpha).\,b \overset{\sigma_1} : (x \overset{\sigma_2} : \alpha) \to \beta} \]

Function types

\[ \frac{\Pi \mid 0\Gamma \vdash \alpha \overset 0 : \mathsf{Sort}\, u \quad \Pi \mid 0\Gamma, x \overset 0 : \alpha \vdash \beta \overset 0 : \mathsf{Sort}\, v}{\Pi \mid 0\Gamma \vdash (x \overset \sigma : \alpha) \to \beta \overset 0 : \mathsf{Sort}\, \mathsf{imax}(u, v)} \]

Let expressions

\[ \frac{\Pi \mid \Gamma_1 \vdash a \overset{\sigma_1\sigma_2} : \alpha \quad \Pi \mid \Gamma_2, x \overset{\sigma_1\sigma_2} : \alpha \vdash b \overset{\sigma_2} : \beta \quad 0\Gamma_1 = 0\Gamma_2}{\Pi \mid \Gamma_1 + \Gamma_2 \vdash \mathsf{let}_{\sigma_1\sigma_2}\ x = a;\, b \overset{\sigma_2} : \beta} \]

This rule admits three forms.

\( \sigma_1 \) arbitrary, \( \sigma_2 = 0 \). The ambient context is erased, so the let-binding is also erased.
\( \sigma_1 = 0, \sigma_2 = 1 \). The ambient context exists at runtime, but we are constructing an erased value.
\( \sigma_1 = 1, \sigma_2 = 1 \). The standard \( \mathsf{let} \) rule from linear logic.

Sort expressions

\[ \frac{\Pi \vdash 0\Gamma\ \mathsf{ctx}}{\Pi \mid 0\Gamma \vdash \mathsf{Sort}\ u \overset 0 : \mathsf{Sort}\ (u + 1)} \]

Environmental typing rules

For clarity, we describe the typing rule for some expressions in English rather than through mathematical symbols.

Instantiate expressions

In the following rules, the precise syntax of the \( \mathsf{data} \) and \( \mathsf{prop} \) intro rules is shortened for brevity.

\[ \frac{\Pi, Q = \mathsf{data}\ u\ \dots \vdash 0\Gamma\ \mathsf{ctx}}{\Pi, Q = \mathsf{data}\ u\ \dots \mid 0\Gamma \vdash \mathsf{inst}\ Q \overset 0 : \mathsf{Type}\ u} \]

This rule ascribes meaning to the act of placing a datatype in the environment, by allowing it to be used as a type in an appropriate context. In particular, the universe \( u \) defines the sort in which the datatype resides.

\[ \frac{\Pi, Q = \mathsf{prop}\ \dots \vdash 0\Gamma\ \mathsf{ctx}}{\Pi, Q = \mathsf{prop}\ \dots \mid 0\Gamma \vdash \mathsf{inst}\ Q \overset 0 : \mathsf{Prop}} \]

This rule is like the previous one, except that propositions always live in the sort \( \mathsf{Prop} \).

\[ \frac{\Pi, Q = \mathsf{def}\ a \overset\sigma : \alpha \vdash 0\Gamma\ \mathsf{ctx}}{\Pi, Q = \mathsf{def}\ a \overset\sigma : \alpha \mid 0\Gamma \vdash \mathsf{inst}\ Q \overset{\sigma\sigma'} : \alpha} \]

When instantiating a definition, we can choose to instantiate it with the usage it was defined, or erase it.

Intro expressions

Suppose the environment \( \Pi \) contains \[ \mathsf{data}\ u\ (x_1 : \alpha_1), \dots, (x_r : \alpha_r) \Rightarrow y_1 \mapsto V_1; \dots; y_n \mapsto V_n \] assigned to the name \( Q \), and we wish to assign a type to the term \[ t ::= \mathsf{intro}\ Q\ a_1\ \dots\ a_r\ \mathsf{variant}\ y\ \mathsf{with}\ z_1 \mapsto c_1, \dots, z_m \mapsto c_m \] We assume that we wish to construct \( t \) with usage \( \sigma \). First, we check that for each \( i = 1, \dots, r \), we have \[ \Pi \mid 0\Gamma \vdash a_i \overset 0 : \alpha_i[a_1/x_1, \dots, a_{i-1}/x_{i-1}] \] This ensures that the global parameters for the datatype are type correct. We then check that \( y \) is one of the variants \( y_1, \dots, y_n \). Suppose \( y = y_i \), and \( V_i = z_1 \overset{\sigma_1} : \gamma_1, \dots, z_m \overset{\sigma_m} : \gamma_m \). We implicitly assume in this statement that the names of the fields in \( V_i \) agree with the arguments of the \( \mathsf{intro} \) expression. Then for each \( j = 1, \dots, m \), we check that \[ \Pi \mid \Gamma \vdash c_j \overset {\sigma\sigma_j} : \gamma_j[a_1/x_1, \dots, a_n/x_n, c_1/z_1, \dots, c_{j-1}/z_{j-1}] \] If all of these constraints can be satisfied concurrently (using the sum of the relevant contexts \( \Gamma \)), we conclude \[ t \overset\sigma : Q\ a_1\ \dots\ a_r \] Suppose instead that \( \Pi \) assigns the proposition type \[ \begin{aligned} \mathsf{prop}\ &(x_1 : \alpha_1), \dots, (x_r : \alpha_r) \mid \beta_1, \dots, \beta_s \Rightarrow \\ & y_1 \mapsto V^P_1 : b_{11}, \dots, b_{1s}; \dots; y_n \mapsto V^P_n : b_{n1}, \dots, b_{ns} \end{aligned} \] to the name \( Q \). We first check that all of the global parameters are correctly typed as above, and similarly ensure that \( y = y_i \) for some \( i \). For each field \( j \) in the propositional variant \( V_i^P = z_1 : \gamma_1, \dots, z_m : \gamma_m \), we verify that \[ \Pi \mid 0\Gamma \vdash c_j \overset 0 : \gamma_j[a_1/x_1, \dots, a_n/x_n, c_1/z_1, \dots, c_{j-1}/z_{j-1}] \] Then, we conclude \[ t \overset 0 : Q\ a_1\ \dots\ a_r\ (b_{i1}\ \dots\ b_{is})[a_1/x_1, \dots, a_r/x_r, c_1/z_1, \dots, c_m/z_m] \]

Match expressions

Suppose we wish to typecheck \[ t ::= \mathsf{match}\ a\ \mathsf{return}\ \alpha\ \mathsf{with}\ y_1 \mapsto b_1, \dots, y_n \mapsto b_n \] First, suppose \( \Pi \) contains \[ \mathsf{data}\ u\ (x_1 : \alpha_1), \dots, (x_r : \alpha_r) \Rightarrow y_1 \mapsto V_1; \dots; y_n \mapsto V_n \] assigned to the name \( Q \), and we check \( a \overset \sigma : Q\ a_1\ \dots\ a_r \). Implicitly, we are assuming that the names of the variants of \( Q \) match with the arguments of the \( \mathsf{match} \) expression. We then check that, for some \( u \), \[ \Pi \mid 0\Gamma \vdash \alpha \overset 0 : (x \overset 0 : Q\ a_1\ \dots\ a_r) \to \mathsf{Sort}\ u \] We now verify that each \( b_i \) is well-typed. Specifically, if \( V_i = z_1 \overset{\sigma_1} : \gamma_1, \dots, z_m \overset{\sigma_m} : \gamma_m \), we check that \[ \begin{aligned} \Pi \mid \Gamma \vdash\, &b_i \overset\sigma : (z_1 \overset{\sigma_1} : \gamma_1) \to \dots \to (z_m \overset{\sigma_m} : \gamma_m) \to \\ &\alpha\ (\mathsf{intro}\ Q\ a_1\ \dots\ a_r\ \mathsf{variant}\ y_i\ \mathsf{with}\ z_1 \mapsto z_1, \dots, z_m \mapsto z_m) \end{aligned} \] If all of these checks pass, we conclude \[ \Pi \mid \Gamma \vdash t \overset \sigma : \alpha\ a \] Now, suppose \( \Pi \) binds the name \( Q \) to the proposition \[ \begin{aligned} \mathsf{prop}\ &(x_1 : \alpha_1), \dots, (x_r : \alpha_r) \mid \beta_1, \dots, \beta_s \Rightarrow \\ & y_1 \mapsto V^P_1 : b_{11}, \dots, b_{1s}; \dots; y_n \mapsto V^P_n : b_{n1}, \dots, b_{ns} \end{aligned} \] In this case, we require \( \sigma = 0 \). We check \( a \overset 0 : Q\ a_1\ \dots\ a_r\ a_1'\ \dots\ a_s' \). Then, we verify that \[ \Pi \mid 0\Gamma \vdash \alpha \overset 0 : (x_1' \overset 0 : \beta_1) \to \dots \to (x_s' \overset 0 : \beta_s) \to (x \overset 0 : Q\ a_1\ \dots\ a_r\ x_1'\ \dots\ x_s') \to \mathsf{Sort}\ u \] At this stage, we ensure that \( u \) is a valid universe to eliminate into for this particular proposition. We perform the following sequence of checks.

If \( Q \) has no variants, \( u \) may be any universe.
If \( Q \) has at least two variants, \( u \) must be \( 0 \); we can only eliminate into \( \mathsf{Prop} \).
Suppose \( Q \) has one variant \( V^P \). If every field satisfies either
1. its type lies in \( \mathsf{Prop} \); or
2. it occurs in one of the index parameters \( b_{11}, \dots, b_{1s} \),
then \( u \) may be any universe. If any field fails to satisfy both requirements, \( u \) must be \( 0 \).

We now check that each \( b_i \) is well-typed. Suppose we are considering the variant \( V^P_i = (z_1 : \gamma_1, \dots, z_m : \gamma_m) : b_{i1}, \dots, b_{is} \). Then, we check \[ \begin{aligned} \Pi \mid \Gamma \vdash\, &b_i \overset 0 : (z_1 \overset 0 : \gamma_1) \to \dots \to (z_m \overset 0 : \gamma_m) \to \\ &\alpha\ b_{i1}\ \dots\ b_{is}\ (\mathsf{intro}\ Q\ a_1\ \dots\ a_r\ \mathsf{variant}\ y_i\ \mathsf{with}\ z_1 \mapsto z_1, \dots, z_m \mapsto z_m) \end{aligned} \] We finally conclude \[ \Pi \mid \Gamma \vdash t \overset 0 : \alpha\ a_1'\ \dots\ a_s'\ a \]

TODO: Can we get away with \( \sigma \) usage in some cases, such as to perform casts between propositionally equal types?

Fix expressions

Finally, suppose we wish to typecheck \[ \mathsf{fix}\ (x \overset\sigma : \alpha)\ \mathsf{return}\ \beta\ \mathsf{with}\ y.\, a \] First, we ensure that \( \alpha \) is an algebraic datatype or a propositional type. If \( \alpha \) is a propositional type, we assume \( \sigma = 0 \). We now check that \[ \Pi \mid 0\Gamma \vdash \beta \overset 0 : (x \overset 0 : \alpha) \to \mathsf{Sort}\ u \] and \[ \Pi \mid \Gamma, x \overset\sigma : \alpha, y \overset\sigma : (x \overset\sigma : \alpha) \Rightarrow \beta\ x \vdash a \overset\sigma : \beta\ x \] Now, we check that each use of \( y \) in \( a \) occurs as a function in an application expression, where the argument is one of the bound variables from a match expression on \( x \), possibly with some arguments applied to it. This restriction ensures that the fixpoint function we describe will terminate on all inputs.

Borrowing typing rules

We assume \( \Pi \) contains the definition \( ¬ : \mathsf{Prop} \to \mathsf{Prop} \).

For each \( A : \mathsf{Sort}\ u \), we assume \( \Pi \) contains the type \( =_A \).

The global parameters are \( A : \mathsf{Sort}\ u \) and \( a : A \).
There is one index parameter, \( b : A \).
There is one variant, named \( \mathsf{refl} \), with no fields, and index parameter assignment \( a \).

Reference types

\[ \frac{\Pi \mid 0\Gamma \vdash \alpha \overset 0 : \mathsf{Sort}\ u}{\Pi \mid 0\Gamma \vdash \mathsf{ref}\ \alpha \overset 0 : \mathsf{Sort}\ u} \]

Dereference expressions

\[ \frac{\Pi \mid 0\Gamma \vdash a \overset 0 : \mathsf{ref}\ \alpha}{\Pi \mid 0\Gamma \vdash *a \overset 0 : \alpha} \]

Loan expressions

\[ \frac{\Pi \mid \Gamma, x \overset 0 : \alpha, y \overset 1 : \mathsf{ref}\ \alpha, z \overset 0 : x =_{\mathsf{ref}\ \alpha} *y \vdash b \overset 1 : \beta}{\Pi \mid \Gamma, x \overset 1 : \alpha \vdash \mathsf{loan}\ x\ \mathsf{as}\ y\ \mathsf{with}\ z;\; b \overset 1 : \beta} \]

We add the additional constraint that, in every code path in \( b \), there is a unique \( \mathsf{take}\ x \) expression, not enclosed in any abstraction.

Take expressions

\[ \frac{\Pi \mid \Gamma, x \overset 1 : \alpha \vdash b \overset 1 : \beta \quad \Pi \mid 0\Gamma, x \overset 0 : \alpha \vdash a_1 \overset 0 : ¬(x\ \mathsf{in}\ y_1) \ \dots \ \Pi \mid 0\Gamma, x \overset 0 : \alpha \vdash a_n \overset 0 : ¬(x\ \mathsf{in}\ y_n)}{\Pi \mid \Gamma, x \overset 0 : \alpha \vdash \mathsf{take}\ x\ \mathsf{with}\ y_1 \mapsto a_1, \dots, y_n \mapsto a_n;\; b \overset 1 : \beta} \]

We add the constraint that this \( \mathsf{take} \) expression occurs in the body of a \( \mathsf{loan}\ x \) expression. We also stipulate that the names \( y_1, \dots, y_n \) correspond to the variables bound between the loan and take expressions.

In expressions

\[ \frac{\Pi \mid 0\Gamma \vdash a \overset 0 : \mathsf{ref}\ \alpha \quad \Pi \mid 0\Gamma \vdash b \overset 0 : \beta}{\Pi \mid 0\Gamma \vdash a\ \mathsf{in}\ b \overset 0 : \mathsf{Prop}} \]

Definitional equality

The rules used to derive definitional equality require no resources.

Equality as an equivalence relation

The reflexivity rule is \[ \frac{\Pi \mid 0\Gamma \vdash a \overset 0 : \alpha}{\Pi \mid 0\Gamma \vdash a \equiv a} \] The symmetry rule is \[ \frac{\Pi \mid 0\Gamma \vdash a \equiv b}{\Pi \mid 0\Gamma \vdash b \equiv a} \] The transitivity rule is \[ \frac{\Pi \mid 0\Gamma \vdash a \equiv b \quad \Pi \mid 0\Gamma \vdash b \equiv c}{\Pi \mid 0\Gamma \vdash a \equiv c} \]

Type conversion

Terms can be reinterpreted as a definitionally equal type. The type conversion rule is \[ \frac{\Pi \mid \Gamma \vdash a \overset\sigma : \alpha \quad \Pi \mid 0\Gamma \vdash \alpha \equiv \beta}{\Pi \mid \Gamma \vdash a \overset\sigma : \beta} \]

Quill and Feather specifications