Błąd w niejawnej rozdzielczości?

Question

Pracuję nad implementacją "bezkształtnego stylu" Okasaki's dense binary number system. Jest to po prostu połączona lista bitów na poziomie typu; rodzaj HList binarnych Digit s. Ukończyłem pierwszy szkic moich operacji, które obejmują standardowe operacje matematyczne, których można się spodziewać po liczbach naturalnych. Dopiero teraz zdaję sobie sprawę z dużego problemu w moim kodowaniu. Jak naprawić domyślną rozdzielczość w moim przykładzie Induction? Zachęcamy do wklejenia całego fragmentu kodu do REPL. W tym przykładzie jedyna zależność od bezkształtnego jest dla DepFn1 i DepFn2.

import shapeless.{ DepFn1, DepFn2 } 

sealed trait Digit 
case object Zero extends Digit 
case object One extends Digit 

sealed trait Dense { type N <: Dense } 

final case class ::[+H <: Digit, +T <: Dense](digit: H, tail: T) extends Dense { 
    type N = digit.type :: tail.N 
} 

sealed trait DNil extends Dense { 
    type N = DNil 
} 

case object DNil extends DNil 

/* ops */ 
trait IsDCons[N <: Dense] { 
    type H <: Digit 
    type T <: Dense 

    def digit(n: N): H 
    def tail(n: N): T 
} 

object IsDCons { 
    type Aux[N <: Dense, H0 <: Digit, T0 <: Dense] = IsDCons[N] { 
    type H = H0 
    type T = T0 
    } 

    def apply[N <: Dense](implicit ev: IsDCons[N]): Aux[N, ev.H, ev.T] = ev 

    implicit def isDCons[H0 <: Digit, T0 <: Dense]: Aux[H0 :: T0, H0, T0] = 
    new IsDCons[H0 :: T0] { 
     type H = H0 
     type T = T0 

     def digit(n: H0 :: T0): H = n.digit 
     def tail(n: H0 :: T0): T = n.tail 
    } 
} 

// Disallows Leading Zeros 
trait SafeCons[H <: Digit, T <: Dense] extends DepFn2[H, T] { type Out <: Dense } 

trait LowPrioritySafeCons { 
    type Aux[H <: Digit, T <: Dense, Out0 <: Dense] = SafeCons[H, T] { type Out = Out0 } 

    implicit def sc1[H <: Digit, T <: Dense]: Aux[H, T, H :: T] = 
    new SafeCons[H, T] { 
     type Out = H :: T 
     def apply(h: H, t: T) = h :: t 
    } 
} 

object SafeCons extends LowPrioritySafeCons { 
    implicit val sc0: Aux[Zero.type, DNil, DNil] = 
    new SafeCons[Zero.type, DNil] { 
     type Out = DNil 
     def apply(h: Zero.type, t: DNil) = DNil 
    } 
} 

trait ShiftLeft[N <: Dense] extends DepFn1[N] { type Out <: Dense } 

object ShiftLeft { 
    type Aux[N <: Dense, Out0 <: Dense] = ShiftLeft[N] { type Out = Out0 } 

    implicit def sl1[T <: Dense](implicit sc: SafeCons[Zero.type, T]): Aux[T, sc.Out] = 
    new ShiftLeft[T] { 
     type Out = sc.Out 
     def apply(n: T) = Zero safe_:: n 
    } 
} 

trait Succ[N <: Dense] extends DepFn1[N] { type Out <: Dense } 

object Succ { 
    type Aux[N <: Dense, Out0 <: Dense] = Succ[N] { type Out = Out0 } 

    def apply[N <: Dense](implicit succ: Succ[N]): Aux[N, succ.Out] = succ 

    implicit val succ0: Aux[DNil, One.type :: DNil] = 
    new Succ[DNil] { 
     type Out = One.type :: DNil 
     def apply(DNil: DNil) = One :: DNil 
    } 

    implicit def succ1[T <: Dense]: Aux[Zero.type :: T, One.type :: T] = 
    new Succ[Zero.type :: T] { 
     type Out = One.type :: T 
     def apply(n: Zero.type :: T) = One :: n.tail 
    } 

