Labelled preorders and implicit coercions › A clean-room implementation of Sakaguchi’s labelled preorders [01HK]

In order to learn how the algorithm works, I built a clean-room generic implementation in Swift of the labelled preorder structure following Sakaguchi’s algorithm. (Oh, did I mention I’m using Swift?)

Our case will be a bit simpler than that of Rocq. In Rocq, coercions can be between arbitrary things, and therefore the vertices must include definitional equivalence classes of terms. That seems very tricky! We will be using a more restricted kind of coercion in Pterodactyl, where the vertices are only theory names. (We might later on also support coercions to sorts like those of types and functions, like Rocq does, which would not be difficult.)

As a result, the only thing that we need to use expensive definitional equality checks for is the coercion paths themselves. It will indeed be pretty costly to install coercions, but resolving them will be very cheap: it is a single lookup in a hashtable by a totally discrete key. My code is available here.

I am not certain that we will use literally this code (abstracting and modularising too early can be hazardous), but it’s a good start.