This post was posted by Jilen on the ScalaCool team blog.

The previous article introduced an important feature of Shapeless: the automatic derivation of typeclass instances. In this article, I’ll explain a seemingly useless but in fact shapeless cornerstone of generic programming: Nat (natural numbers)

Peano Axioms

First let’s make sure that the natural numbers are just a sign system. Let’s use 0,1,2… These symbols represent some abstract concepts

Peano’s axiom tells us that this symbolic system has three components

  • An initial element (such as 0) x
  • A set X
  • A mapping of X to itself f

And the system satisfies the following axioms

  1. X is a member of x.
  2. X is not in the range of f.
  3. iff(a) = f(b) 则 a = b(that f is injective)
  4. If a is a member of X, then f of a is a member of X
  5. If A is A subset of X and satisfies
  • X is A member of A and
  • If a is a member of A, then f of a is a member of A and then a is equal to X

A first-order arithmetic system can be established based on the above axioms

The mapping between Nat types and natural numbers

trait Nat {
  type N <: Nat
}

case class Succ[P< :Nat] () extends Nat {
  type N = Succ[P]}class _0 extends Nat with Serializable {
  type N = _0}Copy the code

It is easy to summarize the correspondence between Nat types and natural numbers

  • X for allNatsubtypes
  • Succ is a mappingf, note that a type constructor can be thought of as a map
  • _0 is the initial element

Nat corresponds to the above axioms

  • 1. _0 is the Nat subtype
  • Second, _0 is clearly not any type of Succ, and the Scala compiler’s type checking ensures that Succ[P] is not equal to _0
  • 3. Assuming there is A, B satisfies A! = B and Succ[A] = Succ[B], also compiler type checking can ensure that if A! If (A, B) = B, then Succ[A]! = Succ[B], that is, Succ is injective
  • 4. The definition of Succ directly states that if P is Nat, Succ is Nat
  • In article 5, A is the definition of Nat type.

Addition to define

With these axioms in place, we can build a Peyanot arithmetic system, which takes addition as an example and defines addition as a mapping that satisfies the following relation

  1. a + 0 = 0
  2. a + Succ(b) = Succ(a + b)

In Shapeless, the addition definition is as follows (see here for Aux types)


trait Sum[A< :Nat.B< :Nat] extends Serializable { type Out <: Nat }
object Sum {
    type Aux[A< :Nat.B< :Nat.C< :Nat] = Sum[A.B] { type Out = C }
    // defined at 1
    implicit def sum1[B< :Nat] :Aux[_0, B.B] = new Sum[_0, B] { type Out = B }
    // The definition here is slightly different from 2
    implicit def sum2[A< :Nat.B< :Nat.C< :Nat]
      (implicit sum : Sum.Aux[A.Succ[B].C) :Aux[Succ[A].B.C] =
      new Sum[Succ[A].B] { type Out = C}}Copy the code

Sum[A, Succ[B]].c = Sum[Succ[A], B].c, The second rule of addition requires that Sum[A, Succ[B]].c = Succ[Sum[A, B].c] shapeless. This definition actually leads to rule 2.

Convert the above type into a statement: A + S(b) = S(a) + b => A + S(b) = S(a + b)

Here is the proof (S is a subsequent mapping, Succ)

  • B = 0a + S(0) = S(a) + 0 = S(a) = S(a + 0)
  • When b is equal to x,a + S(x) = S(a + x)If true, then b = S(xa + S(S(x)) = S(a) + S(x) = S(S(a) + x) = S(a + S(x)), it can be concluded that forB = S(x), a + S(b) = S(a + b)Also set up
  • These two generalizations lead to the proposition

Now, how do you constrain a type with Sum

object alias {
  type _1 = Succ[_0]
  type _2 = Succ[_1]
  type _3 = Succ[_2]}import alias._

def check[A< :Nat.B< :Nat] (implicit sum: Sum.Aux[A.B, _3]) = {} check [_0 _3] check check [_1, _2] [_2, _1] check [_3, _0] check [_1, _1]// Error compiling

Copy the code

The check method requires the Sum of the two types to be _3. It can be seen that only A and B whose Sum is _3 can be compiled

conclusion

This article introduces an important basic type of SHApeless, Nat. Understanding this type is an important prerequisite for mastering the other types of Shapeless