A quick explanation of Path Dependent Types
Tags: programming, scala, tutorial, c
Published: 2022-01-17 13:26:41

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](http://lampwww.epfl.ch/~amin/dot/scaladays-slides.pdf)). 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 
```scala
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`:
```scala
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":
```scala
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.
```scala
trait Platform extends time_t_proto

object PlatformI386 extends Platform, time_t_impl[Int]
object PlatformX64 extends Platform, time_t_impl[Long]

val platform: Platform = if arch == i386 then PlatformI386 
else if arch == x86_64 then PlatformX64
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: 
```scala
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.
```scala
import PlatformX64.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`:

```scala
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 PlatformI386 extends Platform[Int], time_t_impl[Int]
object PlatformX64 extends Platform[Long], time_t_impl[Long]

val platform: Platform[?] = if arch == i386 then PlatformI386 
else if arch == x86_64 then PlatformX64
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.