Is compiler for dependent type much harder than an intepreter? 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?
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.