型無し算術式の実装

型システム入門の第4章　算術式の実装がOCamlで書かれていたので、勉強がてらHaskellで書いてみました。

import Data.Maybe (fromJust)

data Term = T_TRUE | T_FALSE | T_ZERO | T_SUCC Term | T_PRED Term | T_ISZERO Term | T_IF Term Term Term deriving (Eq, Show)

eval :: Term -> Maybe Term
eval t | isv t = Just t
       | otherwise = step t >>= eval

step :: Term -> Maybe Term
step (T_IF T_TRUE t2 t3) = Just t2
step (T_IF T_FALSE t2 t3) = Just t3
step (T_IF t1 t2 t3) = if t1' /= Nothing then Just (T_IF (fromJust t1') t2 t3) else Nothing where t1' = step t1
step (T_SUCC t1) = if t1' /= Nothing then Just (T_SUCC (fromJust t1')) else Nothing where t1' = step t1
step (T_PRED T_ZERO) = Just T_ZERO
step (T_PRED (T_SUCC t1)) | isn t1 = Just t1
step (T_PRED t1) = if t1' /= Nothing then Just (T_PRED (fromJust t1')) else Nothing where t1' = step t1
step (T_ISZERO T_ZERO) = Just T_TRUE
step (T_ISZERO (T_SUCC t1)) | isn t1 = Just T_FALSE
step (T_ISZERO t1) = if t1' /= Nothing then Just (T_ISZERO (fromJust t1')) else Nothing where t1' = step t1
step _ = Nothing

isn :: Term -> Bool
isn T_ZERO = True
isn (T_SUCC x) = isn x
isn _ = False

isv :: Term -> Bool
isv T_TRUE = True
isv T_FALSE = True
isv x | isn x = True
isv _ = False

OCamlみたいにパターンマッチ使ってます。
実行時エラーを考慮して、計算結果にはMaybeモナドを使っています。

評価関数evalを使ってみると、こんな感じになります。

*Main> eval $ T_IF (T_ISZERO T_ZERO) T_FALSE T_ZERO
Just T_FALSE

*Main> eval $ T_IF (T_ISZERO (T_SUCC T_ZERO)) (T_SUCC $ T_SUCC $ T_SUCC $ T_ZERO) T_ZERO
Just T_ZERO

*Main> eval $ T_IF T_ZERO T_TRUE T_FALSE
Nothing