Skip to content

Instantly share code, notes, and snippets.

@lastland
Created September 4, 2016 04:29
Show Gist options
  • Save lastland/62bbf3ffe1b898645bf98aecc6c48075 to your computer and use it in GitHub Desktop.
Save lastland/62bbf3ffe1b898645bf98aecc6c48075 to your computer and use it in GitHub Desktop.
Dependently Typed Vector in Scala
package dependent
import scala.language.implicitConversions
import shapeless._, shapeless.nat._
object Vector {
trait Vec[+A, N <: Nat]
case object Nil extends Vec[Nothing, _0]
case class Cons[+A, N <: Nat](h: A, t: Vec[A, N]) extends Vec[A, Succ[N]]
implicit def narrow[A, N <: Nat](v: Vec[A, Succ[N]]): Cons[A, N] = v match {
case vc @ Cons(_, _) => vc
}
trait SNat[A, N <: Nat] {
def apply(a: A): Vec[A, N]
}
implicit def zNat[A] = new SNat[A, _0] {
def apply(a: A) = Nil
}
implicit def sNat[A, N <: Nat](implicit nat: SNat[A, N]) =
new SNat[A, Succ[N]] {
def apply(a: A) = Cons(a, rep[A, N](a))
}
def rep[A, N <: Nat](a: A)
(implicit snat: SNat[A, N]): Vec[A, N] = snat(a)
trait Plus[A, XS, YS] {
type MN <: Nat
type Out = Vec[A, MN]
def apply(xs: XS, ys: YS): Out
}
implicit def zPlus[A, N <: Nat] =
new Plus[A, Vec[A, _0], Vec[A, N]] {
type MN = N
def apply(xs: Vec[A, _0], ys: Vec[A, N]): Out = ys
}
implicit def sPlus[A, M <: Nat, N <: Nat]
(implicit tail: Plus[A, Vec[A, M], Vec[A, N]]) =
new Plus[A, Vec[A, Succ[M]], Vec[A, N]] {
type MN = Succ[tail.MN]
def apply(xs: Vec[A, Succ[M]], ys: Vec[A, N]): Out =
Cons(xs.h, app(xs.t, ys))
}
def app[A, N <: Nat, M <: Nat](xs: Vec[A, N], ys: Vec[A, M])
(implicit plus: Plus[A, Vec[A, N], Vec[A, M]]): plus.Out =
plus(xs, ys)
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment