Go to Qiita Advent Calendar 2024 Top
LoginSignup
19
10

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.

@hiruberuto

PureScript型レベル計算入門

Last updated at Posted at 2016-12-13

型レベル計算(あるいは型レベルプログラミング)は、プログラミング言語の型システムを悪用有効活用して、実行時ではなくコンパイル時に任意の計算を可能にするものです。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
実行時計算のためのの2要素タプル
data Tuple a b = Tuple a b

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

型レベル計算のための真偽値
data True

data False
型レベル計算のための自然数
data Zero

data Succ a
型レベル計算のためのの2要素タプル
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の使用例が非常に稀なので、これはバグである気がします。まともに使っている例もこれがほとんど唯一。よくわかりません。

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

さいごに

ふーん……。型システムだけでこれだけ計算できるのは、すごいといえばすごいですけど、役に立つ場面は相当に限られそうです。ベクトル型に型レベルで要素数を与えてベクトルどうしを加算するときに同じ要素数であることを保証する、みたいな応用例があるみたいですが、他の応用例があんまり思いつきません。 (追記)……と最初は思ったのですが、RowToListという型クラスの実装を転機に、ジャスティンさんを始めいろんな人が型レベル計算を使ったライブラリをどんどん試作していて、実用性が見えてきました。

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

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

参考文献

19
10
0

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
19
10

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?