Functional programing and intensional type theory

Question

I know very little about how computers work, so please excuse my ignorance!

I think of the Glasgow Haskell Compiler as a program that eats up extensional type theory and spits out a program which can be run on my computer.

Question 1: Would it be possible to write a compiler which eats intensional type theory and spits out programs? Inpaticular, I want the compiler to understand higher inductive types.

I am vaguely aware of the notion of turing completeness, so I don't expect this hypothetical programing language to be anymore powerful than any other programing language.

Question 2: Supposing that the answer to question 1 is yes, would there be any reason to write such a compiler?

Answer 1

GHC doesn't eat extensional dependent type theory. The type theory of GHC has some fancy bells and whistles that allow you to fake some things you can do with dependent types, but it isn't truly dependently typed. There are, however, "compilers" that eat true (extensional) dependent type theory, such as Agda. (I put "compiler" in quotes because it's sometimes tricky — though not always impossible — to separate compile-time from run-type in a dependently typed language.) Moreover, Agda has a flag --without-k which transforms its input into intensional dependent type theory, in roughly Martin-Lof's original sense.

The question of whether such a compiler can be extended to new homotopy-theoretic features such as higher inductive types and univalence is an important question of current research in homotopy type theory. One can fake them in order to check proofs involving them, but they don't in general "compute" that way. Various people (Coquand et. al., Licata-Brunerie) are currently investigating versions of ITT in which univalence and HITs would "compute", and some promising preliminary results have been obtained, but a complete solution doesn't yet exist.

As for reasons to write such a compiler, it depends on what your interests are. If you're a mathematician wanting to formally verify proofs in homotopy type theory, then the benefits of such a proof assistant would be significant; current proof assistants require manual manipulation of many equalities that ought to be handled automatically if univalence and HITs "computed". The benefits of homotopy-theoretic features for programmers are not as obvious, but people have some ideas for how HITs could be used, e.g. here.

Edit: In general these compilers are not actually Turing-complete. They are used to check proofs, which means that all of their programs must terminate, and therefore (because of the undecidability of the halting problem) there must be some terminating programs that they can't compile. However, they generally have quite powerful termination-checkers that can handle most realistic programs.