Scala 3 通用代数类型 (GADT)

可以跑的源码在这里 👉 https://github.com/jcouyang/meow

我们都知道 ADTAlgebraic Datatypes 指的是 Coproduct 类型, 也就是由多个构造函数返回一种类型, 比如:

enum List[+A]{
  case Nil
  case Cons(head: A, tail: List[A])
}

这是普通的 ADT, 也就是 Nil 和 Cons 构造出来的类型是固定的.

但是如果对类型有一些特别的需求, 这种 ADT 就难以满足, 幸运的是 Scala 3 的 enum 本身就是 GADT. https://dotty.epfl.ch/docs/reference/enums/adts.html

然我们来定义一个类型更安全的 List, 叫 SafeList

1: enum Size {
2:   case Empty
3:   case NonEmpty
4: }
5: 
6: enum SafeList[+A, +S <: Size] {
7:   case Nil extends SafeList[Nothing, Size.Empty.type] // <-
8:   case Cons(head: A, tail: SafeList[A, Size]) extends SafeList[A, Size.NonEmpty.type]
9: }

你看这行就不是默认的返回类型 List[Nothing] , 我们可以定制这个类型为 SafeList[Nothing, Size.Empty,type], 来在类型上表示该 list 为空.

同样的我们把 Cons 的返回类型写死成 SafeList[A, Size.NonEmpty.type] 表示它不空.

import SafeList._

def safeHead[A](list: SafeList[A, Size.NonEmpty.type]): A = list match
  case SafeList.Cons(head, tail) => head

从类型上看 SafeList[A, Size.NonEmpty.type] 只接受 Size.NonEmpty 的 list.

所以如果你传个 Nil 进去, 编译器就不乐意了.

safeHead(Nil)

Found:    (Main.SafeList.Nil : Main.SafeList[Nothing, (Main.Size.Empty : Main.Size)])
Required: Main.SafeList[Any, (Main.Size.NonEmpty : Main.Size)]

不信? 自己试试吧 https://scastie.scala-lang.org/jcouyang/yGQTSUJ6SN2P2oUsfWu9zw/1

Scala 3 通用代数类型 (GADT)

Recommend

Rank N Types in Scala 3

Scala 3 N 阶类型

Scala 3 幻影类型

Dependent Types in Scala 3

Scala 3 从属类型

Scala 3 Kan Extensions

FunctionK in Scala 3

Phantom Types in Scala 3

Dummy Guide to sbt

"First Class" Types in Scala 3

About Joyk