Created
August 20, 2014 20:19
-
-
Save david-christiansen/106dfc25fc3338bc8165 to your computer and use it in GitHub Desktop.
Simple presentation of singletons in Scala
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
package dep | |
import scala.language._ | |
object Dep extends App { | |
sealed trait Nat { | |
type Plus[M <: Nat] <: Nat | |
def plus[M <: Nat](m: M): Plus[M] | |
} | |
implicit object Z extends Nat { | |
type Plus[M <: Nat] = M | |
def plus[M <: Nat](m: M) = m | |
override def toString = "Z" | |
} | |
type Z = Z.type | |
case class S[N <: Nat](n: N) extends Nat { | |
type Plus[M <: Nat] = S[N#Plus[M]] | |
def plus[M <: Nat](m: M) = S(n plus m) | |
} | |
implicit def getS[N <: Nat](implicit n: N): S[N]= S(implicitly[N]) | |
type T0 = Z | |
type T1 = S[T0] | |
type T2 = S[T1] | |
type T3 = S[T2] | |
type T4 = S[T3] | |
type T5 = S[T4] | |
type T6 = S[T5] | |
type T7 = S[T6] | |
type T8 = S[T7] | |
type T9 = S[T8] | |
sealed trait Vect[+A, N <: Nat] { | |
def ++[B >: A, M <: Nat](other: Vect[B, M]): Vect[B, N#Plus[M]] | |
def length: N | |
} | |
final case object VNil extends Vect[Nothing, Z] { | |
def ++[B, M <: Nat](other: Vect[B, M]) = other | |
def length = implicitly | |
} | |
final case class VCons[A, B >: A, N <: Nat](b: B, xs: Vect[A, N]) extends Vect[B, S[N]] { | |
def ++[C >: B, M <: Nat](other: Vect[C, M]) = VCons(b, xs ++ other) | |
def length = S(xs.length) | |
} | |
val two: Vect[Int, T2] = VCons(1, VCons(2, VNil)) | |
val one: Vect[Int, T1] = VCons(3, VNil) | |
val three: Vect[Int, T3] = two ++ one | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This is some fantastic stuff. Thanks for taking the time to share it! I've actually turned that blog post along with some of the follow up posts into polished articles for NFJS Magazine. They've been received so well, I've decided to take them to leanpub and develop them further. I think the book will be unique having been written by someone actively learning the topic. 👍