    implicit def succ2[T <: Dense, S <: Dense] 
    (implicit ev: Aux[T, S], sl: ShiftLeft[S]): Aux[One.type :: T, sl.Out] = 
     new Succ[One.type :: T] { 
     type Out = sl.Out 
     def apply(n: One.type :: T) = n.tail.succ.shiftLeft 
     } 
} 

/* syntax */ 
val Cons = :: 
implicit class DenseOps[N <: Dense](val n: N) extends AnyVal { 
    def ::[H <: Digit](h: H): H :: N = Cons(h, n) 

    def safe_::[H <: Digit](h: H)(implicit sc: SafeCons[H, N]): sc.Out = sc(h, n) 

    def succ(implicit s: Succ[N]): s.Out = s(n) 

    def digit(implicit c: IsDCons[N]): c.H = c.digit(n) 

    def tail(implicit c: IsDCons[N]): c.T = c.tail(n) 

    def shiftLeft(implicit sl: ShiftLeft[N]): sl.Out = sl(n) 
} 

/* aliases */ 
type _0 = DNil 
val _0: _0 = DNil 

val _1 = _0.succ 
type _1 = _1.N 

val _2 = _1.succ 
type _2 = _2.N 

/* test */ 
trait Induction[A <: Dense] 

object Induction{ 
    def apply[A <: Dense](a: A)(implicit r: Induction[A]) = r 
    implicit val r0 = new Induction[_0] {} 
    implicit def r1[A <: Dense](implicit r: Induction[A], s: Succ[A]) = 
    new Induction[s.Out]{} 
} 

Induction(_0) 
Induction(_1) 
Induction(_2) // <- Could not find implicit value for parameter r... 

This is a link to the question's follow up

Answer 1

Jest to nieco niekompletna odpowiedź, ale mam nadzieję, że Ci powieść ...

Myślę, że problem jest definicja r1 Tutaj

object Induction{ 
    def apply[A <: Dense](a: A)(implicit r: Induction[A]) = r 
    implicit val r0 = new Induction[_0] {} 
    implicit def r1[A <: Dense](implicit r: Induction[A], s: Succ[A]) = 
    new Induction[s.Out]{} 
} 

Gdy pytasz o numer Induction(_2), masz nadzieję na zastosowanie r1 i s.Out, który zostanie naprawiony jako _2 i że będzie sterował procesem wnioskowania od prawej do lewej w ukrytym bloku parametrów r1.

Niestety tak się nie stanie. Po pierwsze, s.Out nie zostanie naprawiony jako _2, ponieważ nie jest zmienną typu. Tak byś przynajmniej trzeba przepisać to jak

implicit def r1[A <: Dense, SO <: Dense] 
    (implicit r: Induction[A], s: Succ.Aux[A, SO]): Induction[SO] = 
    new Induction[SO]{} 

dla r1 nawet być stosowane. Nie spowoduje to jednak znacznie więcej, ponieważ SO jest ograniczone do równego elementowi typu Out z s ... nie odgrywa roli w wyborze instancji Succ dla s. I nie możemy zrobić żadnego postępu z drugiego końca, ponieważ w tym momencie A jest całkowicie nieokreślony, jeśli chodzi o typechecker.

Obawiam się, że będziesz musiał to trochę przemyśleć. Myślę, że najlepszym rozwiązaniem byłoby zdefiniowanie operatora Pred który pozwoliłby na określenie czegoś wzdłuż tych linii,

implicit def r1[S <: Dense, PO <: Dense] 
    (implicit p: Pred.Aux[S, PO], r: Induction[PO]): Induction[S] = 
    new Induction[S]{} 

Teraz, gdy prosimy o Induction(_2)S zostanie rozwiązany natychmiast _2 instancja Pred dla _2 będzie być rozwiązany, dostarczając rozwiązanie _1 dla PO, które daje typowi sprawdzającemu, co jest potrzebne do rozwiązania następnego etapu indukcji.

Należy zauważyć, że ogólną strategią jest rozpoczynanie od typu wyniku (Induction[S]) w celu naprawienia początkowych zmiennych typu (zmiennych), a następnie pracy od lewej do prawej na liście niejawnych parametrów.

Zauważ również, że dodałem jawne typy wyników do niejawnych definicji: prawie zawsze należy to robić (są rzadkie wyjątki od tej reguły).