Więcej dowodów potrzebnych niż w przypadku metody wykorzystującej Shapeless

Question

Wczoraj odkryłem Shapeless z kilkoma kolegami i zdecydowaliśmy się napisać metodę zabawki, aby dodać ją do pierwszego parametru klasy sprawy, gdy parametr ten to Int:

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

wydaje mi się, że parametr ev2 jest zbędna - na pewno można wywnioskować, że E :: T =:= Int :: T, ale kompilator nie był w stanie dokonać tego dopuścić.

Czy istnieje jakiś szczególny powód, dla którego?

Answer 1

Twoje intuicje są rozsądne, ale niestety kompilator Scala nie jest wystarczająco sprytny, aby wyprowadzić ev2 z h i ev. Problem polega na tym, że h ustala tylko, że H rozkłada się na E :: T, nie ustanawia on odwrotności, a mianowicie, że E i T są połączone na równą H.

tersest sformułowanie to, że mogę wymyślić jest podobna do oryginału, ale ma jeden mniej świadka,

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

Tutaj jesteśmy w stanie wyeliminować dowód, że E =:= Int za pomocą h do pokazania że R rozkłada się do Int :: T. Jednak wciąż musimy pokazać, że Int :: T jest równe R, aby przenieść ponownie gen ze zaktualizowanymi elementami.