Skip to content

Instantly share code, notes, and snippets.



Created Sep 4, 2016
What would you like to do?
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
You can’t perform that action at this time.