An insider's look at LF type reconstruction: everything you (n)ever wanted to know
Abstract Although type reconstruction for dependently typed languages is common in practical systems, it is still ill-understood. Detailed descriptions of the issues around it are hard to find and formal descriptions together with correctness proofs are non-existing. In this paper, we discuss a one-...
| Published in: | Journal of Functional Programming |
|---|---|
| Main Author: | |
| Format: | Article in Journal/Newspaper |
| Language: | English |
| Published: |
Cambridge University Press (CUP)
2012
|
| Subjects: | |
| Online Access: | http://dx.doi.org/10.1017/s0956796812000408 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0956796812000408 |
| Summary: | Abstract Although type reconstruction for dependently typed languages is common in practical systems, it is still ill-understood. Detailed descriptions of the issues around it are hard to find and formal descriptions together with correctness proofs are non-existing. In this paper, we discuss a one-pass type reconstruction for objects in the logical framework LF, describe formally the type reconstruction process using the framework of contextual modal types, and prove correctness of type reconstruction. Since type reconstruction will find most general types and may leave free variables, we in addition describe abstraction which will return a closed object where all free variables are bound at the outside. We also implemented our algorithms as part of the Beluga language, and the performance of our type reconstruction algorithm is comparable to type reconstruction in existing systems such as the logical framework Twelf. |
|---|