-
Notifications
You must be signed in to change notification settings - Fork 235
_type_checker_brainstorming
TODO (tl): review approaches by
- Matthieu Sozeau (Coq - new unification algorithm - including type classes),
- Claudio Sacerdoti Coen (ELPI's implementation of part of Matita),
- Francesco Mazzoli and Andreas Abel about type checking as a unification problem,
- Nanevski's contextual modal type theory (different syntax for dependent types and its type inference),
- etc.
The POPL2017 paper DM4F proves correctness of the core calculus EMF* (Explicitly Monadic F* ) by embedding it into Coq. The main lacking point of this formalization wrt the actual F* implementation seems to be fixpoints and recursion (KM : at least that's my understanding of the situation as 01/2017). The elaboration and type inference from actual F* to EMF* seem to have been treated in the POPL2016 paper Multi-monadic effects. Building up on recent papers on Coq plugin system and syntactic models, it might be possible to have an elaboration of "full" F* to Coq using something like the topos of tree to account for recursion (KM : the main problems that I foresee is the difference about universes : Coq has a predicative Prop universe and cumulativity whereas F* has only predicative universes - and prop is not (syntactically at least) a universe - without cumulativity ). In particular the parametric syntactic model of then weaning translation has quite some similarity with the elaborations of DM4F.
TODO (tl): understand the differences between the type systems
TODO (tl): define several approaches for the problem, do we want:
-
- a specification on paper
-
- reference implementation (i.e. lambda-prolog/elpi)
-
- specify the code by extensively testing it
-
- refactor existing code only
-
- Elaboration to a more mainstream typechecker (Coq, Agda, ...)
Discussion with Aseem (14/2/2017)
- The Lax mode of the compiler does type inference but does not compute WPs and does not propagate obligations to SMT. Q: I understood form Nik that subtyping is also checked using SMT. Is it planned to test it in the second phase?
- Aseem has implemented the separation, see commit: https://github.com/FStarLang/FStar/commit/10bc5c4f8f31d2ebc5792d51984a28875ad043ef#diff-c8e927bd0241868682ede8eb0bc1afd2 Some problems are:
- Universe instantiation problem: Aseem thinks it is because of State effects. Universes should not play a role in second phase.
- Qualifiers for let binders are computed in first phase and should be used for second phase. Aseem plans on storing errors and load them for second phase.
- Some encoding of obligations to SMT done twice when separating phases right now. Only Prims should be encoded in first phase right now.
- Lax originated as a compiler for FStar since there are no proofs right now. Name originated from Relax?
- It is a proof of concept right now
- Once Aseem's approach works on tests, we can try to optimize each phase and simplify the code
- Files in focus:
-
rel.fs- a change with regard to honoring universe_lax -
tc.fs- main separation, see commit above
- Full typechecking example
- Typechecking internals about the actual implementation
- Typechecking theory about the TC algorithm