Created
February 19, 2017 19:03
-
-
Save ragb/cb087d1befc85fc695decc38566fec28 to your computer and use it in GitHub Desktop.
Type-level natural numbers in Scala, with operations. Inspiration is Shapeless, but very simplified.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // This is a natural number | |
| trait Nat | |
| { | |
| type N <: Nat | |
| } | |
| // This is Zero | |
| class Zero extends Nat { | |
| type N = Zero | |
| } | |
| // This is the successor of Some natural number P, | |
| // which itself happens to be a natural number | |
| class Suc[P <: Nat] extends Nat { | |
| type N = Suc[P] | |
| } | |
| // Converts a type-level natural number to an integer (runtime) | |
| trait ToInt[N <: Nat] { | |
| def apply(): Int | |
| } | |
| object ToInt { | |
| case class ToIntInstance[N <: Nat](i : Int) extends ToInt[N] { | |
| def apply() = i | |
| } | |
| // Evidence that Zero -> 0 | |
| implicit val zeroToInt = ToIntInstance[Zero](0) | |
| // if we have a `ToInt` for some number | |
| // the `ToInt` for its successor is easily computed (sum 1) | |
| implicit def sucToInt[N <: Nat]( | |
| implicit nToInt: ToInt[N]) | |
| : ToInt[Suc[N]] = ToIntInstance[Suc[N]](nToInt() + 1) | |
| // implicit helper | |
| def apply[N <: Nat](implicit toInt: ToInt[N]) = toInt | |
| } | |
| // Give proper names to some numbers | |
| type One = Suc[Zero] | |
| type Two = Suc[One] | |
| // Print the runtime integer for the non-believers | |
| val toInt = ToInt[Two] | |
| println(toInt()) | |
| // More names | |
| type Three = Suc[Two] | |
| type Four = Suc[Three] | |
| type Five = Suc[Four] | |
| type Six = Suc[Five] | |
| // Tells that N + P = Out | |
| trait Plus[N, P] { | |
| type Out <: Nat | |
| } | |
| object Plus { | |
| // Aux pattern: makes the type member a type parameter | |
| type Aux[N <: Nat, P <: Nat, Out0 <: Nat] = Plus[N, P] { type Out = Out0} | |
| // 0 + N = N | |
| implicit def zeroPlusN[N <: Nat]: Aux[Zero, N, N] = new Plus[Zero, N] { type Out = N} | |
| // N + (P + 1) = Out -> (N + 1) + P = Out | |
| // Zero will be found, don't be afraid | |
| implicit def plus1[N <: Nat, P <: Nat]( | |
| implicit plus: Plus[N, Suc[P]]) | |
| : Aux[Suc[N], P, plus.Out] = new Plus[Suc[N], P] { type Out = plus.Out} | |
| // implicit helper | |
| def apply[N <: Nat, P <: Nat](implicit plus: Plus[N, P]) = plus | |
| } | |
| // Ask the compiler when in dobt | |
| implicitly[Plus.Aux[Two, Three, Five]] | |
| implicitly[Plus[Three, Three]] | |
| implicitly[Plus[Two, Five]] | |
| // Tells that N * P = Out | |
| trait Prod[N, P] { | |
| type Out <: Nat | |
| } | |
| object Prod { | |
| type Aux[N, P, Out0] = Prod[N, P] { type Out = Out0} | |
| // 0 * N = 0 | |
| implicit def prodZero[N <: Nat]: Aux[Zero, N, Zero] = new Prod[Zero, N] {type Out = Zero} | |
| // N * P = Q -> (N + 1) * P = Q + P, | |
| // P + Q = Out -> (N + 1) * P = Out | |
| implicit def prodSuc[N <: Nat, P <: Nat, Q <: Nat]( | |
| implicit prod: Prod.Aux[N, P, Q], // N * P = Q | |
| plus: Plus[P, Q]) // P + Q = plus.Out | |
| : Prod.Aux[Suc[N], P, plus.Out] // (N + 1) * P = plus.Out | |
| = new Prod[Suc[N], P] {type Out = plus.Out} | |
| def apply[N <: Nat, P <: Nat](implicit prod: Prod[N, P]) = prod | |
| } | |
| // Trust the compiller | |
| implicitly[Prod.Aux[Two, Two, Four]] | |
| // Tells that Factoria[N] = Out | |
| trait Factorial[N <: Nat] { | |
| type Out <: Nat | |
| } | |
| object Factorial { | |
| type Aux[N <: Nat, Out0 <: Nat] = Factorial[N] {type Out = Out0} | |
| // Factorial[0] = 1 | |
| implicit val factorialZero: Factorial.Aux[Zero, One] = new Factorial[Zero] { type Out = One} | |
| // Factorial(n+1) = (n + 1) * Factorial(N) | |
| implicit def FactorialSuc[N <: Nat, F <: Nat, F1 <: Nat]( | |
| implicit factN: Factorial.Aux[N, F1], // Factorial(N) = F1 | |
| prod: Prod.Aux[Suc[N], F1, F]) // (n + 1) * F1 = F | |
| : Factorial.Aux[Suc[N], F] // Factorial(N + 1) = F | |
| = new Factorial[Suc[N]] { type Out = F} | |
| def apply[N <: Nat](implicit factorial: Factorial[N]) = factorial | |
| } | |
| implicitly[Factorial.Aux[Zero, One]] | |
| implicitly[Factorial.Aux[Three, Six]] | |
| Factorial[Four] |
Author
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
To run with ammonite