7
$\begingroup$

I was trying to read a paper called Implementing a Modal Dependent Type Theory that implements a type that causes the context to "lock" but I don't know how it would be useful outside of formal proofs. What are the uses of modal types outside of formal proofs?

$\endgroup$
0

1 Answer 1

6
$\begingroup$

Modal types allow the type system to reason about scope in a very general sense. So potential applications are very broad and not thoroughly understood yet—it’s an active area of research. Potential applications include:

  • Staged metaprogramming
  • Distributed programming
  • Memory management
  • First-class control
  • Algebraic effects

Background

Here’s a typical sort of rule for typechecking a dependent function term:

$$\frac{\Gamma, x : A \vdash e : B}{\Gamma \vdash \lambda(x : A). e : \Pi(x : A). B}$$

Notice that the antecedent, $\Gamma, x : A \vdash e : B$, is a judgement about $e$, with a hypothesis $x : A$ in the context. The variable $x$ may appear free in the type $B$, but this isn’t represented internally in the type itself; it’s an external, metalogical feature of the type system.

Because of this, the two parts of a function term—namely, the variable binding $\lambda(x : A).$ and the body $e$—can’t be separated. Alone, neither of these parts is typeable; the former isn’t even syntactically valid.

Internalising a judgement as a type in the system, and thereby making it “first-class”, is a good way to add expressive power to a type system. Of course, usually this immediately raises serious challenges for typechecking, but I’ll set that aside for now.

The usual first-class function type $A \to B$ can be seen as an internal form of the external entailment judgement $x : A \vdash e : B$, and likewise the dependent function space $\Pi(x : A). B$ corresponds to the indexed version of that, $x : A \vdash e : B$, with the side condition that $x$ may be free in the type of the body, $B$.

But both of these judgements also have an implicit side condition: the variable x may be free in the body term itself, $e$. This is so pervasive an assumption that it’s rarely given much attention in a paper.

If we internalise that side condition, then what we get is something very interesting: an indexed modal type, usually written as $\square_{\{x : A\}} B$ or $[x : A] B$. This box modality describes the type of a term of type $B$ that may contain a free variable $x$ of type $A$. If we look at this in the context of the lambda rule:

$$\frac{\Gamma \vdash e : [x : A] B}{\Gamma \vdash \lambda(x : A). e : \Pi(x : A). B}$$

Now the variable binding is reflected in the type, and we can give a type to a lambda body, separately from its binder!

Examples

We can extend this naturally to a box indexed by a whole context, $[\Delta] A$. In the case that the context is empty, $\square A$, we have a closed term of type $A$, one that has no free variables. This is the sort of system described in the paper you link. A use for such types is typed metaprogramming, where $\square A$ represents an expression which will evaluate to a value of type $A$. Let’s call this const A. The box modality forms a comonad, so we have a projection extract : const A -> A whereby we can run a constant computation at compile time and splice its result into the program, but we don’t have an injection return : A -> const A, because we can’t convert a runtime value into a compile-time computation.

But what else can we do with these things, particularly when they’re indexed? Logically, boxes are very much like functions: $[A] B$ requires $A$ and produces $B$. However, their eliminators are different. We might type a dependent box eliminator like so:

$$\frac{\Gamma \vdash e_1 : [\Delta] A \qquad \Gamma, y : [\Delta] A \vdash B(y) : \ast \qquad \Gamma, z : [\Delta] A \vdash e_2 : B(\mathop{\textbf{box}} \Delta. z[\Delta/\Delta])}{\Gamma \vdash \mathop{\textbf{open}} x = e_1 \mathrel{\textbf{in}} e_2 : B(e_1)}$$

This is mostly plumbing—at a high level, it says that if we have a contextually typed term, then we can open it up and bind the contents to a metavariable. Notice that we use two different types of bindings in the context: $y : [\Delta] A$ says that this is a variable which has a boxed type, while $z [\Delta]: A$ says that this is a metavariable indexed by a context; all we can do with a metavariable is apply it to a substitution, and/or close it up again in a new box.

So whereas eliminating a function requires the input value to be given as an argument, eliminating a box only requires a value to be available for the duration of the application.

And this “contextual availability” can be given many different operational meanings, based on different modal axioms or different implementations of the same axioms.

We could use this to safely pass the address of a variable on the stack: [A] B could denote a function that produces a B from a reference to a value of type A, which is guaranteed to be “pinned” by the caller’s open … in …. Under this interpretation, []T is like Rust’s &'static T.

Algebraic effect handlers, capabilities, and dependency injection can also be handled this way—the caller grants the callee temporary access to some kind of resource.

[]T can denote any kind of “persistent T”: a source of values of type T, a copyable value of type T, a handle to a remote value of type T, and so on.

Finally, the dual of the comonadic box $\square$ modality [A] B is the monadic diamond $\diamond$ modality, in its indexed form $\langle A \rangle B$ or <A> B. Whereas the box is like a function or universal quantifier, the diamond is like a pair or existential quantifier: it describes a term along with a context that makes it valid. This could be used to model things like closures, stack frames, and effects.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .