Errore di risoluzione implicita?

Question

Ho lavorato a un'implementazione "stile senza forma" di Okasaki's dense binary number system. È semplicemente un elenco di bit collegati a livello di testo; una sorta di HList di binario Digit s. Ho completato una prima bozza delle mie operazioni, che include le operazioni matematiche standard che ti aspetteresti per i numeri naturali. Solo ora mi rendo conto di un grosso problema nella mia codifica. Come posso risolvere la risoluzione implicita nel mio esempio Induction? Sentiti libero di incollare l'intero snippet in REPL. In questo esempio, l'unica dipendenza da shapeless è per DepFn1 e 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

Questa è una risposta un po 'incompleta, ma si spera che ti farti scollarsi ...

Credo che il problema è la definizione di r1 qui,

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]{} 
} 

Quando chiedi Induction(_2), speri che sia applicabile r1 e s.Out da correggere come _2 e che guiderà il processo di inferenza da destra a sinistra nel blocco di parametri impliciti r1 s.

Purtroppo non succederà. Innanzitutto, s.Out non verrà risolto come _2 perché non è una variabile di tipo. Così si avrebbe per lo meno dovuto riscrivere questo come,

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

per r1 anche di essere applicabile. Questo non ti porterà molto oltre, perché SO è semplicemente vincolato per essere uguale al membro di tipo Out di s ... non ha alcun ruolo nella selezione dell'istanza Succ per s. E non possiamo fare progressi dall'altra parte, perché a questo punto A è completamente indeterminato per quanto riguarda il typechecker.

Quindi temo che dovrai ripensarci un po '. Credo che il tuo approccio migliore sarebbe quella di definire un operatore di Pred che permetterebbe di definire qualcosa in questo senso,

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

Ora, quando si chiede Induction(_2)S sarà risolto immediatamente come _2, l'istanza Pred per _2 volontà essere risolto, ottenendo una soluzione di _1 per PO che fornisce al tipografo ciò di cui ha bisogno per risolvere il prossimo passo dell'induzione.

Si noti che la strategia generale è di iniziare con il tipo di risultato (Induction[S]) per correggere le variabili di tipo iniziali, quindi lavorare da sinistra a destra attraverso l'elenco di parametri impliciti.

Notate anche che ho aggiunto tipi di risultati espliciti alle definizioni implicite: dovreste quasi sempre farlo (ci sono rare eccezioni a questa regola).