file:scala/dotty/en/dependent-types.org
source link: https://blog.oyanglul.us/scala/dotty/en/dependent-types.html
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
-
10
Dependent Types in Scala 3 Table of Contents 中文 | English I'm...
-
9
Do you know about Intersection Types in Scala 3.0, Dotty? Reading Time: 2 minutes You might have learnt intersection of su...
-
16
Functional Scala Caching Table of Contents 雎鳩ju jiu Functional Scala Caching
-
7
Scala 3 从属类型 Scala 3 从属类型 Table of Contents 中文
-
11
Type Classes in Scala 3 Type Classes in Scala 3 Table of Contents I'm recently migrating some libs and projects to Scala 3, I gues...
-
5
First Class Types In Idris, types are first class, meaning that they can be computed and manipulated (and passed to functions) just like any other language construct.
-
2
Generic Type Class Derivation in Scala 3 Generic Type Class Derivation in Scala 3 Table of Contents I'm recently migrating some li...
-
13
Get Started with Http4s follow the structure of Getting Started with Rails This guide covers getting up and...
-
10
Scala 3 Kan Extensions Scala 3 Kan Extensions Table of Contents 可以跑的源码在这里 👉
-
7
Then follow the Stereo type So the common here they are both very simple to use, without understanding how it works even what it means, just follow the same pattern you could get the build worki...
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK