Mehr Beweis benötigt als notwendig für Methode mit Shapeless

Question

Ich war gestern mit einigen Kollegen Shapeless erkunden, und wir beschlossen, eine Spielzeug-Methode zu einem ersten Parameter einer Fall-Klasse hinzufügen, wenn dieser Parameter ein Int:

ist

def addOneToCaseClass[C, H <: HList, E, T <: HList] 
    (c: C) 
    (implicit gen: Generic.Aux[C, H], 
       h: IsHCons.Aux[H, E, T], 
       ev: E =:= Int, 
       ev2: (Int :: T) =:= H 
    ): C = { 

    val hList = gen.to(c) 

    val elem = hList.head 
    val tail = hList.tail 

    val newElem = elem + 1 

    gen.from(newElem :: tail) 
} 

es scheint mir, dass die ev2 Parameter redundant ist - es kann sicher, dass E :: T =:= Int :: T gefolgert werden, aber der Compiler war nicht in der Lage, um dies zuzulassen.

Gibt es einen bestimmten Grund warum?

Answer 1

Ihre Intuitionen sind vernünftig, aber leider ist der Scala-Compiler nicht so clever genug, um ev2 von h und ev abzuleiten. Das Problem ist, dass h stellt nur fest, dass H zu E :: T zerlegt, es stellt nicht die Umkehrung, nämlich dass E und T kombinieren, um H zu entsprechen.

Die tersest Formulierung dieser, die ich mit ähnlich ursprünglichen aufwarten kann, hat aber ein weniger Zeuge,

def addOneToCaseClass[C, R <: HList, T <: HList](c: C) 
    (implicit 
    gen: Generic.Aux[C, R], 
    h: IsHCons.Aux[R, Int, T], 
    ev: (Int :: T) =:= R) = { 
    val hList = gen.to(c) 
    val elem = hList.head 
    val tail = hList.tail 
    gen.from(elem+1 :: tail) 
} 

Hier sind wir in der Lage den Beweis, dass E =:= Int unter Verwendung h zeigen zu beseitigen dass R zu Int :: T zerfällt. Allerdings müssen wir noch zeigen, dass Int :: T gleich R ist, um mit den aktualisierten Elementen über gen zurückzugehen.