オプションで、シェイプレスのサイズリストの先頭を変更します。

Question

Sizedリストを指定します。ヘッドが存在する場合、ヘッドを修正する方法はありますか？ある

def addOneToHeadIfExists[N <: Nat](l: Sized[IndexedSeq[Int], N]): Sized[IndexedSeq[Int], N] = ??? 

は、私が呼び出すことができます：

val x: Sized[IndexedSeq[Int], _3] = Sized(1, 2, 3) 
addOneToHeadIfExists(x) // gives Sized(2, 2, 3) 

val y: Sized[IndexedSeq[Int], _0] = Sized() // sample. doesn't actually compile 
addOneToHeadIfExists(x) // gives Sized() 

Answer 1

型崩れの大きさの種類の主な目的はで値についての十分な情報を提供することである1は、FFを定義する方法である

、このソートのプロパティのランタイムテストは不要です。

サイズコレクションが空でないこと、つまりheadとtailが明確に定義されていることが非常にわかりやすく、暗黙的な証拠がすぐには必要ない場合はまれなケースの1つです。これは、length型の引数に少なくとも1つの外側の型コンストラクタを必要とすることによって、シーケンスが0より大きいサイズの制約を取得できるからです。

これは、この方法は、Nは0

より大きい全てのNAT用Nat、すなわち、すべてのNためSucc[N]の長さのサイズの配列に対して定義され、私たち

def addOneToHead[N <: Nat](l: Sized[IndexedSeq[Int], Succ[N]]): 
    Sized[IndexedSeq[Int], Succ[N]] = (l.head+1) +: l.tail 

を与えますREPLセッションのサンプル：

scala> addOneToHead(Sized(1, 2, 3)) 
res0: shapeless.Sized[IndexedSeq[Int],shapeless.Succ[shapeless.nat._2]] = 
     Vector(2, 2, 3) 

scala> addOneToHead(Sized()) 
<console>:16: error: polymorphic expression cannot be instantiated to expected type 
found : [CC[_]]shapeless.Sized[CC[Nothing],shapeless._0] 
required: shapeless.Sized[IndexedSeq[Int],shapeless.Succ[?]] 
    addOneToHead(Sized()) 
         ^

これはタイプエラーですコンパイラは_0タイプをSucc[N]と統合することはできません。すべてのナットタイプはNです。