Scala 类型编程资源 [英] Scala type programming resources

问题描述

根据这个问题，Scala 的类型系统是图灵完备.有哪些资源可以让新手利用类型级编程的力量?

According to this question, Scala's type system is Turing complete. What resources are available that enable a newcomer to take advantage of the power of type-level programming?

以下是我目前找到的资源:

Here are the resources I've found so far:

• Daniel Spiewak 的斯卡拉王国的高级魔法
• Apocalisp 的类型级编程斯卡拉
• Jesper 的 HList

这些资源很棒，但我觉得我缺少基础知识，因此没有坚实的基础来构建.例如，哪里有类型定义的介绍?我可以对类型执行哪些操作?

These resources are great, but I feel like I'm missing the basics, and so do not have a solid foundation on which to build. For instance, where is there an introduction to type definitions? What operations can I perform on types?

有什么好的介绍资源吗?

Are there any good introductory resources?

推荐答案

概览

类型级编程与传统的值级编程有很多相似之处.然而，与计算发生在运行时的值级编程不同，在类型级编程中，计算发生在编译时.我将尝试在值级编程和类型级编程之间进行比较.

Type-level programming has many similarities with traditional, value-level programming. However, unlike value-level programming, where the computation occurs at runtime, in type-level programming, the computation occurs at compile time. I will try to draw parallels between programming at the value-level and programming at the type-level.

范式

类型级编程有两种主要范式:面向对象"和函数式".此处链接的大多数示例都遵循面向对象的范例.

There are two main paradigms in type-level programming: "object-oriented" and "functional". Most examples linked to from here follow the object-oriented paradigm.

在 apocalisp 的 lambda 演算的实现，复制在这里:

A good, fairly simple example of type-level programming in the object-oriented paradigm can be found in apocalisp's implementation of the lambda calculus, replicated here:

// Abstract trait
trait Lambda {
  type subst[U <: Lambda] <: Lambda
  type apply[U <: Lambda] <: Lambda
  type eval <: Lambda
}

