Dependent Types in Scala 3

中文 | English

I'm recently migrating some libs and projects to Scala 3, I guess it would be very helpful to me or anyone interested to learn some new functional programming features that Scala 3 is bringing to us.

Source code 👉 https://github.com/jcouyang/meow

You probably already noticed what dependent type looks like in Vector example for Phantom Types, where the actual type of Vector depends on the actual value. We can call it dependent type because the type of Vector actually depends on the vector length, e.g. a value of list has length 2 will result in type Vector[Nat2, Int], where Nat2 is actually calculated based on value of length.

Scala 2

There is a very common pattern in Shapeless, Aux pattern basically a pattern to derive output type :

trait Second[L <: HList] {
  type Out
  def apply(value: L): Out
}

object Second {
  type Aux[L <: HList, O] = Second[L] { type Out = O }

  def apply[L <: HList, R](l: L)(implicit inst: Aux[L, R]): R =
    inst(l)
}

Second(1 :: "2" :: HNil)

will output:

"2"

Here Second.apply is actually dependent type, since you can basically tell the output type from Aux[L, R] is R, if input is L.

e.g. when the input is another HList:

Second("1" :: 2 :: HNil)
// => 2

Output type will become Int.

Actually with dependent method, this could be simplified as:

object Second {
  def apply[L <: HList, R](l: L)(implicit inst: Second[L]): inst.Out =
    inst(l)
}

Scala 3

In Scala 3 it is even better, not only dependent method, we can define dependent function https://dotty.epfl.ch/docs/reference/new-types/dependent-function-types.html now.

With dependent function, it looks like:

1: object Second {
2:   def apply[L <: HList](value: L) = (inst: Second[L]) ?=> inst(value) // <--
3: }

?=> in line 2 https://dotty.epfl.ch/docs/reference/contextual/context-bounds.html is not a typo, it is simplified version of (using inst: Second[L]) => inst(value)

If we add the type for the function it will be like:

def apply[L <: HList](value: L): (inst: Second[L]) ?=> inst.Out =
 (inst: Second[L]) ?=> inst(value)

Aux is somehow still very useful

Ok, there is another problem though, so why do we need Aux pattern anymore if dependent method can solve the problem already?

If we need to implement a 2 dimensional Second, which means it will take the second element's second element.

object Second2D {
  import Second.Aux
  def apply[L <: HList, R <: HList, R2](l: L)(implicit inst1D: Aux[L, R], inst2D: Aux[R, R2]): R2 =
    inst2D(inst1D(l))
}

The inst1D depends on the input type L, inst2D now depends on the inst1D return type R, so the whole method return type R2 depends on R.

See what happen if we try to transform this to dependent method:

object Second2D {
  def apply[L <: HList](l: L)(implicit inst1D: Second[L], inst2D: Second[inst1D.Out]): inst2D.Out =
    inst2D(inst1D(l))
}

You got a compile error:

Type argument inst1D.Out does not conform to upper bound shapeless.HList

Since it is a dependent type, we don't have any chance to tell compiler that inst1D.Out must be a HList.

Try it online at Scastie: https://scastie.scala-lang.org/fyxXSR3ASj6rSkkERnUK7g

Or clone the repo and sbt test: https://github.com/jcouyang/meow

Footnotes:

basically a pattern to derive output type

https://dotty.epfl.ch/docs/reference/new-types/dependent-function-types.html

https://dotty.epfl.ch/docs/reference/contextual/context-bounds.html