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.

About these ads

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

  1. Pingback: Type-Level Programming in Scala « Apocalisp

  2. 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

  3. 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.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s