A quick explanation of Path Dependent Types

Scala has had the concept of Path Dependent Types for a long time, and in Scala 3 this concept has been used to formalize the type system (see: DOT Calculus). However, you have probably wondered for a long time what practical benefits Path Dependent Types bring over generics if you're like me.

Well, path dependent types are very helpful for working with types who are only truly knowable at runtime.

C, time_t, and Path Dependent Types

I've been writing code to have Scala and C interoperate recently, and doing so has introduced me to some unique challenges. One of them was defining the type time_t so that users can use it in C bindings if need-be.

time_t is a part of the c standard library, but its implementation is left to the library implementing the library. On an i386 Linux (i386 is a 32-bit Intel arch) machine, time_t is equivalent to a JVM Long, while on i386 MidnightBSD it's equivalent to a JVM Int. Since my library bases its C bindings on types, this means that I have a serious problem:

• if I define time_t as type time_t=Int my library is only useable on MidnightBSD machines
• if I define time_t as type time_t=Long my library is only useable on Linux machines
• if I define time64_t and time_t then my library works on both, but user code becomes locked down to one OS, and they have to worry about what OS to develop for.

If only types could be defined at runtime... if I could write

type time_t = if os == Linux then Long 
else if os == MidnightBSD then Int 
else Nothing

Then I'd have no problems!! If only there was a way to write types that are defined depending on the path the program takes at runtime...

Oh! Path Dependent Types!!

Making things work

With a couple of traits I can make things work for my users. First I need a prototype for time_t:

trait time_t_proto:
  type time_t
  val time_t_integral: Integral[time_t]
  implicit class time_t_ops(time_t: time_t) 
    extends time_t_integral.IntegralOps(time_t)
  implicit class time_t_ord(time_t: time_t) 
    extends time_t_integral.OrderingOps(time_t)

This version of time_t is what Scala will use at compile time, and in it we promise that time_t will have an Integral typeclass defined no matter the runtime value. Then we tell the compiler how to extend time_t with functionality like a + operator or < operator via the time_t_ops and time_t_ord implicit classes. This lets users do basic ordering and arithmetic on these types as if they were Int or Long despite their type being unknown at compile-time.

Now we need the "implementation":

trait time_t_impl[U](using val time_t_integral: Integral[U]) 
  extends time_t_proto:
  type time_t = U

This doesn't look like much of an implementation, but it's written this way so it can be mixed into a large, arch specific Platform type.

trait Platform extends time_t_proto

object PlatformMidnightBSD extends Platform, time_t_impl[Int]
object PlatformLinux extends Platform, time_t_impl[Long]

val platform: Platform = if os == MidnightBSD then PlatformMidnightBSD
else if os == Linux then PlatformLinux
else ???

Finally we have our end result. The design used for the time_t_proto and impl allows for multiple of these proto types and impl types for other platform specific C types (dev_t for example). It also allows us to quickly and easily define a set of bindings for the myriad computing platforms. Finally, the appropriate Platform implementation is selected at runtime and assigned to the platform value, giving users a way to use platform specific types without writing in a platform specific way.

The end result is that users can define their bindings like so:

import platform.time_t
def time(timer: Ptr[time_t]): time_t = bind

and this binding will work regardless of the computer it's accessed on, because the appropriate, path dependent type info will be loaded and used at runtime, while giving the compiler enough information and assurances at compile time to keep things completely type-safe.

Of course, the users in question can still write platform specific code if they wish.

import PlatformLinux.time_t
def time(timer: Ptr[time_t]): time_t = bind

The above code works just fine, and time_t in the above code is understood to be Long at compile-time instead of being an unknown type. However, this code would no-longer work everywhere, and that's a big draw of writing for the JVM.

Could this be done with generics?

In short, no. We could not achieve the same effect with the same amount of work using generics. We could try to do the above with generics, but generics would fail us. Lets say we modified the proto traits and the Platform trait to take a generic instead of the embedded type time_t:

trait time_t_proto[time_t]:
  val time_t_integral: Integral[time_t]
  implicit class time_t_ops(time_t: time_t) 
    extends time_t_integral.IntegralOps(time_t)
  implicit class time_t_ord(time_t: time_t) 
    extends time_t_integral.OrderingOps(time_t)

trait time_t_impl[U](using val time_t_integral: Integral[U]) 
  extends time_t_proto[U]

trait Platform[A] extends time_t_proto[A]

object PlatformMidnightBSD extends Platform[Int], time_t_impl[Int]
object PlatformLinux extends Platform[Long], time_t_impl[Long]

val platform: Platform[?] = if os == MidnightBSD then PlatformMidnightBSD 
else if os == Linux then PlatformLinux
else ???

The above code will very certainly compile, but how will the user get their time_t type? The ? type here corresponds to the correct type, but it's unusable for our users. Worse, our code has become more complex, and to get Platform to truly work the way we want, we'd probably have to do a lot of work to turn it into a god object that manages all parts of binding to C.

In summary

Path dependent types are a very powerful feature of Scala, but they are generally not well understood in the community. I believe that the problem of platform specific types (like C's time_t) easily illustrates the need for path dependent types, and how they can outshine generics in some situations.