Open Access Te Herenga Waka-Victoria University of Wellington
Browse

Decidable Subtyping for Path Dependent Types

Download (727.32 kB)
Version 2 2023-09-22, 01:44
Version 1 2021-12-08, 21:36
thesis
posted on 2023-09-22, 01:44 authored by Julian Mackay

Path dependent types form a central component of the Scala programming language. Coupled with other expressive type forms, path dependent types provide for a diverse set of concepts and patterns, from nominality to F-bounded polymorphism. Recent years have seen much work aimed at formalising the foundations of path dependent types, most notably a hard won proof of type safety. Unfortunately subtyping remains undecidable, presenting problems for programmers who rely on the results of their tools. One such tool is Dotty, the basis for the upcoming Scala 3. Another is Wyvern, a new programming language that leverages path dependent types to support both first class modules and parametric polymorphism. In this thesis I investigate the issues with deciding subtyping in Wyvern. I define three decidable variants that retain several key instances of expressiveness including the ability to encode nominality and parametric polymorphism. Wyvfix fixes types to the contexts they are defined in, thereby eliminating expansive environments. Wyvnon-μ removes recursive subtyping, thus removing the key source of expansive environments during subtyping. Wyvμ places a syntactic restriction on the usage of recursive types. I discuss the formal properties of these variants, and the implications each has for expressing the common programming patterns of path dependent types. I have also mechanized the proofs of decidability for both Wyvfix and Wyvμ in Coq.

History

Copyright Date

2020-01-01

Date of Award

2020-01-01

Publisher

Te Herenga Waka—Victoria University of Wellington

Rights License

CC BY 4.0

Degree Discipline

Computer Science

Degree Grantor

Te Herenga Waka—Victoria University of Wellington

Degree Level

Doctoral

Degree Name

Doctor of Philosophy

ANZSRC Type Of Activity code

1 PURE BASIC RESEARCH

Victoria University of Wellington Item Type

Awarded Doctoral Thesis

Language

en_NZ

Victoria University of Wellington School

School of Engineering and Computer Science

Advisors

Potanin, Alex; Groves, Lindsay; Aldrich, Jonathan