<p>Consider the following dependently-typed function:</p>
<pre><code>fill : n : Nat -&gt; a -&gt; Vector n a
</code></pre>
<p>What happens if you don't know what values <code>n</code> could be at compile time?</p>
<p>Wouldn't you have to monomorphise (instantiate) <code>fill</code> for every value of <code>Nat</code>?</p>
<p>Also wouldn't you have to monomorphise every call site of <code>fill</code>?</p>
<pre><code>let vec = fill n 1
</code></pre>
<p>would become</p>
<pre><code>switch(n)
case 1: let vec = fill n 1
case 2: let vec = fill n 1
...
case NatMax: let vec = fill n 1
</code></pre>
<p>How does this combinatorial explosion get constrained?</p>

<dependent-types>
How does compiling dependent types work?
CC BY-SA 4.0
2024-06-24T05:34:43.277Z
I believe the answer to "how do you monomorphize dependently-typed functions" is "you typically don't". You might be interested in how Swift (and most languages other than C++ and Rust) compile generics - there are [many benefits](https://faultlore.com/blah/swift-abi/#polymorphic-generics) to doing things mostly-dynamically and occasionally-monomorphically.
apropos
CC BY-SA 4.0
2024-06-24T08:42:48.397Z
That blog post is actually a very good answer to the question https://faultlore.com/blah/swift-abi/ thanks!
Tom Huntington
<p>While it’s possible to monomorphise if <code>n</code> is statically known, it’s not necessary just to compile the function.</p>
<p>Typically in a dependently typed language you have a “pi” quantifier, where <em>f</em> : Π(<em>x</em> : A). B[<em>x</em>] indicates that <em>f</em> is a function from an input value <em>x</em> of type A, to an output of a type B[<em>x</em>] that can depend on <em>x</em>.</p>
<p>The representation of <em>f</em> can vary based on A and B, and how the parameter <em>x</em> is used.</p>
<ul>
<li><p>If B[<em>x</em>] doesn’t mention x at all, this is a non-dependent function type, f : A → B. That’s not the case for <code>fill</code>, because <code>n : Nat</code> is mentioned in <code>a -&gt; Vector n a</code>.</p>
</li>
<li><p>If <em>f</em> doesn’t inspect the value of <em>x</em>, this is a parametric type—commonly A will be a kind like <code>Type</code>, and then this is a generic “for all” type ∀(x : A). B[x]. In <code>fill</code>, <code>a : Type</code> can be quantified in this way, but <code>n : Nat</code> can’t—we need to use the value of <code>n</code> to construct the resulting vector.</p>
</li>
<li><p>Therefore this is a “runtime-relevant” quantifier—it will become an ordinary value parameter, passed in at runtime.</p>
</li>
</ul>
<p>One of the challenges of implementing a dependently typed language is figuring out how to <em>avoid</em> keeping such values around at runtime when they’re not needed.</p>
<hr />
<p>This topic is related to a common misconception about dependent types, that they couldn’t possibly depend on runtime values. But of course they can!</p>
<p>For example, you can construct a vector of static length from a dynamic input list <code>xs</code>, and its dynamically computed length, <code>length xs</code>. You would then have a pair of a length and a vector of <em>that length</em>, whatever it may be, in the form of a sigma type Σ(<em>n</em> : Nat). Vector <em>n</em> A.</p>
<p>The compiler doesn’t need to know the concrete value of <em>n</em>, it just knows that there’s some relationship between the elements of this pair, represented by the variable <em>n</em>. If you want to make assumptions about <em>n</em>—say, that it’s nonzero—the compiler just needs to check that you’ve inserted an appropriate runtime test first.</p>
<p>In Idris you would check whether “decidable equality” <code>decEq n 0</code> returns <code>Yes zero</code> or <code>No nonzero</code>, where <code>zero</code> and <code>nonzero</code> are dummy “proof objects” that you can name and deal with explicitly, and pass to other functions—say, a division function that forces you to check for a zero denominator before calling it.</p>
<p>In languages with “flow typing”, those proof objects are built-in and implicit. So you may only need to write <code>if (n != 0) { … }</code> for the compiler to know that <em>n</em> is nonzero within that block, but you can’t extend the system with new types of checks.</p>

CC BY-SA 4.0
2024-06-27T02:11:17.500Z
2024-06-27T02:11:17.500Z
Jon Purdy
# How does compiling dependent types work?
Posted by: username_0 on 2024-06-24
Consider the following dependently-typed function:
fill : n : Nat -> a -> Vector n a

What happens if you don't know what values n could be at compile time?
Wouldn't you have to monomorphise (instantiate) fill for every value of Nat?
Also wouldn't you have to monomorphise every call site of fill?
let vec = fill n 1

would become
switch(n)
case 1: let vec = fill n 1
case 2: let vec = fill n 1
...
case NatMax: let vec = fill n 1

How does this combinatorial explosion get constrained?
**Tags:** dependent-types
> **Comments:**
> **username_1**: I believe the answer to "how do you monomorphize dependently-typed functions" is "you typically don't". You might be interested in how Swift (and most languages other than C++ and Rust) compile generics - there are [many benefits](https://faultlore.com/blah/swift-abi/#polymorphic-generics) to doing things mostly-dynamically and occasionally-monomorphically.  
> **username_0**: That blog post is actually a very good answer to the question https://faultlore.com/blah/swift-abi/ thanks!  
---
## 1 answers
### Answer by username_2 on 2024-06-27. Score: 5 | Accepted answer
While it’s possible to monomorphise if `n` is statically known, it’s not necessary just to compile the function.

Typically in a dependently typed language you have a “pi” quantifier, where *f* : Π(*x* : A). B[*x*] indicates that *f* is a function from an input value *x* of type A, to an output of a type B[*x*] that can depend on *x*.

The representation of *f* can vary based on A and B, and how the parameter *x* is used.

* If B[*x*] doesn’t mention x at all, this is a non-dependent function type, f : A → B. That’s not the case for `fill`, because `n : Nat` is mentioned in `a -> Vector n a`.
* If *f* doesn’t inspect the value of *x*, this is a parametric type—commonly A will be a kind like `Type`, and then this is a generic “for all” type ∀(x : A). B[x]. In `fill`, `a : Type` can be quantified in this way, but `n : Nat` can’t—we need to use the value of `n` to construct the resulting vector.
* Therefore this is a “runtime-relevant” quantifier—it will become an ordinary value parameter, passed in at runtime.

One of the challenges of implementing a dependently typed language is figuring out how to *avoid* keeping such values around at runtime when they’re not needed.

---

This topic is related to a common misconception about dependent types, that they couldn’t possibly depend on runtime values. But of course they can!

For example, you can construct a vector of static length from a dynamic input list `xs`, and its dynamically computed length, `length xs`. You would then have a pair of a length and a vector of *that length*, whatever it may be, in the form of a sigma type Σ(*n* : Nat). Vector *n* A.

The compiler doesn’t need to know the concrete value of *n*, it just knows that there’s some relationship between the elements of this pair, represented by the variable *n*. If you want to make assumptions about *n*—say, that it’s nonzero—the compiler just needs to check that you’ve inserted an appropriate runtime test first.

In Idris you would check whether “decidable equality” `decEq n 0` returns `Yes zero` or `No nonzero`, where `zero` and `nonzero` are dummy “proof objects” that you can name and deal with explicitly, and pass to other functions—say, a division function that forces you to check for a zero denominator before calling it.

In languages with “flow typing”, those proof objects are built-in and implicit. So you may only need to write `if (n != 0) { … }` for the compiler to know that *n* is nonzero within that block, but you can’t extend the system with new types of checks.
---
