Dependent Types in Scala 3
source link: https://blog.oyanglul.us/scala/dotty/en/dependent-types
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Dependent Types in Scala 3
Table of Contents
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
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK