Go to Qiita Advent Calendar 2024 Top
LoginSignup
27
24

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

@piyo7

コンパイル時に型レベルで整数を四則演算してみた

Last updated at Posted at 2014-10-21

概要

型レベルで整数を表現できると便利です。ええと、整数の型Intではなく。

たとえば固定長配列。長さ3の配列と長さ5の配列を結合すると、要素に依らず長さ8の配列になるはずです。この配列から、13番目の要素を取りだすコードは明らかにバグっているわけです。静的型付け脳としては、こういうは実行時ではなくコンパイル時にエラーにしてほしいですね？
たとえば行列。2x4行列と3x6行列を掛け算するコードは、やはりコンパイルエラーになってほしいですね？
たとえば単位系。3km/sec ÷ 7secという計算結果の値には、自動的にkm/sec^2の型が付いてほしいですね？

これらを実現するためには、型に数値情報を埋め込んで、それをコンパイル時に足し算したり比較する必要があります。
そのように値が入り込んでいる型を、依存型(dependent type)と呼びます。まさにそのためのライブラリ shapeless に自然数を表現する型 Nat があります。ただ整数は見当たらなかったので、色々と参考にしながら四則演算できるようにしてみましたーという記事です。
今回はScalaでやってみます。が、手法自体は他の言語でも使えるものなのだと思います。

型レベル真偽値の論理演算

準備として、まず型レベルで真偽値を表現して、論理演算ができるようにしてみます。
単位系ライブラリ KarolS/units の internal/Bools.scala で使われている手法を、ほぼそのまま使いました。
真を表すクラスTBoolと偽を表すクラスTFalseを作ります。どちらもTBoolトレイトをミックスインしています。

TBool.scala
import scala.language.higherKinds

sealed trait TBool {
  type Not <: TBool
  type And[A <: TBool] <: TBool
  type Or[A <: TBool] <: TBool
  type If[Then <: T, Else <: T, T] <: T
}

class TTrue extends TBool {
  type Not = TFalse
  type And[A <: TBool] = A
  type Or[A <: TBool] = TTrue
  type If[Then <: T, Else <: T, T] = Then
}

class TFalse extends TBool {
  type Not = TTrue
  type And[A <: TBool] = TFalse
  type Or[A <: TBool] = A
  type If[Then <: T, Else <: T, T] = Else
}

object TBool {
  type ![A <: TBool] = A#Not
  type &&[A <: TBool, B <: TBool] = A#And[B]
  type ||[A <: TBool, B <: TBool] = A#Or[B]
  type If[A <: TBool, Then <: T, Else <: T, T] = A#If[Then, Else, T]

  object ToBool {
    def apply[A <: TBool](implicit toBool: ToBool[A]): Boolean = toBool()
  }
  trait ToBool[A <: TBool] {
    def apply(): Boolean
  }
  implicit val toBoolTTrue = new ToBool[TTrue] {
    def apply() = true
  }
  implicit val toBoolTFalse = new ToBool[TFalse] {
    def apply() = false
  }
}

これでOKです。TBoolの派生型をBooleanの値に変換するToBoolを用意したので、簡単に型チェックすることができます。

import TBool._

type Temp0 = ![TTrue]  // TFalse
println(ToBool[Temp0]) // false

type Temp1 = TTrue && TFalse // TFalse
println(ToBool[Temp1])       // false

type Temp2 = TTrue || TFalse // TTrue
println(ToBool[Temp2])       // true

type Temp3 = If[TFalse, TFalse, TTrue, TBool] // TTrue
println(ToBool[Temp3])                        // true

たしかに論理演算ができています。コンパイル時に――！

高カインド型について

import scala.language.higherKinds は書かないと、TBoolのAnd / Or / Ifについて、

higher-kinded type should be enabled by making the implicit value scala.language.higherKinds visible.

とコンパイラが警告を出します。この理由は Scala Standard Library 2.11.2 - language に、

Higher kinded types in Scala lead to a Turing-complete type system, where compiler termination is no longer guaranteed.

と書かれています。デメリットを意識して自己責任で使えよ、ということですね。
とくに今回は、型付け時に計算しようとしているので、うっかり終わらない計算を書くと型付けが停止しなくなってしまいます。実際、実装ミスってコンパイラがスタックオーバーフローしたり、開発環境が固まったりしました。メタプログラミングの代償。。。

型レベル整数の四則演算

型レベルで整数を表現するために、 Practical Church Numerals in Scala で解説されている手法を使います。
たとえば、3を表現する型は次のようになります。いわゆるペアノ数ですね。

type T3 = TSuc[TSuc[TSuc[TZero]]]

-3を表現する型のためには、Successorの代わりにPredecessorを使います。

type T_3 = TPre[TPre[TPre[TZero]]]

