Scala中的类型级编程

spa*_*rkr 6 scala type-level-computation

我想深入了解Scala中的类型级编程,并开始做一些小练习.我开始在类型级别实现Peano数字.这是下面的代码!

sealed trait PeanoNumType { // Type at the end indicates to the reader that we are dealing with types
  type plus[That <: PeanoNumType] <: PeanoNumType
}

sealed trait ZeroType extends PeanoNumType {
  type plus[That <: PeanoNumType] = That
}

sealed trait NextType[This <: PeanoNumType] extends PeanoNumType {
   type plus[That <: PeanoNumType] = NextType[This#plus[That]]
}
Run Code Online (Sandbox Code Playgroud)

现在问题是,上述实施会给我带来什么?我该如何使用它?

Mat*_*zok 11

只要你自己需要创建这些类型,它就不会给你太多.但是,只要你让编译器为你做这些东西,它就会更有用.

在我展示之前,让我们改变一种将Peano aritmetic代表更短的方式:

sealed trait Num
case object Zero extends Num
case class Succ[N <: Num](num: N) extends Num
Run Code Online (Sandbox Code Playgroud)

然后,您可以在编译时创建一个已知大小的列表:

sealed abstract class List[+H, N <: Num](val size: N) {
  def ::[T >: H](value: T): List[T, Succ[N]] = Cons(value, this)
}
case object Nil extends List[Nothing, Zero.type](Zero)
case class Cons[+H, N <: Num](head: H, tail: List[H, N]) extends List[H, Succ[N]](Succ(tail.size))
type ::[+H, N <: Num] = Cons[H, N]
Run Code Online (Sandbox Code Playgroud)

如果检查用sych列表创建的sth类型,它的大小将按其类型编码:

val list = 1 :: 2 :: 3 :: 4 :: Nil // List[Int, Succ[Succ[Succ[Succ[Zero.type]]]]] = Cons(1,Cons(2,Cons(3,Cons(4,Nil))))
Run Code Online (Sandbox Code Playgroud)

你可以尝试做的下一件事就是使用implicits来检查一些东西,例如

trait EvenNum[N <: Num]
implicit val zeroIsEven = new EvenNum[Zero.type] {}
implicit def evenNPlusTwo[N <: Num](implicit evenN: EvenNum[N]) = new EvenNum[Succ[Succ[N]]] {}
Run Code Online (Sandbox Code Playgroud)

有了这个,您可以强制执行某些操作只能在提供隐式证据时才能完成:

def operationForEvenSizeList[T, N <: Num](list: List[T, N])(implicit ev: EvenNum[N]) = {
  // do something with list of even length
}

operationForEvenSizeList(1 :: 2 :: Nil) // ok
operationForEvenSizeList(1 :: 2 :: 3 :: Nil) // compiler error
Run Code Online (Sandbox Code Playgroud)

当你开始使用implicits来创建新类型时,我可以看出Scala中类型级编程的真正力量:可以用于隐式证据,类型类派生和删除某些结构样板的那些类型.

一个帮助很多通用编程的库是Shapeless.我相信,与你一起工作将是一件有趣的事情,一旦你做一两个带有隐含的类型派生的练习.

回到你的代码:你可以提供一些暗示,为你生成和提供你的类的实例.此外,除了创建新类之外,此代码还可以执行其他操作,例如组合您将在这些类中添加的元素列表,或提供从PeanoNumType到Int的转换,或添加一些在编译时工作的谓词等.天空是限制.