Rethinking Dependent Type Checking, Co-Contextually
G.J.T. Bot (TU Delft - Electrical Engineering, Mathematics and Computer Science)
J.G.H. Cockx – Graduation committee member (TU Delft - Programming Languages)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Dependent type systems allow types to depend on values, enabling the encoding of rich semantic properties directly in types. Currently, dependently typed systems are not widely used for general-purpose programming, but they are commonly used in proof assistants. Agda, Idris, Lean, and Rocq all support dependent types.
The expressiveness of the type system comes with a cost: type checking is expensive. This thesis explores co-contextual type checking as an alternative foundation for dependent type systems. Co-contextual type checking inverts the ‘traditional’ flow of information, enabling type checking to proceed without immediate access to a complete typing environment.
This work explores a co-contextual formulation of a dependent type system and its accompanying type-checking algorithm. Both incremental and parallel variants of the algorithm are implemented for the dependently typed lambda calculus Elara, based on LambdaPi (Löh, McBride, and Swierstra, 2010). The research primarily focuses on the feasibility of such a type checker.
Apart from providing the first co-contextual implementation of a dependent type system, its performance is compared to LambdaPi’s contextual bidirectional type-checking algorithm for reference. In the end, it is found that the implemented co-contextual type checker generally performs worse than the contextual reference implementation. Its performance is of the same order of magnitude, with plenty of opportunity for improvement discussed in this work. In particular, co-contextual incremental type checking has significant potential through the reuse of evaluation, which is not fully leveraged in the conservative approach taken in this work.