Scala類型編程資源

根據this question，Scala的類型系統是Turing complete。有哪些資源可以使新手充分利用類型級編程的力量？Scala類型編程資源

這裏是我到目前爲止發現的資源：

這些資源是巨大的，但我覺得我錯過了基礎知識，所以沒有堅實的基礎來構建。例如，哪裏有對類型定義的介紹？我可以在類型上執行哪些操作？

有沒有什麼好的入門資源？

來源

2010-12-11 dsg

社區wiki？ – 2010-12-11 09:01:37

就我個人而言，我發現有人想要在Scala中進行類型編程已經知道如何在Scala中編程非常合理。即使這意味着我不理解你鏈接到的那些文章的一個詞:-) – 2010-12-11 12:58:17

133

概述

類型層次的編程與傳統，價值層次的編程有許多相似之處。但是，與運行時發生計算的值級編程不同，在類型級編程中，計算髮生在編譯時。我將嘗試在價值層次的編程和類型層次的編程之間進行比較。

範式

有在類型級別的編程兩個主要範式：「面向對象」和「功能」。從這裏鏈接到的大多數例子遵循面向對象的範例。

在面向對象範型級編程的一個很好的，很簡單的例子可以在apocalisp的implementation of the lambda calculus發現，這裏複製：

// 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 
}

正如在本例中可以看出，面向對象類型級編程的範例如下進行：

第一：用各種抽象類型字段定義一個抽象特徵（參見下文抽象字段是什麼）。這是一個用於保證所有實現中都存在某些類型字段而不強制執行的模板。在lambda微積分示例中，這對應於trait Lambda，它確保存在以下類型：subst,apply和eval。
下一頁：定義擴展抽象性狀subtraits和實施各種抽象類型字段
- 通常，這些subtraits將與參數進行參數化。在演算例如，亞型是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]。這本質上是調用eval類型的特徵參數S，並調用apply與參數T對結果。請注意，S保證有一個eval類型，因爲該參數指定它是Lambda的子類型。類似地，eval的結果必須具有apply類型，因爲它被指定爲Lambda的子類型，如抽象特徵Lambda中所指定的那樣。

的功能範例包括定義許多未在特徵組合在一起，參數化類型構造的。

值電平編程和類型級編程的比較

abstract class
- 值級別：abstract class C { val x }
- 類型級：trait C { type X }
路徑依賴類型
- C.x（引用字段值/功能在對象C X）
- C#x（在性狀ç引用字段類型爲x）
函數簽名（未實施）
- 值電平：def f(x:X) : Y
- type-level：type f[x <: X] <: Y（這稱爲「類型構造函數」，通常發生在抽象特徵中）
函數實現
- 值級別：def f(x:X) : Y = x
- 類型級：type f[x <: X] = x
條件句
- see here
檢查平等
- 值級別：a:A == b:B
- 類型級：implicitly[A =:= B]
- 值級別：在運行時通過一個單元測試發生在JVM（即沒有運行時的錯誤）：
  - 在essense是斷言：assert(a == b)
- 類型級：經由一個類型檢測在編譯器會發生（即沒有編譯器錯誤）：
  - 在本質上是類型比較：例如implicitly[A =:= B]
  - A <:< B，編譯僅當A是B
  - A =:= B一個亞型，編譯僅當A是B和B一個亞型的A
  - A <%< B一個亞型，（「可視」）的編譯僅當A可見爲B（ie存在從A到的B亞型的隱式轉換）
  - an example
  - more comparison operators

類型之間轉換和值

在許多的前通過特徵定義的類型通常都是抽象的和密封的，因此既不能直接實例化，也不能通過匿名子類實例化。因此，在使用某種興趣類型進行值級計算時，通常使用null作爲佔位符值：
- 例如， val x:A = null，其中A的類型是你所關心的
由於類型擦除，參數化類型看起來都一樣。此外，（如上所述），您使用的值往往都是null，因此對對象類型進行條件處理（例如，通過匹配語句）是無效的。

訣竅是使用隱式函數和值。基本情況通常是一個隱含的值，遞歸情況通常是一個隱式函數。事實上，類型級編程大量使用了implicits。

考慮這個例子（taken from metascala和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]]（繼承者對代表零的類型應用兩次）。

我們可以別名各種自然數爲更方便的參考。例如：

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

（這是像限定val是一個函數的結果很多）

現在，假設我們要定義一個值級函數def toInt[T <: Nat](v : T)這需要在一個參數值，v，它符合Nat並返回一個整數，表示在v的類型中編碼的自然數。例如，如果我們的值爲val x:_3 = null（null，類型爲Succ[Succ[Succ[_0]]]），我們希望toInt(x)返回3。

要實現toInt，我們要充分利用以下類：

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

正如我們下面將看到的，將有來自TypeToValue類構造的每個Nat從_0長達一個對象（例如）_3，並且每個將存儲對應類型的值表示（即TypeToValue[_0, Int]將存儲值0,TypeToValue[Succ[_0], Int]將存儲值1等）。請注意，TypeToValue由兩種類型參數化：T和VT。 T對應於我們試圖賦予值的類型（在本例中爲Nat），而VT對應於我們分配給它的值的類型（在我們的示例中爲Int）。

現在我們提出以下兩個隱含的定義：

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是如何工作的，讓我們來看看它做什麼一對夫婦的投入：

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

當我們撥打toInt(z)，編譯器查找TypeToValue[_0, Int]類型的隱式參數ttv（因爲z的類型爲_0）。它找到對象_0ToInt，它調用該對象的getValue方法並取回0。需要注意的重要一點是，我們沒有向程序指定使用哪個對象，編譯器隱式地發現它。

現在讓我們考慮一下toInt(y)。這一次，編譯器查找類型爲TypeToValue[Succ[_0], Int]的隱式參數ttv（因爲y的類型爲Succ[_0]）。它找到函數succToInt，它可以返回適當類型的對象（TypeToValue[Succ[_0], Int]）並對其進行評估。該函數本身採用TypeToValue[_0, Int]類型的隱式參數（v）（即TypeToValue，其中第一個參數的類型爲Succ[_]）。編譯器提供_0ToInt（如上面對toInt(z)的評估中所做的那樣），並且succToInt構造了一個新的TypeToValue對象，其值爲1。同樣，重要的是要注意編譯器隱式提供所有這些值，因爲我們沒有顯式地訪問它們。