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
astype time_t=Int
my library is only useable on MidnightBSD machines - if I define
time_t
astype time_t=Long
my library is only useable on Linux machines - if I define
time64_t
andtime_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 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:
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 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
:
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.
Top comments (0)