// Implementations
trait App[S <: Lambda, T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = App[S#subst[U], T#subst[U]]
  type apply[U] = Nothing
  type eval = S#eval#apply[T]
}

trait Lam[T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = Lam[T]
  type apply[U <: Lambda] = T#subst[U]#eval
  type eval = Lam[T]
}

trait X extends Lambda {
  type subst[U <: Lambda] = U
  type apply[U] = Lambda
  type eval = X
}

从示例中可以看出，类型级编程的面向对象范式如下:

As can be seen in the example, the object-oriented paradigm for type-level programming proceeds as follows:

• 首先:定义具有各种抽象类型字段的抽象特征(有关抽象字段的含义，请参见下文).这是一个模板，用于保证某些类型字段存在于所有实现中，而不强制实现.在 lambda 演算示例中，这对应于保证以下类型存在的 trait Lambda:subst、apply 和 eval.
• 下一步:定义扩展抽象特征并实现各种抽象类型字段的子特征
  • 通常，这些子特征将使用参数进行参数化.在 lambda 演算示例中，子类型是 trait App extends Lambda，它被参数化为两种类型(S 和 T，两者都必须是Lambda)、trait Lam extends Lambda 参数化为一种类型(T)，以及 trait X extends Lambda(未参数化).
  • 类型字段通常通过引用子特征的类型参数来实现，有时通过哈希运算符引用它们的类型字段:#(与点运算符非常相似:. 用于值).在 lambda 演算示例的特征 App 中，类型 eval 实现如下:type eval = S#eval#apply[T].这实质上是调用特征参数 S 的 eval 类型，并在结果上调用带有参数 T 的 apply.请注意，S 保证具有 eval 类型，因为参数指定它是 Lambda 的子类型.类似地，eval 的结果必须具有 apply 类型，因为它被指定为 Lambda 的子类型，如抽象特征中所指定Lambda.
  • First: define an abstract trait with various abstract type fields (see below for what an abstract field is). This is a template for guaranteeing that certain types fields exist in all implementations without forcing an implementation. In the lambda calculus example, this corresponds to trait Lambda that guarantees that the following types exist: subst, apply, and eval.
  • Next: define subtraits that extend the abstract trait and implement the various abstract type fields
    • Often, these subtraits will be parameterized with arguments. In the lambda calculus example, the subtypes are trait App extends Lambda which is parameterized with two types (S and T, both must be subtypes of Lambda), trait Lam extends Lambda parameterized with one type (T), and trait X extends Lambda (which is not parameterized).
    • the type fields are often implemented by referring to the type parameters of the subtrait and sometimes referencing their type fields via the hash operator: # (which is very similar to the dot operator: . for values). In trait App of the lambda calculus example, the type eval is implemented as follows: type eval = S#eval#apply[T]. This is essentially calling the eval type of the trait's parameter S, and calling apply with parameter T on the result. Note, S is guaranteed to have an eval type because the parameter specifies it to be a subtype of Lambda. Similarly, the result of eval must have an apply type, since it is specified to be a subtype of Lambda, as specified in the abstract trait Lambda.

    Functional 范式包括定义大量参数化的类型构造函数，这些构造函数没有在 trait 中组合在一起.

    The Functional paradigm consists of defining lots of parameterized type constructors that are not grouped together in traits.

    值级编程和类型级编程的比较

    • 抽象类
      • 值级:abstract class C { val x }
      • 类型级别:trait C { type X }
      • C.x(引用对象 C 中的字段值/函数 x)
      • C#x(引用 trait C 中的字段类型 x)
      • C.x (referencing field value/function x in object C)
      • C#x (referencing field type x in trait C)
      • 值级别:def f(x:X) : Y
      • type-level: type f[x <: X] <: Y(这被称为类型构造函数"，通常出现在抽象特征中)
      • value-level: def f(x:X) : Y
      • type-level: type f[x <: X] <: Y (this is called a "type constructor" and usually occurs in the abstract trait)
      • 值级别:def f(x:X) : Y = x
      • 类型级别:type f[x <: X] = x
      • 见这里
      • 值级:a:A == b:B
      • 类型级别:隐式[A =:= B]
      • 值级别:通过运行时的单元测试在 JVM 中发生(即没有运行时错误):
        • 本质上是一个断言:assert(a == b)
        • 本质上是一种类型比较:例如隐式[A =:= B]
        • A <:，仅当 A 是 B
        的子类型时才编译
        • A =:= B，仅当 A 是 B 的子类型并且 B 是一个A
        的子类型
        • A <%<;B, ("viewable as") 仅在 A 可被视为 B 时才编译(即存在从 A 的隐式转换到 B) 的子类型
        • 示例
        • 更多比较运算符
        • in essence is a type comparison: e.g. implicitly[A =:= B]
        • A <:< B, compiles only if A is a subtype of B
        • A =:= B, compiles only if A is a subtype of B and B is a subtype of A
        • A <%< B, ("viewable as") compiles only if A is viewable as B (i.e. there is an implicit conversion from A to a subtype of B)
        • an example
        • more comparison operators

        类型和值之间的转换

        • 在许多示例中，通过特征定义的类型通常既是抽象的又是密封的，因此既不能直接实例化，也不能通过匿名子类实例化.因此，在使用某种兴趣类型进行值级计算时，通常使用 null 作为占位符值:

        • 例如val x:A = null，其中A是你关心的类型
        • e.g. val x:A = null, where A is the type you care about

        由于类型擦除，参数化类型看起来都一样.此外，(如上所述)您使用的值往往都是 null，因此对对象类型的调节(例如通过 match 语句)是无效的.

        Due to type-erasure, parameterized types all look the same. Furthermore, (as mentioned above) the values you're working with tend to all be null, and so conditioning on the object type (e.g. via a match statement) is ineffective.

        诀窍是使用隐式函数和值.基本情况通常是隐式值，递归情况通常是隐式函数.事实上，类型级编程大量使用了隐式.

        The trick is to use implicit functions and values. The base case is usually an implicit value and the recursive case is usually an implicit function. Indeed, type-level programming makes heavy use of implicits.

        考虑这个例子(取自 metascala 和 apocalisp):

        Consider this example (taken from metascala and apocalisp):

        sealed trait Nat
        sealed trait _0 extends Nat
        sealed trait Succ[N <: Nat] extends Nat
        

        这里有一个自然数的皮亚诺编码.也就是说，每个非负整数都有一个类型:0 的特殊类型，即 _0；并且每个大于零的整数都具有 Succ[A] 形式的类型，其中 A 是表示较小整数的类型.例如，表示 2 的类型将是:Succ[Succ[_0]](后继应用于表示零的类型两次).

        Here you have a peano encoding of the natural numbers. That is, you have a type for each non-negative integer: a special type for 0, namely _0; and each integer greater than zero has a type of the form Succ[A], where A is the type representing a smaller integer. For instance, the type representing 2 would be: Succ[Succ[_0]] (successor applied twice to the type representing zero).

        我们可以给各种自然数取别名，方便参考.示例:

        We can alias various natural numbers for more convenient reference. Example:

        type _3 = Succ[Succ[Succ[_0]]]
        

        (这很像定义一个 val 作为函数的结果.)

        (This is a lot like defining a val to be the result of a function.)

        现在，假设我们要定义一个值级函数 def toInt[T <: Nat](v : T) 它接受一个参数值，v，符合 Nat 并返回一个整数，表示以 v 类型编码的自然数.例如，如果我们有值 val x:_3 = null (null 类型 Succ[Succ[Succ[_0]]])，我们希望 toInt(x) 返回 3.

        Now, suppose we want to define a value-level function def toInt[T <: Nat](v : T) which takes in an argument value, v, that conforms to Nat and returns an integer representing the natural number encoded in v's type. For example, if we have the value val x:_3 = null (null of type Succ[Succ[Succ[_0]]]), we would want toInt(x) to return 3.

        要实现 toInt，我们将使用以下类:

        To implement toInt, we're going to make use of the following class:

        class TypeToValue[T, VT](value : VT) { def getValue() = value }
        

        正如我们将在下面看到的，对于从 _0 到(例如)_3，每个都会存储对应类型的值表示(即TypeToValue[_0, Int] 会存储值0, TypeToValue[Succ[_0], Int] 将存储值 1 等).注意，TypeToValue 被参数化为两种类型:T 和 VT.T 对应于我们试图赋值的类型(在我们的例子中，Nat)，VT 对应于我们要赋值的类型'正在分配给它(在我们的例子中，Int).

        As we will see below, there will be an object constructed from class TypeToValue for each Nat from _0 up to (e.g.) _3, and each will store the value representation of the corresponding type (i.e. TypeToValue[_0, Int] will store the value 0, TypeToValue[Succ[_0], Int] will store the value 1, etc.). Note, TypeToValue is parameterized by two types: T and VT. T corresponds to the type we're trying to assign values to (in our example, Nat) and VT corresponds to the type of value we're assigning to it (in our example, Int).

        现在我们做以下两个隐式定义:

        Now we make the following two implicit definitions:

        implicit val _0ToInt = new TypeToValue[_0, Int](0)
        implicit def succToInt[P <: Nat](implicit v : TypeToValue[P, Int]) = 
             new TypeToValue[Succ[P], Int](1 + v.getValue())
        

        我们实现了 toInt 如下:

        def toInt[T <: Nat](v : T)(implicit ttv : TypeToValue[T, Int]) : Int = ttv.getValue()
        

        要了解 toInt 的工作原理，让我们考虑一下它对几个输入的作用:

        To understand how toInt works, let's consider what it does on a couple of inputs:

        val z:_0 = null
        val y:Succ[_0] = null
        

        当我们调用 toInt(z) 时，编译器会寻找 TypeToValue[_0, Int] 类型的隐式参数 ttv(因为z 的类型为 _0).它找到对象_0ToInt，调用该对象的getValue 方法并返回0.需要注意的重要一点是，我们没有向程序指定使用哪个对象，编译器隐式地发现了它.

        When we call toInt(z), the compiler looks for an implicit argument ttv of type TypeToValue[_0, Int] (since z is of type _0). It finds the object _0ToInt, it calls the getValue method of this object and gets back 0. The important point to note is that we did not specify to the program which object to use, the compiler found it implicitly.

        现在让我们考虑 toInt(y).这一次，编译器查找类型为 TypeToValue[Succ[_0], Int] 的隐式参数 ttv(因为 y 的类型为 <代码>成功[_0]).它找到函数 succToInt，该函数可以返回适当类型的对象 (TypeToValue[Succ[_0], Int]) 并对其求值.此函数本身采用 TypeToValue[_0, Int] 类型的隐式参数 (v)(即，TypeToValue，其中第一个类型参数少了一个 Succ[_]).编译器提供 _0ToInt(如上面对 toInt(z) 的评估所做的那样)，并且 succToInt 构造一个新的 TypeToValue 对象，值为 1.同样，重要的是要注意编译器隐式提供所有这些值，因为我们无法显式访问它们.

        Now let's consider toInt(y). This time, the compiler looks for an implicit argument ttv of type TypeToValue[Succ[_0], Int] (since y is of type Succ[_0]). It finds the function succToInt, which can return an object of the appropriate type (TypeToValue[Succ[_0], Int]) and evaluates it. This function itself takes an implicit argument (v) of type TypeToValue[_0, Int] (that is, a TypeToValue where the first type parameter is has one fewer Succ[_]). The compiler supplies _0ToInt (as was done in the evaluation of toInt(z) above), and succToInt constructs a new TypeToValue object with value 1. Again, it is important to note that the compiler is providing all of these values implicitly, since we do not have access to them explicitly.

        检查您的工作

        有几种方法可以验证您的类型级计算是否按照您的预期进行.这里有一些方法.使要验证的两种类型A 和B 相等.然后检查以下编译:

        There are several ways to verify that your type-level computations are doing what you expect. Here are a few approaches. Make two types A and B, that you want to verify are equal. Then check that the following compile:

        • 等于[A, B]
          • with: trait Equal[T1 >: T2 <: T2, T2] (取自 apocolisp)

          或者，您可以将类型转换为值(如上所示)并对值进行运行时检查.例如.assert(toInt(a) == toInt(b))，其中 a 是 A 和 b 类型属于 B 类型.

          Alternatively, you can convert the type to a value (as shown above) and do a runtime check of the values. E.g. assert(toInt(a) == toInt(b)), where a is of type A and b is of type B.

          其他资源

          完整的可用结构集可以在 scala 的类型部分找到参考手册 (pdf).

          The complete set of available constructs can be found in the types section of the scala reference manual (pdf).

          Adriaan Moors 有几篇关于类型构造函数和相关主题的学术论文，并附有来自 Scala 的示例:

          Adriaan Moors has several academic papers about type constructors and related topics with examples from scala:

          • 更高的泛型种类 (pdf)
          • Scala 的类型构造函数多态性:理论与实践 (pdf)(博士论文，其中包括 Moors 之前的论文)
          • 类型构造函数多态推理
          • Generics of a higher kind (pdf)
          • Type Constructor Polymorphism for Scala: Theory and Practice (pdf) (PhD thesis, which includes the previous paper by Moors)
          • Type Constructor Polymorphism Inference

          Apocalisp 是一个包含许多 Scala 类型级编程示例的博客.

          Apocalisp is a blog with many examples of type-level programming in scala.

          • Scala 中的类型级编程 是一些类型级编程的精彩导览，其中包括布尔值、自然数(如上)、二进制数、异构列表等.
          • 更多 Scala Typehackery 是上面的 lambda 演算实现.
          • Type-Level Programming in Scala is a fantastic guided tour of some type-level programming which includes booleans, natural numbers (as above), binary numbers, heterogeneous lists, and more.
          • More Scala Typehackery is the lambda calculus implementation above.

          ScalaZ 是一个非常活跃的项目，它提供了使用各种扩展 Scala API 的功能类型级编程功能.这是一个非常有趣的项目，拥有大量的追随者.

          ScalaZ is a very active project that is providing functionality that extends the Scala API using various type-level programming features. It is a very interesting project that has a big following.

          MetaScala 是 Scala 的类型级库，包括自然数的元类型、布尔值、单位、HList 等.这是 Jesper Nordenberg(他的博客) 的一个项目.

          MetaScala is a type-level library for Scala, including meta types for natural numbers, booleans, units, HList, etc. It is a project by Jesper Nordenberg (his blog).

          Michid(博客) 有一些很棒的 Scala 类型级编程示例(来自其他答案):

          The Michid (blog) has some awesome examples of type-level programming in Scala (from other answer):

          • 使用 Scala 进行元编程第一部分:添加
          • 使用 Scala 进行元编程第二部分:乘法
          • Meta- Scala 编程第三部分:部分函数应用
          • Meta- Scala 编程:条件编译和循环展开
          • Scala 类型级别SKI演算的编码

          Debasish Ghosh(博客) 也有一些相关的帖子:

          Debasish Ghosh (blog) has some relevant posts as well:

          • Scala 中的高阶抽象
          • 静态输入让您有一个良好的开端
          • Scala 隐式类型类，我来了
          • 重构为 Scala 类型类
          • 使用广义类型约束立>
          • Scalas 如何输入系统词你
          • 在抽象类型成员之间进行选择

          (我一直在对这个主题进行一些研究，这是我学到的东西.我还是个新手，所以请指出这个答案中的任何不准确之处.)

          (I've been doing some research on this subject and here's what I've learned. I'm still new to it, so please point out any inaccuracies in this answer.)

          这篇关于Scala 类型编程资源的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！