TaPL 第4章「算術式のML実装」をElmで実装する。
はじめに
「低レイヤを知りたい人のための C コンパイラ作成入門」[1]を読む中で、関数型言語や型システムにも興味が沸いてきたので少し寄り道をして「型システム入門 プログラミング言語と型の理論」TaPL[2]を少し読んでみた。この記事では、TaPL の第 3 章と第 4 章で議論されている「算術式の ML 実装」を Elm で実装を行う。
すでに TaPL 第 4 章を Elm で実装した例は存在するが、勉強を兼ねて自分で実装してみた。
上記の記事では評価規則を Maybe 型で実装しているが、私は Result 型で実装している。それ以外はほぼ変わらない。
算術式の ML
TaPL 第 4 章で取り扱っている算術式の ML とは以下のような言語である。
term = "true"
| "false"
| "if" term "then" term "else" term
| "0"
| "succ" term
| "pred" term
| "iszero" term
この言語をそのまま代数的データ型で表現すると次のようになる。
type Term
= TmTrue
| TmFalse
| TmIf Term Term Term
| TmZero
| TmSucc Term
| TmPred Term
| TmIsZero Term
この表現ではiszero trueやif 1 then true else 2のような評価できない文字列も代数的データ型には変換できてしまう。
構文解析器の実装
はじめに、elm/parser を用いてこの言語の構文解析器を実装する。
termParser : Parser Term
termParser =
let
fromInt : Int -> Term
fromInt n =
if n == 0 then
TmZero
else
TmSucc (fromInt (n - 1))
in
succeed identity
|. spaces
|= oneOf
[ succeed TmTrue
|. symbol "true"
, succeed TmFalse
|. symbol "false"
, succeed TmIf
|. symbol "if"
|= lazy (\_ -> termParser)
|. spaces
|. symbol "then"
|= lazy (\_ -> termParser)
|. spaces
|. symbol "else"
|= lazy (\_ -> termParser)
, int |> Parser.map fromInt
, succeed TmSucc
|. symbol "succ"
|= lazy (\_ -> termParser)
, succeed TmPred
|. symbol "pred"
|= lazy (\_ -> termParser)
, succeed TmIsZero
|. symbol "iszero"
|= lazy (\_ -> termParser)
]
parse : String -> Result (List Parser.DeadEnd) Term
parse =
Parser.run (termParser |. end)
正の整数を入力できるようにした。
評価規則
評価規則の実装した。
eval : Term -> Result String Term
eval t =
let
isNumericVal : Term -> Bool
isNumericVal t1 =
case t1 of
TmZero ->
True
TmSucc t2 ->
isNumericVal t2
_ ->
False
isVal : Term -> Bool
isVal t1 =
case t1 of
TmTrue ->
True
TmFalse ->
True
_ ->
isNumericVal t1
eval1 : Term -> Result String Term
eval1 t_ =
case t_ of
TmIf TmTrue t2 _ ->
Ok t2
TmIf TmFalse _ t3 ->
Ok t3
TmIf t1 t2 t3 ->
eval1 t1 |> Result.map (\t1_ -> TmIf t1_ t2 t3)
TmSucc t1 ->
eval1 t1 |> Result.map TmSucc
TmPred TmZero ->
Ok TmZero
TmPred (TmSucc nv) ->
if isNumericVal nv then
Ok nv
else
eval1 (TmSucc nv) |> Result.map TmPred
TmPred t1 ->
eval1 t1 |> Result.map TmPred
TmIsZero TmZero ->
Ok TmTrue
TmIsZero (TmSucc nv) ->
if isNumericVal nv then
Ok TmFalse
else
Err "No rule applies 2"
TmIsZero t1 ->
eval1 t1 |> Result.map TmIsZero
_ ->
Err "No rule applies 3"
in
if isVal t then
Ok t
else
eval1 t |> Result.andThen eval
前回の算術演算の時は木構造の葉側から順番に評価することで答えが一意に定まったが、一般のプログラミングもそうなのだろうか。プログラムとは葉から評価するべきものであると決まっているのだろうか。この辺がまだ分からない。
もう少し TaPL を読まないと。。。
疑問
前回の算術演算の時にExprをExpr, Mul, Unary, Primaryと 4 つの型に分離できるのではないかと書いた。
今回の「算術式の ML 実装」についても以下のようにtermをnumとboolの二つのデータ型に分離するような設計が可能になる。こうすることで評価できない文字列はパースができなくなるため、評価時のエラーが起こらなくなるというメリットがある。
num = "0"
| "succ" num
| "pred" num
| "nif" bool "then" num "else" num
bool = "true"
| "false"
| "iszero" num
| "bif" bool "then" bool "else" bool
term = num
| bool
if 式は返す型が不明になるのでboolを返すbifとnumを返すnifを定義する必要がある。
これをデータ型に変換すると次のようになる。
type NumVal
= NVZero
| NVSucc NumVal
| NVPred NumVal
| NVIf BoolVal NumVal NumVal
type BoolVal
= BVTrue
| BVFalse
| BVIsZero NumVal
| BVIf BoolVal BoolVal BoolVal
type Term
= Num NumVal
| Bool BoolVal
構文解析器と評価規則は以下のように実装した
構文解析器
numParser : Parser NumVal
numParser =
let
fromInt : Int -> NumVal
fromInt n =
if n == 0 then
NVZero
else
NVSucc (fromInt (n - 1))
in
succeed identity
|= oneOf
[ int
|. spaces
|> Parser.map fromInt
, succeed NVSucc
|. symbol "succ"
|. spaces
|= lazy (\_ -> numParser)
, succeed NVPred
|. symbol "pred"
|. spaces
|= lazy (\_ -> numParser)
, succeed NVIf
|. symbol "nif"
|. spaces
|= lazy (\_ -> boolParser)
|. symbol "then"
|. spaces
|= lazy (\_ -> numParser)
|. symbol "else"
|. spaces
|= lazy (\_ -> numParser)
]
boolParser : Parser BoolVal
boolParser =
succeed identity
|= oneOf
[ succeed BVTrue
|. symbol "true"
|. spaces
, succeed BVFalse
|. symbol "false"
|. spaces
, succeed BVIf
|. symbol "bif"
|. spaces
|= lazy (\_ -> boolParser)
|. symbol "then"
|. spaces
|= lazy (\_ -> boolParser)
|. symbol "else"
|. spaces
|= lazy (\_ -> boolParser)
, succeed BVIsZero
|. symbol "iszero"
|. spaces
|= lazy (\_ -> numParser)
]
termParser : Parser Term
termParser =
succeed identity
|. spaces
|= oneOf
[ numParser |> Parser.map Num
, boolParser |> Parser.map Bool
]
parse : String -> Result (List Parser.DeadEnd) Term
parse =
Parser.run (termParser |. end)
評価規則
eval : Term -> Term
eval t =
let
isNumericVal : Term -> Bool
isNumericVal t1 =
case t1 of
Num NVZero ->
True
Num (NVSucc nv) ->
isVal (Num nv)
_ ->
False
isVal : Term -> Bool
isVal t1 =
case t1 of
Bool BVTrue ->
True
Bool BVFalse ->
True
_ ->
isNumericVal t1
evalNum : NumVal -> NumVal
evalNum n =
case n of
NVZero ->
NVZero
NVSucc nv ->
evalNum nv |> NVSucc
NVPred nv ->
case nv of
NVZero ->
NVZero
NVSucc nv_ ->
nv_
_ ->
evalNum nv |> NVPred
NVIf t1 n1 n2 ->
case t1 of
BVTrue ->
n1
BVFalse ->
n2
_ ->
evalBool t1 |> (\b -> NVIf b n1 n2)
evalBool : BoolVal -> BoolVal
evalBool b =
case b of
BVTrue ->
BVTrue
BVFalse ->
BVFalse
BVIf t1 b1 b2 ->
case t1 of
BVTrue ->
b1
BVFalse ->
b2
_ ->
evalBool t1 |> (\b_ -> BVIf b_ b1 b2)
BVIsZero n ->
case n of
NVZero ->
BVTrue
NVSucc _ ->
BVFalse
_ ->
evalNum n |> BVIsZero
eval1 : Term -> Term
eval1 t1 =
case t1 of
Num n ->
evalNum n |> Num
Bool b ->
evalBool b |> Bool
in
if isVal t then
t
else
eval1 t |> eval
これだけ単純な言語であったとしても型を二つに分離するだけで実装が倍ぐらいになった。型を不用意に分離すると、それだけ実装が面倒になるからやらないのかなと思った。構文解析器が読み取れる文字列の集合と、構文解析器して評価できる文字列の集合を別にする方が実装には優しいっぽい。
その辺からプログラミング言語に型という概念が持ち込まれたのかな。TaPL の続きを読もう。
おわりに
Elm で算術式の ML の実装を行った。実装自体は以前実施されていた方の記事を参考にしたら簡単にできた。elm はパターンガードがないこと[3]から微妙に実装がしづらかった。モナドから逃げてないできちんと Haskell と格闘しようかな。
TaPL を読んでいて「低レイヤを知りたい人のための C コンパイラ作成入門」は非常に教育的にいい教材なんだなぁと思った。数年前に TaPL を読んだ時は数学の証明が多すぎてよく分からなかったが、C コンパイラを作る中でだんだんと構文解析や型の付けやアセンブラへの変換が身体に染み付いてくるので、その経験が TaPL 読解には非常に役に立った。そして面白くなった。
最後に書いた疑問点は今後 TaPL を読みながら理解したい。
Discussion