Scalaでの型レベルプログラミング

Question

私は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]] 
} 

ここで問題は、私が何を購入するのですか？どうすればそれを利用できますか？

Answer 1

これらのタイプを自分で作成する必要がある場合は、それほど大きなものにはなりません。しかし、あなたがコンパイラにあなたのためのものをやらせるとすぐに、それははるかに役に立つでしょう。私はこれを示す前に

すること、のは短いものにペアノaritmeticを表現する方法を変更してみましょう：

sealed trait Num 
case object Zero extends Num 
case class Succ[N <: Num](num: N) extends Num 

あなたは、コンパイル時に知られているサイズのリストを作成することができます。あなたの場合は

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] 

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)))) 

あなたがやろうとすることができることは、何かをチェックする暗黙の使用です。

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 

を限りScalaはときに表示される中で、私はタイプレベルのプログラミングの真の力を伝えることができるよう：あなたは、暗黙的な証拠が供給することができたときに、いくつかの操作のみ行うことができることを強制することができるとして

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]]] {} 

暗黙的な証拠、型クラスの導出、およびいくつかの構造的な定型文の削除に使用できる新しい型を作成するための暗黙的な使用を開始します。

一般的なプログラミングで多くを助けるライブラリはシェイプレスです。私は、あなたがインプライチを使っていくつかのタイプ・クラスの導出をして1つまたは2つの演習を行うと、あなたが仕事をするのは楽しいことだと信じています。

あなたのコードに戻ってくると、あなたのクラスのインスタンスを生成し提供することができます。また、新しいクラスを作成するだけでなく、このコードは他の処理も行います。それらのクラスに追加する要素のリストを組み合わせたり、PeanoNumTypeからIntに変換したり、コンパイル時などに動作する述語を追加したりすることができます。