Understanding recursion in type-level programming: comparing Peano numbers

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

Understanding recursion in type-level programming: comparing Peano numbers

Hugo Ferreira
Hello,

I am looking at Apocalisp blog [1] attempting to understand the way Nat are compared.
I just about understand how this works except for the following (most important) code:

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]
}


The question is:

In the Compare type we pass on the type N#Compare as a parameter to O#Match. But this compare type requires
another "parameter". So were does it come from? Am I correct in saying that the O#Match type binds NonZero[N <: Nat] to
N#Compare effectively making NonZero[N] = N#Comopare[N]?

TIA.
Hugo F.


[1] https://apocalisp.wordpress.com/2010/06/17/type-level-programming-in-scala-part-4b-comparing-peano-numbers/

--
You received this message because you are subscribed to the Google Groups "scala-user" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|

Understanding recursion in type-level programming: comparing Peano numbers

Jasper-M
Yes. Compare accepts a type constructor as first parameter. So when you pass in an argument you only have to write the name of the type constructor you're passing in, without applying it.
It's like when a function accepts another function. But on the type level.

--
You received this message because you are subscribed to the Google Groups "scala-user" group.
To unsubscribe from this group and stop receiving emails from it, send an email to [hidden email].
For more options, visit https://groups.google.com/d/optout.