Admittedly something small.
2016年12月13日

PureScriptで型レベル計算ドリル

Haskell purescript


型レベル計算は、プログラミング言語の型システムを悪用有効活用して、実行時ではなくコンパイル時に任意の計算を可能にするものです。型レベル計算はチューリング完全であり、理論上どんな計算でもできることが知られていて、うまく使うといろいろと便利なことができるようです。私も練習してみます。言語はPureScriptですが、Haskellでも事情はだいたい同じだと思います。

型レベル計算 基礎編

EmptyDataDecls

代数的データ型では通常、=のあとに|で区切ってその型に含まれるデータを列挙して定義します。

data Bool = True | False
data Nat = Zero | Succ Nat
data Tuple a b = Tuple a b

実行時計算がデータを計算の対象にするのに対して、型レベル計算では型そのものが計算の対象になります。必要なのは型だけであってデータは不要ですから、代数的データ型では何もデータのない型を定義することもできるようになっています。型レベルの真偽値や自然数などを定義してみます。

data True

data False
data Zero

data Succ a
data Tuple a b

型レベル計算をするときにデータのある型を使っても構わないのですが、空の型にしたほうが型レベル計算のための型であるという意図がわかりやすいです。

実行時計算ではデータを計算の対象とし、型レベル計算では型を計算の対象とします。そして、実行時計算ではデータを型によって分類しますが、それと同じように型レベル計算では型をによって分類して扱います。通常の型は*という種で表されます。また* -> *という種を持つものは型コンストラクタであり、これは実行時計算におけるデータコンストラクタに相当するものであると考えればいいでしょう。他にもSymbolという型レベルの文字列を表す種が存在します。また、::を使うと、実行時の式に型を::を与えるような感じで、型レベルでのそれぞれの計算の対象について、種を示すことができます。

True :: *

False :: *

Zero :: *

Succ :: * -> *

Tuple :: * -> * -> *

TypeString :: * -> Symbol

TypeConcat :: Symbol -> Symbol -> Symbol

"Hello" :: Symbol

Fail :: Symbol -> *

組み込みの種として** -> *Symbolが存在しますが、それ以外の種を自分で新たに定義することはできません。種*を持つ型はみんなひとくくりです。と思ったら、種のユーザ定義まで導入を検討されているみたいです。

type

実行時計算で変数を使って値に名前を付けられるように、型レベル計算ではtypeを使って型に名前をつけることができます。

one :: Nat
one = Succ Zero

two :: Nat
two = Succ One

three :: Nat
three = Succ Two
type One = Succ Zero

type Two = Succ One

type Three = Succ Two

Symbol

Symbolは言語に組み込みの種で、型レベルの文字列を表しています。型のなかに置かれた文字列リテラルがシンボルになります。

type Foo = "Foo" :: Symbol

TypeString

組み込みの型コンストラクタTypeStringを使うと、型からシンボルを作り出すことができます。

TypeString :: * -> Symbol

TypeConcat

TypeConcatは組み込みの型コンストラクタで、シンボル同士を連結することができます。型レベル計算に於ける文字列の連結です。

TypeConcat :: Symbol -> Symbol -> Symbol

型コンストラクタに別名をつけることもできますので、実行時計算での文字列の連結に使う<>と同じように、型レベルでの文字列結合演算子として<>を定義してみます。

infixl 6 type TypeConcat as <>

これを使うと、任意のシンボル同士を連結することができます。

type HelloWorld = "Hello" <> "World"

Proxy

Proxyを使うと、データのないデータ型に代理の実行時データを与えて、実行時の計算に使うことができます。

data Proxy a = Proxy

Proxy aにはaという型変数があるのに、データ自体にはaのデータを持っていません。このように、型変数があるのにその型変数が表すデータを実際には持っていないようなデータ型をPhantom Typeといいます。データコンストラクタProxyは実際にはaのデータを受け取るわけではないので、データの存在しないZeroのような型に対してもProxy Zeroという型を持つデータを作り出せます。

zero :: Proxy Zero
zero = Proxy

Zeroの型を持つデータは存在しませんが、Proxy Zeroのデータならいつでも作ることができるというわけです。具体的な応用については、このあとの実践編をごらんください。

SProxy

Proxyは汎用のプロキシですが、SProxyというシンボル専用のプロキシもあります。このSProxyなデータを用意してそれにreflectSymbolという関数を適用すると、任意のシンボルから実行時の文字列データを取得することができます。例えば次のようにすれば、型レベル計算でシンボル"foo"とシンボル"bar"を<>演算子で連結し、そのシンボルをSProxyで仮の実行時の肉体を与え、それにreflectSymbolを適用することで、型レベルで計算した"foobar"という文字列をlogで実行時に出力できます。

foobar :: SProxy ("foo" <> "bar")
foobar = SProxy

main :: forall e. Eff (console :: CONSOLE | e) Unit
main = log (reflectSymbol foobar)

Fail

Failは言語に組み込みの型コンストラクタで、シンボルを受け取って型を返します。しかしこの型はコンパイラによって特別に扱われ、コンパイルしようとするとエラーになります。

Fail :: Symbol -> *

要するに型レベル計算におけるエラー表現です。コンパイルエラーになったときのメッセージをカスタマイズするのに使えるようです。

型レベル計算における関数

型レベル計算で、型を別の型に対応させるには、型クラスを使えばいいようです。たとえば、

