🧩

Haskellの型パズルで作るMini Interpreter

2021/02/21に公開

「効率よく素数を計算するプログラムを作る課題」を出したら「コンパイル時に素数判定を行うプログラムが優勝した」なんて話がありますが[要出典]、今回は型レベル文字列で数式を渡すとコンパイル時に計算を行ってくれる型レベルインタプリタを作ってみようと思います^[1]

動作イメージはこんな感じ

> :kind! Calc "(1 + 1) * (2 + 0) + 10"
Calc "(1 + 1) * (2 + 0) + 10" :: Nat
= 14

GHCiで :kind! を使うと与えられた型の型シノニムや型族による変換を評価してくれます。つまり上記のプログラムは数式を表す型レベル文字列を評価してNatカインドの14という型に評価されているというわけです。

元ネタはQuramyさんのこの記事です

今朝この記事を引用した友人が

「文字列型を型レベルで扱える似たような機能って他の静的型付け言語にもあるんでしょうか？」

と質問していたので Haskellでも書けるよおおおと答えるために書いた記事 でもあります

Haskellの型レベル文字列

まず最初にGHC特有の面倒くさい話があります

GHCには DataKinds という言語拡張があり、これを使えば値を型に、型をカインドに持ち上げてくれるのですが、Haskellの文字列リテラルを型の部分に書いた場合、GHCはこれをStringカインドではなくSymbolカインドに推論します

これの何が問題かというと、Stringは[Char]というリストの型シノニムになっていたのでリストのパターンマッチが使えて便利だったのですが、Symbolカインドにはそのような機能は無く、パターンマッチによって処理を切り替えるような型族の実装を書くのが困難になります

この問題を解決するために ToList というSymbolを一文字ずつのSymbolのリスト[Symbol]に変換する型族を実装しているsymbolsというライブラリがあるので今回はそれを使って実装を進めることにしましょう。詳しくは以下の記事で解説されています

ちなみに "The Char kind" という GHC Proposal があって、これは型レベルの文字リテラルをCharカインドに推論しようというものなのですが、この Proposal によって

type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol)

という型族も追加されるので Symbol のパターンマッチは幾分かやりやすくなるはずです。すでに実装されてマージされているので近いうちに使えるようになるでしょう

逆ポーランド記法の評価

まず手始めにインタプリタを実装するのが簡単な逆ポーランド記法（Reverse Polish Notation, RPN）で与えられた数式を評価する型族を作ります

type family EvalRPN (sym :: Symbol) :: Nat where
  EvalRPN sym = EvalRPN1 '[] (ToList sym)

type family EvalRPN1 (stack :: [Nat]) (syms :: [Symbol]) :: Nat where
  EvalRPN1      (x ': stack)          '[]  = x
  EvalRPN1            stack  (" " ': syms) = EvalRPN1                 stack  syms
  EvalRPN1 (x ': y ': stack) ("+" ': syms) = EvalRPN1       (x + y ': stack) syms
  EvalRPN1 (x ': y ': stack) ("*" ': syms) = EvalRPN1       (x * y ': stack) syms
  EvalRPN1            stack  (sym ': syms) = EvalRPN1 (ReadNat sym ': stack) syms

ReadNatはsymbolsライブラリで提供されているSymbolをNatに変換する型族です

早速GHCiで評価してみましょう

> :kind! EvalRPN "1 1 + 2 *"
EvalRPN "1 1 + 2 *" :: Nat
= 4

上手く動いていますね👏

トークナイザの実装

EvalRPNは一桁の数字しか扱えないという欠点があるので、複数桁の数字も一つのトークンとして扱うようなトークナイザを実装してみましょう。ついでに不要な空白文字も取り除きます

実装する前に型レベルリストの並び順を反転するための型族を用意しておきましょう

type family Reverse (xs :: [k]) :: [k] where
  Reverse xs = Reverse1 '[] xs

type family Reverse1 (reversed :: [k]) (xs :: [k]) where
  Reverse1 reversed      '[]  = reversed
  Reverse1 reversed (x ': xs) = Reverse1 (x ': reversed) xs

これを使ってSymbolをトークンの列[Symbol]に変換するトークナイザを実装していきます

type family Tokenize (sym :: Symbol) :: [Symbol] where
  Tokenize sym = Tokenize1 '[] "" (ToList sym)

type family Tokenize1 (tokens :: [Symbol]) (digits :: Symbol) (syms :: [Symbol]) :: [Symbol] where
  Tokenize1 tokens digits '[]           = Reverse   (If (digits == "")         tokens         (digits ': tokens))
  Tokenize1 tokens digits (" " ': syms) = Tokenize1 (If (digits == "")         tokens         (digits ': tokens)) "" syms
  Tokenize1 tokens digits ("+" ': syms) = Tokenize1 (If (digits == "") ("+" ': tokens) ("+" ': digits ': tokens)) "" syms
  Tokenize1 tokens digits ("*" ': syms) = Tokenize1 (If (digits == "") ("*" ': tokens) ("*" ': digits ': tokens)) "" syms
  Tokenize1 tokens digits ("(" ': syms) = Tokenize1 (If (digits == "") ("(" ': tokens) ("(" ': digits ': tokens)) "" syms
  Tokenize1 tokens digits (")" ': syms) = Tokenize1 (If (digits == "") (")" ': tokens) (")" ': digits ': tokens)) "" syms
  Tokenize1 tokens digits (sym ': syms) = Tokenize1 tokens (AppendSymbol digits sym) syms

型族Ifと(==)はそれぞれbaseのData.Type.Bool, Data.Type.Equalityに定義されているものです。後々のために括弧()にも対応しました

実際に使ってみましょう

> :kind! Tokenize "(1 + 20) * 300"
Tokenize "(1 + 20) * 300" :: [Symbol]
= '["(", "1", "+", "20", ")", "*", "300"]

期待通りに動いてますね 👏

操車場アルゴリズム

通常の数式を逆ポーランド記法に変換するアルゴリズムとして操車場アルゴリズムというものがあります

これは前述の例の["(", "1", "+", "20", ")", "*", "300"]というようなトークン列が与えられた時に以下のルールに従って順々にトークンを並び替えていくアルゴリズムです。このアルゴリズムには入力のトークン列と演算子を一時的に入れておくスタックと出力用のスタックが登場します

トークン	操作
数値	出力用のスタックにプッシュする
演算子`o1`	演算子用のトップにある演算子`o2`が`o1`より優先順位が等しいか低い間、演算子用のスタックからポップして出力用のスタックにプッシュする最後、`o1`を演算子用のスタックにプッシュする
左括弧	演算子用のスタックにプッシュする
右括弧	演算子用のスタックのトップにあるトークンが左括弧になるまでスタックからポップし、出力用のスタックにプッシュする最後、左括弧を演算子用のスタックからポップし、そのまま捨てる
読み込むトークンがなくなった場合	演算子用のスタックにあるトークンを全てポップし出力用のスタックにプッシュする

（結合順序やエラーハンドリングを無視したのでWikipediaの説明より幾分か簡単になっています）

このルールに従ってトークン列を処理する型族を実装してみましょう

type family ShuntingYard (xs :: [Symbol]) :: [Symbol] where
  ShuntingYard xs = ShuntingYard1 '[] '[] xs

type family ShuntingYard1 (output :: [Symbol]) (operators :: [Symbol]) (input :: [Symbol]) :: [Symbol] where
  ShuntingYard1 output '[]                '[]            = Reverse output
  ShuntingYard1 output (sym ': operators) '[]            = ShuntingYard1 (sym ': output)         operators          '[]
  ShuntingYard1 output ("*" ': operators) ("+" ': input) = ShuntingYard1 ("*" ': output)         operators  ("+" ': input)
  ShuntingYard1 output ("+" ': operators) ("+" ': input) = ShuntingYard1 ("+" ': output)         operators  ("+" ': input)
  ShuntingYard1 output         operators  ("+" ': input) = ShuntingYard1         output  ("+" ': operators)         input
  ShuntingYard1 output         operators  ("*" ': input) = ShuntingYard1         output  ("*" ': operators)         input
  ShuntingYard1 output         operators  ("(" ': input) = ShuntingYard1         output  ("(" ': operators)         input
  ShuntingYard1 output ("(" ': operators) (")" ': input) = ShuntingYard1         output          operators          input
  ShuntingYard1 output (sym ': operators) (")" ': input) = ShuntingYard1 (sym ': output)         operators  (")" ': input)
  ShuntingYard1 output         operators  (sym ': input) = ShuntingYard1 (sym ': output)         operators          input

演算子が２つしか無いので簡単に優先順位をパターンマッチの評価順序で表現したので（力技！）、パターンマッチによる分岐が多くなってしまいましたが問題ないでしょう。ShuntingYardによって数式がポーランド記法に変換できていることを確認してみましょう

> :kind! ShuntingYard '["(", "1", "+", "20", ")", "*", "300"]
ShuntingYard '["(", "1", "+", "20", ")", "*", "300"] :: [Symbol]
= '["1", "20", "+", "300", "*"]

想定通りですね👏

仕上げ

最後に、トークナイザ、操車場アルゴリズム、逆ポーランド記法の評価を組み合わせれば完成です

最初に定義したEvalRPNをトークナイザの導入に合わせて少し書き直しておきましょう

type family EvalRPN (syms :: [Symbol]) :: Nat where
  EvalRPN syms = EvalRPN1 '[] syms

type family EvalRPN1 (stack :: [Nat]) (syms :: [Symbol]) :: Nat where
  EvalRPN1      (x ': stack)          '[]  = x
  EvalRPN1 (x ': y ': stack) ("+" ': syms) = EvalRPN1       (x + y ': stack) syms
  EvalRPN1 (x ': y ': stack) ("*" ': syms) = EvalRPN1       (x * y ': stack) syms
  EvalRPN1            stack  (sym ': syms) = EvalRPN1 (ReadNat sym ': stack) syms

入力として最初から[Symbol]を想定しており、空白文字の処理が無くなっているところが変わっています

これらを組み合わせると欲しかったMini Interpreterの完成です！

type Calc xs = EvalRPN (ShuntingYard (Tokenize xs))

実際に使ってみましょう

> :kind! Calc "(1 + 20) * 300"
Calc "(1 + 20) * 300" :: Nat
= 6300

> :kind! Calc "(1 + 1) * (2 + 0) + 10"
Calc "(1 + 1) * (2 + 0) + 10" :: Nat
= 14

ちゃんと型レベル文字列の数式を計算できていますね👏

最後に実装したコードの全体を載せておきます

＼読んでいただきありがとうございました！／
この記事が面白かったらいいね♡ をいただけると嬉しいです☺️
バッジを贈っていただければ次の記事を書くため励みになります🙌

脚注

Haskellでコンパイル時に素数判定を行う方法が解説されている記事はこちら "コンパイル時に素数判定を行ってみた - Qiita" ↩︎

Haskellの型レベル文字列

逆ポーランド記法の評価

トークナイザの実装

操車場アルゴリズム

仕上げ

Discussion