# Type-Level Programming in Scala, Part 4b: Comparing Peano numbers

Next, let’s look at comparing natural numbers. Define a Comparison type as follows:

```sealed trait Comparison {
type Match[IfLT <: Up, IfEQ <: Up, IfGT <: Up, Up] <: Up

type gt = Match[False, False, True, Bool]
type ge = Match[False, True, True, Bool]
type eq = Match[False, True, False, Bool]
type le = Match[True, True, False, Bool]
type lt = Match[True, False, False, Bool]
}
```

The implementations look like:

```sealed trait GT extends Comparison {
type Match[IfLT <: Up, IfEQ <: Up, IfGT <: Up, Up] = IfGT
}
sealed trait LT extends Comparison {
type Match[IfLT <: Up, IfEQ <: Up, IfGT <: Up, Up] = IfLT
}
sealed trait EQ extends Comparison {
type Match[IfLT <: Up, IfEQ <: Up, IfGT <: Up, Up] = IfEQ
}
```

We can then define a Compare type member for Nat. It is shown here along with the Match type we defined in the last post.

```sealed trait Nat {
type Match[NonZero[N <: Nat] <: Up, IfZero <: Up, Up] <: Up

type Compare[N <: Nat] <: Comparison
}
```

For _0#Compare, the resut is EQ if the other Nat is _0 and LT if it is not.

```sealed trait _0 extends Nat {
type Match[NonZero[N <: Nat] <: Up, IfZero <: Up, Up] = IfZero

type Compare[N <: Nat] =
N#Match[ConstLT, EQ, Comparison]

type ConstLT[A] = LT
}
```

For Succ[N]#Compare, the result is GT if the other Nat is _0 and it recurses if it is not. The recursion compares O-1 to N. (Remember that N is Succ[N] – 1.)

```sealed trait Succ[N <: Nat] extends Nat {
type Match[NonZero[N <: Nat] <: Up, IfZero <: Up, Up] = NonZero[N]

type Compare[O <: Nat] =
O#Match[N#Compare, GT, Comparison]
}
```

This recursion is allowed because Compare implements an abstract type in a super-trait and the bound of that abstract type doesn’t change during recursion. We call N#Compare so we aren’t directly recursing, which wouldn’t be allowed.

Examples:

```scala> toBoolean[ _0#Compare[_0]#eq ]
res0: true

scala> toBoolean[ _0#Compare[_0]#lt ]
res1: false

scala> toBoolean[ _3#Compare[_4]#le ]
res2: true
```

When we get to our binary search tree, Compare allows us to use Nats as keys in the tree. Next, we’ll define a general way to recurse on Nat using folds.

## 4 thoughts on “Type-Level Programming in Scala, Part 4b: Comparing Peano numbers”

1. Hi Mark,

I need clarification for this part:

sealed trait Succ[N <: Nat] extends Nat {
type Match[NonZero[N <: Nat] <: Up, IfZero <: Up, Up] = NonZero[N]

type Compare[O <: Nat] =
O#Match[N#Compare, GT, Comparison]
}

I will explain my questions on this example : toBoolean[ _3#Compare[_4]#le ]

Declaring O#Match is actually Match declaration of previous number, _2 in this case ?
Allo N#Compare is Match declaration of previous number,_3 in this case ?

I suppose idea is to go down until O or N is zero so system can figure out final type?

Which type parameter, 0?, for N#Compare[O?] declaration will be used in part of this declaration O#Match[N#Compare, GT, Comparison] ?
Is it O and how system figure out it, just because name ?

Thanks

P.S.

Also thanks for articles on this blog they are great for learning

2. I made mistake in previous post, I revert values for N and O. Actually I am not shure how O has been decreased through recursion.

• I think I have figure out how it works.
Compiler evaluates O#Match[N#Compare, GT, Comparison]
to NonZero[N] where NonZero is N#Compare and N is N from O#Match which is previous number of O so we get N#Compare[O-1] in next recursion step. Process go further unitl one of them reach zero.