それでは実装を貼ります。掛け算と割り算が自力で試行錯誤したところです。

TInt.scala
import scala.language.higherKinds
import TBool._

sealed trait TInt {
  type Neg <: TInt
  type Abs <: TInt
  type Suc <: TInt
  type Pre <: TInt
  type Add[A <: TInt] <: TInt
  type Sub[A <: TInt] = Add[A#Neg]
  type Mul[A <: TInt] <: TInt
  // type Div[A <: TInt] <: TInt
  protected type TSucDivTSuc[A <: TInt] <: TInt
  type Div[A <: TInt] = IfTZeroTSucTPre[
    TZero,
    A#IfTZeroTSucTPre[TZero, TSucDivTSuc[A], TSucDivTSuc[A#Neg]#Neg, TInt],
    A#IfTZeroTSucTPre[TZero, Neg#TSucDivTSuc[A]#Suc#Neg, Neg#TSucDivTSuc[A#Neg]#Suc, TInt],
    TInt]
  type Mod[A <: TInt] <: TInt

  type IfTZeroTSucTPre[TZeroThen <: T, TSucThen <: T, TPreThen <: T, T] <: T
  type IsTZero = IfTZeroTSucTPre[TTrue, TFalse, TFalse, TBool]
  type IsTSuc = IfTZeroTSucTPre[TFalse, TTrue, TFalse, TBool]
  type IsTPre = IfTZeroTSucTPre[TFalse, TFalse, TTrue, TBool]

  type Equal[A <: TInt] = Sub[A]#IsTZero
  type Greater[A <: TInt] = Sub[A]#IsTSuc
  type Less[A <: TInt] = Sub[A]#IsTPre
}

trait TPos extends TInt
trait TNeg extends TInt

class TZero extends TPos with TNeg {
  type Neg = TZero
  type Abs = TZero
  type Suc = TSuc[TZero]
  type Pre = TPre[TZero]
  type Add[A <: TInt] = A
  type Mul[A <: TInt] = TZero
  // type Div[A <: TInt] = TZero
  type TSucDivTSuc[A <: TInt] = TZero
  type Mod[A <: TInt] = TZero

  type IfTZeroTSucTPre[TZeroThen <: T, TSucThen <: T, TPreThen <: T, T] = TZeroThen
}

class TSuc[P <: TPos] extends TPos {
  type Neg = Pre#Neg#Pre
  type Abs = Pre#Suc
  type Suc = TSuc[TSuc[Pre]]
  type Pre = P
  type Add[A <: TInt] = Pre#Add[A]#Suc
  type Mul[A <: TInt] = Pre#Mul[A]#Add[A]
  /*
  type Div[A <: TInt] = A#IfTZeroTSucTPre[
    TZero, // ゼロで割った商はゼロとする
    If[Less[A], TZero, Sub[A]#Div[A]#Suc, TInt],
    If[Less[A#Neg], TZero, Add[A]#Div[A]#Pre, TInt],
    TInt]
  */
  type TSucDivTSuc[A <: TInt] = If[Less[A#Abs], TZero, Sub[A#Abs]#TSucDivTSuc[A]#Suc, TInt]
  type Mod[A <: TInt] = A#IfTZeroTSucTPre[
    TZero, // ゼロで割った余りはゼロとする
    If[Less[A], Pre#Suc, Sub[A]#Mod[A], TInt],
    If[Less[A#Neg], Pre#Suc, Add[A]#Mod[A], TInt],
    TInt]

  type IfTZeroTSucTPre[TZeroThen <: T, TSucThen <: T, TPreThen <: T, T] = TSucThen
}

class TPre[S <: TNeg] extends TNeg {
  type Neg = Suc#Neg#Suc
  type Abs = Neg
  type Suc = S
  type Pre = TPre[TPre[Suc]]
  type Add[A <: TInt] = Suc#Add[A]#Pre
  type Mul[A <: TInt] = Suc#Mul[A]#Sub[A]
  /*
  type Div[A <: TInt] = A#IfTZeroTSucTPre[
    TZero, // ゼロで割った商はゼロとする
    Add[A]#Div[A]#Pre,
    Sub[A]#Div[A]#Suc,
    TInt]
  */
  type TSucDivTSuc[A <: TInt] = TZero
  type Mod[A <: TInt] = A#IfTZeroTSucTPre[
    TZero, // ゼロで割った余りはゼロとする
    Add[A]#Mod[A],
    Sub[A]#Mod[A],
    TInt]

  type IfTZeroTSucTPre[TZeroThen <: T, TSucThen <: T, TPreThen <: T, T] = TPreThen
}

object TInt {
  type +[N1 <: TInt, N2 <: TInt] = N1#Add[N2]
  type -[N1 <: TInt, N2 <: TInt] = N1#Sub[N2]
  type *[N1 <: TInt, N2 <: TInt] = N1#Mul[N2]
  type /[N1 <: TInt, N2 <: TInt] = N1#Div[N2]
  type %[N1 <: TInt, N2 <: TInt] = N1#Mod[N2]

  type ==[A <: TInt, B <: TInt] = A#Equal[B]
  type !=[A <: TInt, B <: TInt] = A#Equal[B]#Not
  type  >[A <: TInt, B <: TInt] = A#Greater[B]
  type <=[A <: TInt, B <: TInt] = A#Greater[B]#Not
  type  <[A <: TInt, B <: TInt] = A#Less[B]
  type >=[A <: TInt, B <: TInt] = A#Less[B]#Not

  object ToInt {
    def apply[N <: TInt](implicit toIntN: ToInt[N]): Int = toIntN()
  }
  trait ToInt[N <: TInt] {
    def apply(): Int
  }
  implicit def toIntTZero = new ToInt[TZero] {
    def apply() = 0
  }
  implicit def toIntTSuc[P <: TPos](implicit toIntP: ToInt[P]) = new ToInt[TSuc[P]] {
    def apply() = toIntP() + 1
  }
  implicit def toIntTPre[S <: TNeg](implicit toIntS: ToInt[S]) = new ToInt[TPre[S]] {
    def apply() = toIntS() - 1
  }

  type T0 = TZero
  type T1 = T0#Suc
  type T2 = T1#Suc
  type T3 = T2#Suc
  type T4 = T3#Suc
  type T5 = T4#Suc
  type T6 = T5#Suc
  type T7 = T6#Suc
  type T8 = T7#Suc
  type T9 = T8#Suc

  type T_1 = T0#Pre
  type T_2 = T_1#Pre
  type T_3 = T_2#Pre
  type T_4 = T_3#Pre
  type T_5 = T_4#Pre
  type T_6 = T_5#Pre
  type T_7 = T_6#Pre
  type T_8 = T_7#Pre
  type T_9 = T_8#Pre
}

うまく出来ているか、TIntの派生型をIntの値に変換するToIntを使って、確かめてみます。

import TInt._

println(ToInt[T8 + T3])   // 11
println(ToInt[T8 + T_3])  // 5
println(ToInt[T_8 + T3])  // -5
println(ToInt[T_8 + T_3]) // -11

println(ToInt[T8 - T3])   // 5
println(ToInt[T8 - T_3])  // 11
println(ToInt[T_8 - T3])  // -11
println(ToInt[T_8 - T_3]) // -5

println(ToInt[T8 * T3])   // 24
println(ToInt[T8 * T_3])  // -24
println(ToInt[T_8 * T3])  // -24
println(ToInt[T_8 * T_3]) // 24

println(ToInt[T8 / T3])   // 2
println(ToInt[T8 / T_3])  // -2
println(ToInt[T_8 / T3])  // -3
println(ToInt[T_8 / T_3]) // 3

println(ToInt[T8 % T3])   // 2
println(ToInt[T8 % T_3])  // 2
println(ToInt[T_8 % T3])  // 1
println(ToInt[T_8 % T_3]) // 1

たしかに四則演算ができています。コンパイル時に――！
以下、余談です。

まず、TIntの演算についてですが、 Typelevel FizzBuzz in Scala のようにimplicit使って外部で実装する手法もあって、そちらの方が筋は良い気がするのですが、計算結果の型そのものを取りだす方法が分からなかったので、TIntトレイトに演算を詰め込みました。

さて、TIntの商を求める割り算Divが、なんだかおかしな実装になっています。これは元々コメントアウトしたコードでいけると思ったのですが、scalacがStackOverflowErrorを吐いてしまいました。おそらくtyperフェーズで、type aliasの再帰呼び出しが循環しているか収束しなくなっているのだと思います。If文で短絡評価できていないのが原因な気はするのですが、このあたりscalacがどういう順番でtype aliasを解決しているか知らないとどうしようもない感じがあって、苦し紛れに色々変形していったら偶然うまくいったのが上記のコードです……。

あと、高カインドなペアノ数で表せる数の上限ですが、 Limits of Nat type in Shapeless によると、

Shapeless 2.0 currently still uses the Church encoding, which will get you to 1,000 or so before the compiler gives up.

だそうです。コンパイル時間の問題もあるので、実用的にはどうなんでしょうね……。
単位系の次元を表す用途の場合は、二桁の整数が必要になることはそうそうないと思うので、適していそうです。

実行環境

build.sbt
name := "type_level_encode"

version := "1.0"

scalaVersion := "2.11.2"
build.properties
sbt.version=0.13.6
27
24
3

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
27
24

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?