I recently visited the PL group at Cornell to give a talk about our formal model and implementation of generics in Swift. While the talk was not recorded, the slides are available online: https://pl.cs.cornell.edu/pldg/slava-pestov.pdf.

The talk was meant for a mathematically-inclined audience unfamiliar with Swift, and the slides might be hard to parse without the narration, but perhaps some of you will find them interesting anyway. Let me know if you have questions!

Imagine you're implementing a Swift compiler. To type check the binarySearch() function here, you need a data type in the compiler to model type parameters, like C, E, C.Element, etc that can be written in the function's declaration and body:

func binarySearch<C: Collection, E>(_ c: C, _ e: E) where C.Element == E, E: Comparable { ... }

The type parameters C and E are called root type parameters. The names of root type parameters don't play any role in the language semantics, so to simplify the formal model to the bare minimum, we replace them with numbers. We assign 0 to C and 1 to E and represent each root type parameter by an integer. A member type parameter like C.Element has a base type C and a name Element; the most general form of a member type parameter is U.A where U is some other type parameter and A is a name.

So a data type to model type parameters looks exactly like this:

enum TypeParameter {
case root(Int)
indirect case member(base: TypeParameter, name: String)
}

Eg, C becomes .root(0), C.Slice.Element becomes .member(.member(.root(0), "Slice"), "Element"), etc.