Matt Oliveri and had a brief off list conversation about his thoughts
on extensible proof checkers, which this email moves back to list.
Much of this is paraphrasing or copying what he wrote, but all
mistakes are my own. This overlaps a bit with some discussion that
appeared on the reflection thread, but I think this is still worth a
separate conversation.
Basic question: How much power would bitc's type system need to allow
fancier heuristic type inference and type checking engineers to be
tacked on after the fact? Coq can already do this theoretically, but
there are many practical obstacles. Although I am on the fence as to
whether it's practical to get all the required functionality into bitc
v1, discussions of this sort may help us future proof bitc in simpler
ways (including grammar).
---------------------------------------------------------------------------
Coq consists of two different languages: a purely functional
dependently typed base language and semantics called Galina and an
imperative logic programming language called Ltac for describing
proofs. Core Galina (1) has simple decidable type checking and (2) is
strong enough to do all mathematics (at least constructive
mathematics). Because of (1), pure Galina is useless as a user
interface. In easy cases, this can be resolved with simple type
inference tricks. In complicated cases, Ltac is used to automatically
generate Galina code to prove whatever is required.
Since proofs in Coq are just pieces of Galina code that type check, a
trick called reflection can be used to generate proofs from Galina
code rather than Ltac:
http://adam.chlipala.net/cpdt/html/Reflection.html
Informally, reflection lets one write an object which has type
checker : Something -> forall (P : Prop). Maybe P
where Something is some kind of proof description (possibly empty), P
is a proposition we'd like to prove, and checker either returns a
proof of said proposition or fails (returns None). Once the core Coq
type checker has verified that "checker" has the promised type, we can
run checker and trust any proof that it produces.
The advantage of this setup is that only the core type checker (which
can be quite fairly simple for full dependent types) needs to be
standardized. Any logic which is either too complex to be practically
standardized (many kinds of heuristic type inference) or is viewed by
some as unsuitable for systems purposes (for example because it's
behavior is hard to predict) becomes a library which people can choose
to download or not as required. Indeed, it is strictly better than a
normal runtime library dependency since both itself and its output are
fully checked by the base type checker: the checker is not part of the
trusted core.
Unfortunately, there are several problems with using reflection in
practice (Matt's list):
1. The checker must be fast when run inside Coq's type checker. While
coq can emit compilable ocaml code, it is not itself a compiled
language. Performance intensive checkers will be very slow.
2. Any Galina code which type checks is strongly normalizing. If it
is most naturally written as a routine which loops forever, it must
use artificial methods such as loop bound limits to provably terminate
(though possibly with None).
3. Since it runs inside Coq's type checker, the normalization proof
cannot be made computational irrelevant, even with the Bove-Capretta
method (this bit is copied straight from Matt). If the normalization
proof is involved, the proof checker will be even slower.
4. The checker must be purely functional. Conceivably, one can
imagine proof checkers that do I/O, such as asking the user questions
or even pulling parts of proofs to be checked off the web (needless to
say: such features would have be optional).
How do these fair under imagined-bitc-with-full-dependent-types?
1. Bitc should be a lot faster than Coq. All good here.
2. Especially if bitc ends up with something like effect types, I
think it might not be too hard to solve this problem. Nontermination
can become an effect just like anything else, as long as the interface
between effect typing and dependent typing is fancy enough to remove a
nontermination effect "after the fact". This is only a hope, but
might be a good question for the ATS folk.
3. Matt will have to answer this one, since he has better knowledge
than I. Does a strong phase distinction between runtime and compile
time help here?
4. Impure type checkers are perfectly fine as long as all the effects
are deemed okay by the user. This would require compiler flags, since
the default would want to be no effects allowed at compile time.
I think the main research question here is (2): How complex does the
base logic get if you require nontermination to be provable after the
fact? I think this question is important enough to try understand now
even if we don't plan to do any of the above in bitc 1v, since it
might tell us a lot about how difficult it would be to extend bitc
towards full dependent types in future.
Geoffrey
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
