13
$\begingroup$

I have been learning something about implementing dependent types, like this tutorial, 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?
Improve this question
$\endgroup$
2
  • $\begingroup$ 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.) $\endgroup$
    – xrq
    Dec 6 '18 at 19:16
  • $\begingroup$ Here's a paper on (dependently) typed assembly $\endgroup$
    – ice1000
    May 17 at 0:25
13
$\begingroup$

This is an interesting question! As Anthony'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. Apparently there is also this 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.

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$^*$ language which has distinct type-level and program-level terms.

Improve this answer
$\endgroup$
7
  • 1
    $\begingroup$ 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? $\endgroup$
    – Martin Berger
    Aug 28 '13 at 8:51
  • 2
    $\begingroup$ 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). $\endgroup$
    – cody
    Aug 29 '13 at 20:16
  • 1
    $\begingroup$ Also: to a certain extent, the solution 1 addresses it as well, by blurring the lines between interpreter and compiler. $\endgroup$
    – cody
    Aug 29 '13 at 20:17
  • 1
    $\begingroup$ I wonder if the futurama projections technique could be used to speed up the interpreter, effectively ending up with a compiler? $\endgroup$
    – Steven Shaw
    Jan 4 '19 at 10:17
  • 1
    $\begingroup$ The only thing I've seen is Unison unisonweb.org/2017-10-13/scala-world.html $\endgroup$
    – Steven Shaw
    Jan 5 '19 at 8:47
10
$\begingroup$

Edwin Brady's PhD thesis 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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.