-
-
Save joroKr21/e7f26f0330d51329296cc8a1cfb13cea to your computer and use it in GitHub Desktop.
This file contains 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
sealed abstract class SingletonOf[A, +B] { | |
} | |
object SingletonOf { | |
} | |
type <::[A, +B] = SingletonOf[A, B] | |
def single[A <: Singleton](a: A): SingletonOf[A, A] = | |
new SingletonOf[A, A] { } | |
type Nat = Nat.Type | |
object Nat { | |
type Base | |
trait Tag extends Any | |
type Type <: Base with Tag | |
type Z <: Type | |
type S[N] <: Type | |
val Z: Z = 0L.asInstanceOf[Z] | |
def S[N](n: N)(implicit ev: N <:: Nat): S[N] = | |
(n.asInstanceOf[Long] + 1).asInstanceOf[S[N]] | |
def cata[N, F[_]](n: N)(k: Cata[F])(implicit N: N <:: Nat): F[N] = { | |
val m: Long = n.asInstanceOf[Long] | |
var i: Long = 0 | |
var r: F[_] = k.z | |
while (i < m) { | |
r = k.s[N](r.asInstanceOf[F[N]]) | |
i += 1 | |
} | |
r.asInstanceOf[F[N]] | |
} | |
def fold[N, F[_]](n: N)(k: Fold[F])(implicit N: N <:: Nat): F[N] = { | |
val m: Long = n.asInstanceOf[Long] | |
if (m == 0) k.z.asInstanceOf[F[N]] | |
else k.s[N]((m - 1).asInstanceOf[N]).asInstanceOf[F[N]] | |
} | |
trait Cata[F[_]] { | |
def z: F[Z] | |
def s[N](n: F[N])(implicit ev: N <:: Nat): F[S[N]] | |
} | |
trait Fold[F[_]] { | |
def z: F[Z] | |
def s[N](n: N)(implicit ev: N <:: Nat): F[S[N]] | |
} | |
implicit val zIsSingleton: Z <:: Type = new SingletonOf[Z, Type] { } | |
implicit def sIsSingleton[N](implicit N: N <:: Type): S[N] <:: Type = new (S[N] <:: Type) { } | |
} | |
import Nat.{ Z, S } | |
type F[_] = Long | |
println(Nat.cata(S(S(S(Z))))(new Nat.Cata[F] { | |
def z: Long = 0 | |
def s[N](n: Long)(implicit ev: N <:: Nat): Long = n + 1 | |
})) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment