実行時にしか解らないベクトルの長さをパス依存型で型安全に扱う例

gistfile1.scala

object Vec {
  object NotEq {
    class =!=[A, B]
    implicit def aNeqB[A, B] = new =!=[A, B]
    implicit def aNeqA1[A] = new =!=[A, A]
    implicit def aNeqA2[A] = new =!=[A, A]
  }
  
  object Nat {
    sealed trait Nat {
      type Prev <: Nat
      type Max[N <: Nat] <: Nat
    }
    sealed trait Z extends Nat {
      type Prev = Z
      type Max[N <: Nat] = N
    }
    sealed trait S[N <: Nat] extends Nat {
      type Prev = N
      type Max[M <: Nat] = S[N#Max[M#Prev]]
    }
  }

  class Wrap[A](xs: List[A]) { self =>
    import NotEq._
    import Nat._
    
    sealed abstract class Vec[+A, N <: Nat] {
      def head(implicit ev: N =!= Z): A
      def tail(implicit ev: N =!= Z): Vec[A, N#Prev]
      def length: Int =
        (this: Vec[A, _]) match {
          case Nil(xs) => xs.length
          case _ :: tl => 1 + tl.length
        }
      
      def toList: List[A] = {
        (this: Vec[A, _]) match {
          case Nil(xs) => xs
          case hd :: tl => hd :: tl.toList
        }
      }
      
      def sameLength[B, M <: Nat](vec: Wrap[B]#Vec[B, M]): Option[Vec[B, N#Max[M]]] = {
        if (vec.length == length) Some(Nil[B, N#Max[M]](vec.toList))
        else None
      }
      
      def ::[T >: A](x: T): Vec[T, S[N]] = self.::(x, this)

      def innerProd[T >: A](vec: Vec[T, N])(implicit ev: Numeric[T]): T =
        (vec.toList, toList).zipped.map{case (a, b) => ev.times(a, b)}.sum
    }
    case class Nil[A, N <: Nat](xs: List[A]) extends Vec[A, N] {
      def head(implicit ev: N =!= Z): A = xs.head
      def tail(implicit ev: N =!= Z): Vec[A, N#Prev] = Nil[A, N#Prev](xs.tail)
    }
    case class ::[A, N <: Nat](hd: A, tl: Vec[A, N]) extends Vec[A, S[N]] {
      def head(implicit ev: S[N] =!= Z): A = hd
      def tail(implicit ev: S[N] =!= Z): Vec[A, S[N]#Prev] = tl
    }
    
    val value = Nil[A, Z](xs)
  }
}

object Test extends App {
  import Vec._
  
  val w1 = new Wrap(List(4, 5, 6))
  val w2 = new Wrap(List(1, 2, 3, 4, 5, 6))

  //ここでw1.valueに三つの要素を追加している。
  val vec1 = 1 :: 2 :: 3 :: w1.value
  //なのでvec1には少なくとも三つの要素があることが、コンパイル時にわかる。

  //vec1.innerProd(w2.value) //まだ同じ長さだと確かめられていないのでコンパイルエラー。

  vec1.sameLength(w2.value) match {
    case Some(vec2) =>
      //vec2はvec1と同じ長さだと確かめられたので、三回までtailをチェインさせても問題ない。
      vec2.tail.tail.tail //これはコンパイルできる。
      //vec2.tail.tail.tail.tail //しかしこれは四回目のtailがあり安全ではないのでコンパイルできない。

      println((0 :: vec1).innerProd(0 :: vec2))
      //println(vec1.tail.tail.innerProd(vec2.tail)) //コンパイルエラー。
      //println((0 :: vec1).innerProd(vec2)) //コンパイルエラー。

    case None =>
  }
}