<p>I was trying to read a paper called <a href="https://jozefg.github.io/papers/2019-implementing-modal-dependent-type-theory.pdf" rel="noreferrer">Implementing a Modal Dependent Type Theory</a> that implements a type that causes the context to &quot;lock&quot; 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?</p>

<types><dependent-types>
What are the advantages of using Dependent Modal Types in a language?
<p>Modal types allow the type system to reason about <em>scope</em> in a very general sense. So potential applications are <em>very</em> broad and not thoroughly understood yet—it’s an active area of research. Potential applications include:</p>
<ul>
<li>Staged metaprogramming</li>
<li>Distributed programming</li>
<li>Memory management</li>
<li>First-class control</li>
<li>Algebraic effects</li>
</ul>
<h1>Background</h1>
<p>Here’s a typical sort of rule for typechecking a dependent function term:</p>
<p><span class="math-container">$$\frac{\Gamma, x : A \vdash e : B}{\Gamma \vdash \lambda(x : A). e : \Pi(x : A). B}$$</span></p>
<p>Notice that the antecedent, <span class="math-container">$\Gamma, x : A \vdash e : B$</span>, is a <em>judgement</em> about <span class="math-container">$e$</span>, with a hypothesis <span class="math-container">$x : A$</span> in the context. The variable <span class="math-container">$x$</span> may appear free in the type <span class="math-container">$B$</span>, but this isn’t represented internally in the <em>type</em> itself; it’s an external, metalogical feature of the type <em>system</em>.</p>
<p>Because of this, the two parts of a function term—namely, the variable binding <span class="math-container">$\lambda(x : A).$</span> and the body <span class="math-container">$e$</span>—can’t be separated. Alone, neither of these parts is typeable; the former isn’t even syntactically valid.</p>
<p>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.</p>
<p>The usual first-class function type <span class="math-container">$A \to B$</span> can be seen as an <em>internal</em> form of the <em>external</em> entailment judgement <span class="math-container">$x : A \vdash e : B$</span>, and likewise the dependent function space <span class="math-container">$\Pi(x : A). B$</span> corresponds to the indexed version of that, <span class="math-container">$x : A \vdash e : B$</span>, with the <em>side condition</em> that <span class="math-container">$x$</span> may be free in the <em>type</em> of the body, <span class="math-container">$B$</span>.</p>
<p>But both of these judgements also have an implicit side condition: the variable <em>x</em> may be free in the body <em>term</em> itself, <span class="math-container">$e$</span>. This is so pervasive an assumption that it’s rarely given much attention in a paper.</p>
<p>If we internalise <em>that</em> side condition, then what we get is something very interesting: an indexed modal type, usually written as <span class="math-container">$\square_{\{x : A\}} B$</span> or <span class="math-container">$[x : A] B$</span>. This box modality describes the type of a term of type <span class="math-container">$B$</span> that may contain a free variable <span class="math-container">$x$</span> of type <span class="math-container">$A$</span>. If we look at this in the context of the lambda rule:</p>
<p><span class="math-container">$$\frac{\Gamma \vdash e : [x : A] B}{\Gamma \vdash \lambda(x : A). e : \Pi(x : A). B}$$</span></p>
<p>Now the variable binding is reflected in the type, and we can give a type to a lambda body, <em>separately</em> from its binder!</p>
<h1>Examples</h1>
<p>We can extend this naturally to a box indexed by a whole context, <span class="math-container">$[\Delta] A$</span>. In the case that the context is empty, <span class="math-container">$\square A$</span>, we have a <em>closed term</em> of type <span class="math-container">$A$</span>, 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 <span class="math-container">$\square A$</span> represents an expression which <em>will</em> evaluate to a value of type <span class="math-container">$A$</span>. Let’s call this <code>const A</code>. The box modality forms a <em>comonad</em>, so we have a <em>projection</em> <code>extract : const A -&gt; A</code> whereby we can run a constant computation at compile time and splice its result into the program, but we <em>don’t</em> have an <em>injection</em> <code>return : A -&gt; const A</code>, because we can’t convert a runtime value into a compile-time computation.</p>
<p>But what else can we do with these things, particularly when they’re indexed? Logically, boxes are very much like functions: <span class="math-container">$[A] B$</span> requires <span class="math-container">$A$</span> and produces <span class="math-container">$B$</span>. However, their eliminators are different. We might type a dependent box eliminator like so:</p>
<p><span class="math-container">$$\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)}$$</span></p>
<p>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: <span class="math-container">$y : [\Delta] A$</span> says that this is a <em>variable</em> which has a boxed type, while <span class="math-container">$z [\Delta]: A$</span> says that this is a <em>metavariable</em> 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.</p>
<p>So whereas eliminating a function requires the input value to be <em>given</em> as an argument, eliminating a box only requires a value to be <em>available</em> for the duration of the application.</p>
<p>And this “contextual availability” can be given many different operational meanings, based on different modal axioms or different implementations of the same axioms.</p>
<p>We could use this to safely pass the address of a variable on the stack: <code>[A] B</code> could denote a function that produces a <code>B</code> from a reference to a value of type <code>A</code>, which is guaranteed to be “pinned” by the caller’s <code>open … in …</code>. Under this interpretation, <code>[]T</code> is like Rust’s <code>&amp;'static T</code>.</p>
<p>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.</p>
<p><code>[]T</code> can denote any kind of “persistent <code>T</code>”: a source of values of type <code>T</code>, a copyable value of type <code>T</code>, a handle to a remote value of type <code>T</code>, and so on.</p>
<p>Finally, the dual of the comonadic box <span class="math-container">$\square$</span> modality <code>[A] B</code> is the monadic diamond <span class="math-container">$\diamond$</span> modality, in its indexed form <span class="math-container">$\langle A \rangle B$</span> or <code>&lt;A&gt; B</code>. Whereas the box is like a function or universal quantifier, the diamond is like a pair or existential quantifier: it describes a term <em>along with</em> a context that makes it valid. This could be used to model things like closures, stack frames, and effects.</p>

CC BY-SA 4.0
2023-05-18T00:05:12.733Z
2023-08-10T22:51:47.593Z
2023-08-10T22:51:47.593Z
Jon Purdy
# What are the advantages of using Dependent Modal Types in a language?
Posted by: username_0 on 2023-05-17
I was trying to read a paper called [Implementing a Modal Dependent Type Theory](https://jozefg.github.io/papers/2019-implementing-modal-dependent-type-theory.pdf) 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?
**Tags:** types dependent-types
---
## 1 answers
### Answer by username_1 on 2023-05-18. Score: 7 | Accepted answer
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  `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.
---
