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.

### Like this:

Like Loading...

*Related*

Pingback: Type-Level Programming in Scala « Apocalisp

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

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.