class Not a b | a -> b
instance notTrue :: Not True False
instance notFalse :: Not False True

このa -> bというのがfunctional dependencyというもので、型aがわかれば型bが決まるという型どうしの対応関係を示すものであるようです。

型レベル計算 実践編

真偽値を用意しました。

data True

data False

これらの真偽値の値をシンボルに変換する型レベルの『関数』のようなクラスを定義します。bb :: Symbolという制約を加えるのと、a -> bという対応を書くのがポイント。

class Show a (b :: Symbol) | a -> b

先ほどの真偽値をそれぞれシンボルに対応させるインスタンスを書くことで、『型レベルの関数』を実装します。

instance showTrue :: Show True "True"
instance showFalse :: Show False "False"

この『型レベルの関数』を適用するには、それを制約として持つような型を定義します。この後で

foo :: forall a. Show True a => SProxy a
foo = SProxy

forall aで変数aを定義し、Show True aTrueShowを適用した結果をaに代入する、みたいなイメージです。

main :: forall e. Eff (console :: CONSOLE | e) Unit
main = log (reflectSymbol foo)

これでfooの型が型推論されますが、Show True aにはShow True "True"というインスタンスが存在するので、foo :: SProxy "True"であると型推論されます。このfooreflectSymbolを適用すれば、実行時の値である"True" :: Stringが取得できるので、これをlogで実行時に出力することができます。

こんどは真偽値を反転させてから出力してみます。Not :: * -> *を定義して、それぞれの値を反転させて対応させるようにインスタンスを書きます。

class Not a b | a -> b
instance notTrue :: Not True False
instance notFalse :: Not False True

さっきのShowと組み合わせてみます。

bar :: forall a b. (Not True a, Show a b) => SProxy b
bar = SProxy

これがコンパイルされると、まず型システムがNot True aのインスタンスがないか探し、instance notTrue :: Not True Falseを見つけてaFalseであると特定します。それから更にShow a bつまりShow False bのインスタンスを探しますが、instance showFalse :: Show False "False"が見つかるのでb"False"になります。これで、aFalseb"False"のときにこの関数が存在し、その値の型はSProxy "False"であるとわかります。したがって、このbarreflectSymbollogで出力させると、"False"が出力されます。型レベルで定義したTrueNotで反転し、Showでシンボルに変換するという計算ができました。

さらにXorを実装してみます。

class Xor a b c | a b -> c
instance xorTT :: Xor True True False
instance xorFT :: Xor False True True
instance xorTF :: Xor True False True
instance xorFF :: Xor False False False

せっかくなので、さっきのNotと組み合わせてみます。

xor :: forall a b c. (Xor True False a, Not a b, Show b c) => SProxy c
xor = SProxy

TrueFalseXorして、それからNotしたものは、Falseであるとわかりました。ふむふむ。

自然数も扱ってみます。Type_arithmeticで紹介されている方法をすこし改造して使いました。

numPred :: forall a. Proxy (Succ a) -> Proxy a
numPred = const Proxy

class Number a where
    numValue :: Proxy a -> Int

instance numberZero :: Number Zero where
    numValue = const 0

instance numberSucc :: Number x => Number (Succ x) where
    numValue x = numValue (numPred x) + 1

three :: Proxy Three
three = Proxy

main :: forall e. Eff (console :: CONSOLE | e) Unit
main = logShow (numValue three)

これで3が出力されます。Succ aからそれが表す実行時の数値を計算するには、Proxy (Succ a)をかわりに使って計算するわけです。ややこしいですね。リストとかもやろうかと思いましたが、めんどうくさくなりました。

TypeStringがうまく動いていない気がします。FailTypeString Trueを与えた時は動くのですが、次のようにreflectSymbolSProxy (TypeString True)を出力しようとするとエラーになります。

s :: SProxy (TypeString True)
s = SProxy

main :: forall e. Eff (console :: CONSOLE | e) Unit
main = log (reflectSymbol s)

github全体で探してもTypeStringの使用例が非常に稀なので、これはバグである気がします。まともに使っている例もこれがほとんど唯一。よくわかりません。

型レベル計算のためのライブラリとか

さいごに

ふーん……。型システムだけでこれだけ計算できるのは、すごいといえばすごいですけど、役に立つ場面は相当に限られそうです。ベクトル型に型レベルで要素数を与えてベクトルどうしを加算するときに同じ要素数であることを保証する、みたいな応用例があるみたいですが、他の応用例があんまり思いつきません。

コンパイル時計算ではその計算の過程をデバッガで追うといったようなことができなくて不便きわまりないですし、マクロやテンプレートメタプログラミング、Templete Haskellとかもそうですが、コンパイル時計算なんて好き好んでやるものじゃないと思います。コンパイル時に何か計算を走らせたかったら、型レベル計算なんてしなくてもビルドスクリプトから普通のプログラムを適当に走らせればいいわけで。ただ、コード生成は型安全でないコーディングをしているようなものですし、コンパイル時により多くの静的な検証を行うには型レベル計算が役に立つのは確かです。でも……他の人が書いてくれたライブラリを使うぶんには嬉しいのですが、型レベル計算を多用したライブラリを自分で書きたいとは思いません。変態性が高すぎます。正直あんまり好きではないです。

今回書いたコードはgistに貼り付けておきました。

参考文献


このエントリーをはてなブックマークに追加