型崩れHListがアペンダ

Question

私はUpdaterは私が欲しいものに最も近いことが判明し、HListを追加します関数を記述しようとしています：

def appender[L <: HList, V, Out <: HList](hl: L, k: Witness, v: V)(implicit updater: Updater.Aux[L, FieldType[k.T, V], Out]) : Out = { 
    updater(hl, field[k.T](v)) 
    } 

私はHListを追加、更新して、この機能を持っています、私は更新を無効にして、関数が追加できるようにしたいので、次のようにしてください：

val hl = 'field1 ->> 1 :: HNil 
appender(hl, 'field2, 2) //should compile 
appender(hl, 'field1, 2) //should fail 

現在のところ、両方がコンパイルされています。とにかく私はこの制約をシェイプレスで表現できますか？私はおそらくOutタイプがinタイプより1つ長いエレメントであるという証拠を尋ねることは可能でしょうか？

Answer 1

使用shapeless.ops.record.LacksKey：後世のために

def appender[L <: HList, V, Out <: HList](hl: L, k: Witness, v: V)(implicit 
                    updater: Updater.Aux[L, FieldType[k.T, V], Out], 
                    lk: LacksKey[L, k.T]) : Out = { 
    updater(hl, field[k.T](v)) 
    } 

Answer 2

は、ここにあなたの長さチェックのアイデアを使用しての答えです。しかし、LacksKeyの方が良いです。また、Updaterは、キーを再利用して別のタイプを使用すると、重複キーを作成します（結局、タイプが実際にキーの一部であるため）。appendは同じことを意味します。あなたは、同じパラメータリスト内の他のパラメータに言及型のパラメータを持つことができませんので、あなたの計算のすべてのタイプレベルの値は、型パラメータである必要が

def append[ 
    Value, 
    In <: HList, 
    Out <: HList, 
    InSize <: Nat, 
    OutSize <: Nat, 
    AddedNum <: Nat 
](in: In, key: Witness, value: Value)(implicit 
    update: Updater.Aux[In, FieldType[key.T, Value], Out], 
    inSize: Length.Aux[In, InSize], 
    outSize: Length.Aux[Out, OutSize], 
    addedNum: ops.nat.Diff.Aux[OutSize, InSize, AddedNum], // ops.{hlist, nat}.Diff conflict 
    sizeRestriction: AddedNum =:= _1 // Bonus: error messages are fairly readable: "Cannot prove that AddedNum = Succ[_0]" (followed by a horrifyingly long "not enough arguments" error). 
): Out = update(in, field[key.T](value)) 

注意。コンパイラに各ステップを処理できる以上のことを決して行うことを決して慎重にする必要はありません。