型レベル計算(あるいは型レベルプログラミング)は、プログラミング言語の型システムを悪用有効活用して、実行時ではなくコンパイル時に任意の計算を可能にするものです。PureScript v0.12ではこの型レベル計算の機能がさらに強化されており、型レベル計算を活用した実用的なライブラリがすでに幾つか公開されています。
たとえば、purescript-safe-printf は型安全なformat/printfを実現することができます。
format (SProxy :: SProxy "Hello, %s!") "World"
ここで%sというフォーマット文字列がありますが、この個数や型が正しいことをコンパイル時に検証することができます。(SProxy :: SProxy ...という部分がちょっと冗長ですが……たぶんそのうち何らかのショートハンドが用意されるような気がします)
ほかにも、purescript-kushiyaki はURLのパースを行い、パラメータとなる部分を型安全に取り出すことができます。たとえば次のように"/hello/{name}/{age}"のような直感的な文字列でパスを定義してparseURLでパースすると、そのパラメータ部分をnameとageというフィールドを持つレコード型で取り出すことができます。
case parseURL (SProxy :: SProxy "/hello/{name}/{age}") "/hello/Bill/12" of
Left e -> do
log $ "didn't work: " <> e
Right r -> do
assert $ r.name == "Bill"
assert $ r.age == "12"
このとき、変数rの型{ name :: String, age :: String }がどこにも定義されていないことに注目してください。これは、"/hello/{name}/{age}"という部分からコンパイラが自動的に型推論で導き出すのです。
この記事ではPureScriptの型レベル計算を基本的なところから紹介していきたいと思います。
型レベル計算 前知識編
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
型レベル計算をするときにデータのある型を使っても構わないのですが、空の型にしたほうが型レベル計算のための型であるという意図がわかりやすいです。HaskellではEmptyDataDeclsという拡張を使うとこのような空の型の定義できるようになりますが、PureScriptはこの種のコンパイルフラグは一切なく、デフォルトで空のデータ型を定義することができるようになっています。
種
実行時計算ではデータを計算の対象とし、型レベル計算では型を計算の対象とします。そして、実行時計算ではデータを型によって分類しますが、それと同じように型レベル計算では型を種によって分類して扱います。通常の型はTypeという種で表されます。またType -> Typeという種を持つものは型コンストラクタであり、これは実行時計算におけるデータコンストラクタに相当するものであると考えればいいでしょう。他にもSymbolという型レベルの文字列を表す種が存在します。また、::を使うと、実行時の式に型を::を与えるような感じで、型レベルでのそれぞれの計算の対象について、種を示すことができます。
True :: Type
False :: Type
Zero :: Type
Succ :: Type -> Type
Tuple :: Type -> Type -> Type
TypeString :: Type -> Symbol
TypeConcat :: Symbol -> Symbol -> Symbol
"Hello" :: Symbol
Fail :: Symbol -> Type
組み込みの種としてType、Type -> Type、Symbolが存在しますが、それ以外の種を自分で新たに定義することもできます。foreign import kindという予約語のあとに、種の名前を書くだけです。
foreign import kind Nat
foreing import data Zero :: Nat
foreing import data Succ :: Nat -> Nat
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が決まるという型どうしの対応関係を示すものであるようです。
こうしたインスタンス定義では、インスタンスが重複することがよくあります。このときどのインスタンスを優先するかという順序が重要になってきますが、インスタンスチェーンといってインスタンスの順序を明示する方法が導入されました。elseキーワードでインスタンスをつなぐだけです。
class Not a b | a -> b
instance notTrue :: Not True False
else instance notFalse :: Not False True
型レベル計算 応用編
真偽値を用意しました。
data True
data False
これらの真偽値の値をシンボルに変換する型レベルの『関数』のようなクラスを定義します。bにb :: 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 aでTrueにShowを適用した結果をaに代入する、みたいなイメージです。
main :: forall e. Eff (console :: CONSOLE | e) Unit
main = log (reflectSymbol foo)
これでfooの型が型推論されますが、Show True aにはShow True "True"というインスタンスが存在するので、foo :: SProxy "True"であると型推論されます。このfooにreflectSymbolを適用すれば、実行時の値である"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を見つけてaがFalseであると特定します。それから更にShow a bつまりShow False bのインスタンスを探しますが、instance showFalse :: Show False "False"が見つかるのでbが"False"になります。これで、aがFalse、bが"False"のときにこの関数が存在し、その値の型はSProxy "False"であるとわかります。したがって、このbarをreflectSymbolとlogで出力させると、"False"が出力されます。型レベルで定義したTrueをNotで反転し、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
TrueとFalseをXorして、それから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がうまく動いていない気がします。FailにTypeString Trueを与えた時は動くのですが、次のようにreflectSymbolでSProxy (TypeString True)を出力しようとするとエラーになります。
s :: SProxy (TypeString True)
s = SProxy
main :: forall e. Eff (console :: CONSOLE | e) Unit
main = log (reflectSymbol s)
github全体で探してもTypeStringの使用例が非常に稀なので、これはバグである気がします。まともに使っている例もこれがほとんど唯一。よくわかりません。
型レベル計算のためのライブラリとか
- purescript-typelevel 型レベルの自然数と真偽値
- purescript-type-lang 型レベルのラムダ計算
- purescript-type-map 型レベルのマップ
さいごに
ふーん……。型システムだけでこれだけ計算できるのは、すごいといえばすごいですけど、役に立つ場面は相当に限られそうです。ベクトル型に型レベルで要素数を与えてベクトルどうしを加算するときに同じ要素数であることを保証する、みたいな応用例があるみたいですが、他の応用例があんまり思いつきません。 (追記)……と最初は思ったのですが、RowToListという型クラスの実装を転機に、ジャスティンさんを始めいろんな人が型レベル計算を使ったライブラリをどんどん試作していて、実用性が見えてきました。
コンパイル時計算ではその計算の過程をデバッガで追うといったようなことができなくて不便きわまりないですし、マクロやテンプレートメタプログラミング、Templete Haskellとかもそうですが、コンパイル時計算なんて好き好んでやるものじゃないと思います。コンパイル時に何か計算を走らせたかったら、型レベル計算なんてしなくてもビルドスクリプトから普通のプログラムを適当に走らせればいいわけで。ただ、コード生成は型安全でないコーディングをしているようなものですし、コンパイル時により多くの静的な検証を行うには型レベル計算が役に立つのは確かです。でも……他の人が書いてくれたライブラリを使うぶんには嬉しいのですが、型レベル計算を多用したライブラリを自分で書きたいとは思いません。変態性が高すぎます。正直あんまり好きではないです。(追記) 型クラス計算を利用したライブラリを自分で書きたくはありませんが、他の人が作ったライブラリを使うぶんには快適です。どんどん使いましょう。
今回書いたコードはgistに貼り付けておきました。
- https://gist.github.com/aratama/fa1c2b51753c0dd15ff162b36b9bd48d
- https://gist.github.com/aratama/316e796a5792a7da040be6754fc51938
参考文献
-
https://wiki.haskell.org/Type_arithmetic 型レベル計算についての一般的な情報や例は、これが一番参考になりました
-
https://github.com/paf31/24-days-of-purescript-2016/blob/master/11.markdown PureScriptに於ける型レベル計算についてはコレと
-
https://github.com/paf31/24-days-of-purescript-2016/blob/master/21.markdown コレが参考になります
-
https://pursuit.purescript.org/packages/purescript-proxy/1.0.0/docs/Type.Proxy