HOME | EDIT | RSS | INDEX | ABOUT | GITHUB

Scala 3 通用代数类型 (GADT)

中文 | English

可以跑的源码在这里 👉 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: enum SafeList[+A, +S <: Size]:
6:   case Nil extends SafeList[Nothing, Size.Empty.type] // <-
7:   case Cons(head: A, tail: SafeList[A, Size]) extends SafeList[A, Size.NonEmpty.type]

你看 这行 就不是默认的返回类型 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

Footnotes:

1

https://dotty.epfl.ch/docs/reference/enums/adts.html