Open Access Te Herenga Waka-Victoria University of Wellington
thesis_access.pdf (727.32 kB)

Decidable Subtyping for Path Dependent Types

Download (727.32 kB)
Version 2 2023-09-22, 01:44
Version 1 2021-12-08, 21:36
posted on 2023-09-22, 01:44 authored by Julian MackayJulian 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.


Copyright Date


Date of Award



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


Degree Name

Doctor of Philosophy

ANZSRC Type Of Activity code


Victoria University of Wellington Item Type

Awarded Doctoral Thesis



Victoria University of Wellington School

School of Engineering and Computer Science


Potanin, Alex; Groves, Lindsay; Aldrich, Jonathan