Ich habe an einer "formlosen" Implementierung von @ gearbeit Okasakis dichtes Binärzahlensystem. Es ist einfach eine verkettete Liste von Bits auf Typebene. eine ArtHList of binaryDigits. Ich habe einen ersten Entwurf meiner Operationen fertiggestellt, der die Standard-Rechenoperationen enthält, die Sie für natürliche Zahlen erwarten würden. Erst jetzt erkenne ich ein großes Problem in meiner Codierung. Wie behebe ich die implizite Auflösung in meinemInduction beispiel? Fühlen Sie sich frei, das gesamte Snippet in eine REPL einzufügen. In diesem Beispiel ist die einzige Abhängigkeit von shapeless fürDepFn1, undDepFn2.

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...

Dies ist ein Link zum Follow-up der Frage