Consider the following definition of natural numbers.
sealed trait Nat
final case object Z extends Nat
final case class S[N <: Nat]() extends Nat
And the following definition of vectors.
sealed trait Vec[N <: Nat, +A]
final case object Nil extends Vec[Z.type, Nothing]
final case class Cons[N <: Nat, +A](head: A, tail: Vec[N, A]) extends Vec[S[N], A]
Now, I defined the induction on natural numbers as follows.
trait Alg[P[_ <: Nat]] {
val z: P[Z.type]
def s[N <: Nat](p: P[N]): P[S[N]]
}
def ind[N <: Nat, P[_ <: Nat]](alg: Alg[P])(implicit indN: Alg[P] => P[N]) = indN(alg)
implicit def indZ[P[_ <: Nat]](): Alg[P] => P[Z.type] = alg => alg.z
implicit def indS[N <: Nat, P[_ <: Nat]](implicit indN: Alg[P] => P[N]): Alg[P] => P[S[N]] = alg => alg.s(indN(alg))
And, I want to use it to define a function that creates a fixed size vector.
def rep[N <: Nat, A](head: A) = {
type P[N <: Nat] = Vec[N, A]
val alg = new Alg[P] {
val z: P[Z.type] = Nil
def s[N <: Nat](tail: P[N]): P[S[N]] = Cons(head, tail)
}
ind[N, P](alg) // No implicit view available from Alg[P] => P[N]
}
val vec = rep[S[S[S[Z.type]]], Int](37) // expected Cons(37, Cons(37, Cons(37, Nil)))
Unfortunately, this doesn't work. Scala doesn't know which implicit value to use. How can I make this work?
First of all, don't put () in implicit def indZ[P[_ <: Nat]](). The implicits implicit def indZ[P[_ <: Nat]]() and implicit def indZ[P[_ <: Nat]] are very different
How to write an implicit Numeric for a tuple
It's convenient to introduce type Z = Z.type. Then you can write just Z instead of Z.type.
Scala is not an actual theorem prover. Implicits are not resolved like that. If you defined implicit def indZ and implicit def indS, Scala knows implicits (and their types) indZ, indS(indZ), indS(indS(indZ)), ... but it can't generate an implicit of an unknown length indS(...(indS(indZ))). So with inductive logic based on implicits you can prove theorems for a fixed N (like Z, S[Z], S[S[Z]], ...) but not for arbitrary N (or for arbitrary N but with implicits of a fixed length). At those places where you have arbitrary N you should add an evidence (implicit parameter) Alg[P] => P[N], it will be checked later for a concrete N. So to say, if a method lacks an implicit (see your compile error No implicit view available from Alg[P] => P[N]) then you just add it as an implicit parameter:
Scala: Question about shapeless to tranform HList to List
Implicit Encoder for TypedDataset and Type Bounds in Scala
How to resolve implicit lookup by bounded generic?
Typeclasses methods called in functions with type parameters
Play-JSON cannot find implicit Writes[T] for type parameter T
Why the Scala compiler can provide implicit outside of object, but cannot inside?
So try
class Rep[A](head: A) {
type P[N <: Nat] = Vec[N, A]
val alg = new Alg[P] {
val z: P[Z] = Nil
def s[N <: Nat](tail: P[N]): P[S[N]] = Cons(head, tail)
}
def apply[N <: Nat](implicit ev: Alg[P] => P[N]): P[N] = ind[N, P](alg)
// ^^^^^^^^^^^^^^^^^^^^^^^^^^^ added
}
val vec = new Rep[Int](37)[S[S[S[Z]]]] // Cons(37, Cons(37, Cons(37, Nil)))
Be careful with building your logic on implicits of functional type Alg[P] => P[N]. Functional types play special role for implicits, they are for implicit conversions and such implicits are resolved slightly differently than implicits of all other types:
Implicit view not working - is my implicit def to blame?
Scala Kleisli throws an error in IntelliJ
What are the hidden rules regarding the type inference in resolution of implicit conversions?
https://contributors.scala-lang.org/t/can-we-wean-scala-off-implicit-conversions/4388
This is improved in Scala 3: https://docs.scala-lang.org/scala3/reference/contextual/conversions.html (a new type class Conversion is introduced instead of standard functional type, although currently with more restrictions than in Scala 2, for example implicit conversions into a path-dependent type are currently impossible - But https://github.com/lampepfl/dotty/issues/7412 https://github.com/lampepfl/dotty/pull/8523).
It can be better to introduce a new type class TC[P[_ <: N], N <: Nat] and build your inductive logic on TC[P, N] rather than standard functional types Alg[P] => P[N].
It's important to know how to debug implicits (at compile time)
In scala 2 or 3, is it possible to debug implicit resolution process in runtime?