Phantom Types in Scala 3
source link: https://blog.oyanglul.us/scala/dotty/en/phantomtype
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.
Phantom Types in Scala 3
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
Phantom Types are types on the left-hand side, but not on the right-hand side, which means the types that you don't actually need, to construct a data.
We actually met phantom type already in the SafeList
example in GADT.
Here is a better one, we can put more info other than just Empty
, NonEmpty
in the type.
We can have length info in type as well, then we got a type safe Vector
:
enum Nat { case Zero case Succ[A]() } import Nat._ type Nat2 = Succ[Succ[Zero.type]] type Nat3 = Succ[Succ[Succ[Zero.type]]] enum Vector[+N <: Nat, +A] { case Cons(head: A, tail: Vector[N, A]) extends Vector[Succ[N], A] case Nil extends Vector[Zero.type, Nothing] } import Vector._ val vector2: Vector[Nat2, Int] = Cons(1, Cons(2, Nil)) val vector3: Vector[Nat3, Int] = Cons(1, Cons(2, Cons(3, Nil)))
See the type Nat2
does only appear on the left hand side. Cons
don't need anything
about Nat
to create a Vector
.
We know that for Scala List
, if we call head
, it could cause run time error when
the list is empty.
When we have the length info tagged into the Vector[N, A]
, we can actually create
a type level safe head
, let us call it typeSafeHead
:
def typeSafeHead[A](vec: Vector[Succ[Nat], A]):A = vec match case Cons(head, _) => head
When you have some code that trying to get head
from Nil
, the compiler will tell you:
typeSafeHead(Nil)
Found: (Main.Vector.Nil : Main.Vector[(Main.Nat.Zero : Main.Nat), Nothing]) Required: Main.Vector[Main.Nat.Succ[Main.Nat], Any]
Similarly, you can easily create safe second
as well, by counting how many Succ
there are in Nat
at type level.
Try it online at Scastie: https://scastie.scala-lang.org/jcouyang/JTX3OFXrTCOuq6LNfgRj8Q/8
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