13

Phantom Types in Scala 3

 3 years ago
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

Phantom 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


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


About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK