Örtük Çözünürlük Hatası?

Question

Okasaki's dense binary number system'un "shapeless stili" uygulaması üzerinde çalışıyorum. Bu basitçe tip-düzeyli bitler listesidir; İkili Digit s'nin HList bir tür. Doğal sayılar için beklediğiniz standart matematik işlemlerini içeren ilk operasyonlarımı tamamladım. Sadece şimdi kodlamada büyük bir sorun olduğunu anlıyorum. Induction örneğindeki örtük çözünürlüğü nasıl giderebilirim? Parçacıkların tümünü bir REPL'ye yapıştırmaktan çekinmeyin. Bu örnekte, şekilsizliğe olan tek bağımlılık DepFn1 ve DepFn2 içindir. ,

Ben senin sorunun burada r1 tanımı olduğunu düşünüyorum ...

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

Bu biraz eksik cevabı, ama umarım yanılmak seni alırsınız

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(_2) için istendiğinde, r1'un geçerli olmasını ve s.Out, _2 olarak sabitlenecek ve bu, çıkarım işlemini r1 s örtük parametre bloğunda sağdan sola sürecek.

Maalesef bu olmayacak. İlk olarak, s.Out, bir tür değişkeni olmadığından _2 olarak düzeltilmez. Yani en azından r1 için

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

bile geçerli olmak üzere, bu yeniden yazmak gerekir. Ancak bu, SO'un'un Out tip elemanına eşit olması için sınırlı olduğundan, s için Succ örneğinin seçiminde bir rol oynamaz. Ve diğer ucundan herhangi bir ilerleme kaydedemeyiz, çünkü bu noktada A, typechecker söz konusu olduğunda tamamen belirsizdir.

Korkarım ki bunu biraz düşünmelisiniz. Ben _2 için, en iyi yaklaşım, bu satırlar boyunca bir şey tanımlamak için izin verecek bir Pred operatörü tanımlamak olacaktır Eğer Induction(_2)S sormak Şimdi ne zaman _2 olarak derhal çözülecektir

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

, Pred örneği düşünmek olacak çözülecek, PO için _1 çözümü sağlayarak, indekslemenin bir sonraki adımını çözmek için ihtiyaç duyduğu şeyi yazmacıya verir.

Genel stratejinin, başlangıç ​​türü değişkenlerini düzeltmek için sonuç türüyle (Induction[S]) başlaması ve sonra örtülü parametre listesinden soldan sağa doğru çalışması olduğuna dikkat edin.

Ayrıca, açık sonuç türlerini örtük tanımlara eklediğime de dikkat edin: Bunu her zaman yapmalısınız (bu kuralın nadir istisnaları vardır).