How to define induction on natural numbers in Scala 2.13?

Question

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?

Answer 1

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?

In scala, are there any condition where implicit view won't be able to propagate to other implicit function?

When calling a scala function with compile-time macro, how to failover smoothly when it causes compilation errors?

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

https://contributors.scala-lang.org/t/proposed-changes-and-restrictions-for-implicit-conversions/4923

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?