<p>Edwin Brady's <a href="https://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf" rel="nofollow noreferrer">PhD thesis</a> outlines how to construct a compiler for a dependently typed programming language.
I'm not an expert, but I'd say it's not extremely harder than implementing a System F-like compiler. Many of the principles are quite similar and some are the same (e.g. supercombinator compilation.) The thesis covers many other concerns.</p>

CC BY-SA 4.0
2013-08-27T19:08:35.950Z
2018-12-04T11:21:50.707Z
2018-12-04T11:21:50.707Z
Anthony
<p>This is an interesting question! As Anthony's answer suggests, one can use the usual approaches to compiling a non-dependent functional language, <strong>provided you already have an interpreter to evaluate terms for type-checking</strong>.</p>

<p>This is the approach taken by Edwin Brady. Now this is conceptually simpler, but it does lose the speed advantages of compilation when performing type checking. This has been addressed in several manners.</p>

<p>First, one can implement a virtual machine which compiles terms to byte-code on the fly to perform the conversion check. This is the idea behind <code>vm_compute</code> implemented in Coq by <a href="http://cristal.inria.fr/~xleroy/publi/strong-reduction.pdf" rel="noreferrer">Benjamin Gregoire</a>. Apparently there is also <a href="http://opus4.kobv.de/opus4-tuberlin/files/2859/kleeblatt_dirk.pdf" rel="noreferrer">this</a> thesis by Dirk Kleeblatt on this exact subject, but down actual machine code rather than a virtual machine.</p>

<p>Second, one may generate code in a more conventional language which, upon execution, checks all the conversions necessary to type-check a dependently typed program. This means we can use Haskell, say, to type-check an Agda module. The code can be compiled and run, and if it accepts, then the code in the dependently-type language can be assumed to be well-typed (barring implementation and compiler errors). I've first heard this approach suggested by <a href="http://www.cs.mcgill.ca/~mboes/papers/cpp11.pdf" rel="noreferrer">Mathieu Boesflug</a>.</p>

<p>Finally, one may require that the terms appearing in types and the terms intended to be run be part of two distinct languages. If the terms appearing at the type level do not themselves have dependent types, then one may compile in two stages: first, compile the "type-level" code and then you can execute this when checking the types of the "term-level" code. I'm not aware of any system that proceeds in this manner, but it is potentially possible for many systems, like Microsoft's <a href="http://research.microsoft.com/en-us/projects/fstar/" rel="noreferrer">F$^*$</a> language which has distinct type-level and program-level terms.</p>

CC BY-SA 3.0
2013-08-28T08:51:42.740Z
A bit tongue-in-cheeck: why would you bother writing a compiler if you have an interpreter doing the type-checking? After all, most (all?) serious users of dependently typed programming languages only care about the type-checker, using the language as a proof-assistant.  I certainly have never actually run any of my Agda or Coq programs. So if you care about speed, wouldn't you want to compile the type conversions?
Martin Berger
CC BY-SA 3.0
2013-08-29T20:16:37.680Z
The solutions 2 and 3 address this issue: you compile code which checks well-typedness (and in particular performs type conversions). My second remark is that you actually do want to run dependently typed code in some situations (see Idris, Ur/Web).
cody
CC BY-SA 3.0
2013-08-29T20:17:45.060Z
Also: to a certain extent, the solution 1 addresses it as well, by blurring the lines between interpreter and compiler.
cody
CC BY-SA 4.0
2018-12-06T19:15:00.490Z
@MartinBerger It is certainly not always the case: there is a Coq program that I have run many times and the name of the program is CompCert :-) But yes, a compiler for the type-check phase is still important for performance reasons.
xrq
CC BY-SA 4.0
2019-01-04T10:17:57.790Z
I wonder if the _futurama projections_ technique could be used to speed up the interpreter, effectively ending up with a compiler?
Steven Shaw
CC BY-SA 4.0
2019-01-05T03:12:58.773Z
@StevenShaw presumably, though I'll admit that I've never really seen the Futumura technique applied very effectively in the real world.
cody
CC BY-SA 4.0
2019-01-05T08:47:36.523Z
The only thing I've seen is Unison http://unisonweb.org/2017-10-13/scala-world.html
Steven Shaw
CC BY-SA 3.0
2013-08-27T21:29:56.383Z
2013-09-03T21:03:42.160Z
2013-09-03T21:03:42.160Z
cody
<p>I have been learning something about implementing dependent types, like <a href="http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/">this tutorial</a>, but most of them is implementing interpreters. My question is, it seems that implementing a compiler for dependent type is much harder than a compiler, because you can really evaluate the the dependent type arguments for type checking.</p>

<p>So</p>

<ul>
<li>Is my naive impression right?</li>
<li>If it is right, any example / resources about implementing a statically checked language supporting dependent type?</li>
</ul>

CC BY-SA 4.0
2018-12-06T19:16:50.033Z
No, as you can reduce the dependent types compiling problem to a known problem: (1) type check the program using an interpreter; (2) extract the program to OCaml/Haskell/whatever; (3) compile using `ocamlopt` or GHC :-) (This is the Coq and Agda approach, by the way.)
xrq
CC BY-SA 4.0
2021-05-17T00:25:58.040Z
Here's a [paper](https://www.cs.cmu.edu/~rwh/papers/dtal/icfp01.pdf) on (dependently) typed assembly
ice1000
<type-systems><compilers><dependent-type>
Is compiler for dependent type much harder than an intepreter?
molikto
# Is compiler for dependent type much harder than an intepreter?

(Asked by: username_0 on 2013-08-27)

I have been learning something about implementing dependent types, like [this tutorial](http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/), but most of them is implementing interpreters. My question is, it seems that implementing a compiler for dependent type is much harder than a compiler, because you can really evaluate the the dependent type arguments for type checking.

So

* Is my naive impression right?
* If it is right, any example / resources about implementing a statically checked language supporting dependent type?

**Tags:** type-systems, compilers, dependent-type

> **Comments:**
> **username_1**: No, as you can reduce the dependent types compiling problem to a known problem: (1) type check the program using an interpreter; (2) extract the program to OCaml/Haskell/whatever; (3) compile using `ocamlopt` or GHC :-) (This is the Coq and Agda approach, by the way.)  
> **username_2**: Here's a [paper](https://www.cs.cmu.edu/~rwh/papers/dtal/icfp01.pdf) on (dependently) typed assembly  

---

## 2 answers

### Answer by username_4 on 2013-08-27. Score: 13 | Accepted answer

This is an interesting question! As username_3's answer suggests, one can use the usual approaches to compiling a non-dependent functional language, **provided you already have an interpreter to evaluate terms for type-checking**.

This is the approach taken by Edwin Brady. Now this is conceptually simpler, but it does lose the speed advantages of compilation when performing type checking. This has been addressed in several manners.

First, one can implement a virtual machine which compiles terms to byte-code on the fly to perform the conversion check. This is the idea behind `vm_compute` implemented in Coq by [Benjamin Gregoire](http://cristal.inria.fr/~xleroy/publi/strong-reduction.pdf). Apparently there is also [this](http://opus4.kobv.de/opus4-tuberlin/files/2859/kleeblatt_dirk.pdf) thesis by Dirk Kleeblatt on this exact subject, but down actual machine code rather than a virtual machine.

Second, one may generate code in a more conventional language which, upon execution, checks all the conversions necessary to type-check a dependently typed program. This means we can use Haskell, say, to type-check an Agda module. The code can be compiled and run, and if it accepts, then the code in the dependently-type language can be assumed to be well-typed (barring implementation and compiler errors). I've first heard this approach suggested by [Mathieu Boesflug](http://www.cs.mcgill.ca/~mboes/papers/cpp11.pdf).

Finally, one may require that the terms appearing in types and the terms intended to be run be part of two distinct languages. If the terms appearing at the type level do not themselves have dependent types, then one may compile in two stages: first, compile the "type-level" code and then you can execute this when checking the types of the "term-level" code. I'm not aware of any system that proceeds in this manner, but it is potentially possible for many systems, like Microsoft's [F$^\*$](http://research.microsoft.com/en-us/projects/fstar/) language which has distinct type-level and program-level terms.

> **Comments:**
> **username_5**: A bit tongue-in-cheeck: why would you bother writing a compiler if you have an interpreter doing the type-checking? After all, most (all?) serious users of dependently typed programming languages only care about the type-checker, using the language as a proof-assistant.  I certainly have never actually run any of my Agda or Coq programs. So if you care about speed, wouldn't you want to compile the type conversions?  
> **username_4**: The solutions 2 and 3 address this issue: you compile code which checks well-typedness (and in particular performs type conversions). My second remark is that you actually do want to run dependently typed code in some situations (see Idris, Ur/Web).  
> **username_4**: Also: to a certain extent, the solution 1 addresses it as well, by blurring the lines between interpreter and compiler.  
> **username_1**: @MartinBerger It is certainly not always the case: there is a Coq program that I have run many times and the name of the program is CompCert :-) But yes, a compiler for the type-check phase is still important for performance reasons.  
> **username_6**: I wonder if the _futurama projections_ technique could be used to speed up the interpreter, effectively ending up with a compiler?  
> **username_4**: @StevenShaw presumably, though I'll admit that I've never really seen the Futumura technique applied very effectively in the real world.  
> **username_6**: The only thing I've seen is Unison http://unisonweb.org/2017-10-13/scala-world.html  

---

### Answer by username_3 on 2013-08-27. Score: 10

Edwin Brady's [PhD thesis](https://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf) outlines how to construct a compiler for a dependently typed programming language.
I'm not an expert, but I'd say it's not extremely harder than implementing a System F-like compiler. Many of the principles are quite similar and some are the same (e.g. supercombinator compilation.) The thesis covers many other concerns.


---

