🐡

Haskellで単純型付きラムダ計算

2023/03/28に公開

Haskell

tech

はじめに

単純型付きラムダ計算をHaskellで実装します。ただし、base typeは自然数で、let式もあります。
この設定でさらに型チェックと評価まであることが少なかったのでこの記事を書いています。

実装

data Exp
    = Var String　-- 変数
    | Lam String Type Exp -- ラムダ
    | Exp :@: Exp -- Apply
    | Exp :+: Exp -- 足し算
    | Int Int -- base type
    | Let String Type Exp Exp -- let式
    deriving (Show, Eq)

data Type
    = TInt　-- base type
    | TArrow Type Type -- 関数型
    deriving (Show, Eq)

type TEnv = [(String, Type)]　-- 型環境
type Env = [(String, Exp)] -- 式環境（？）

そうしたら、型チェックは以下です。

typeOf:: TEnv -> Exp -> Either String Type
typeOf env (Var x) = case lookup x env of
    Just t -> Right t -- 型環境に変数があればその型を返す
    Nothing -> Left $ "Unbound Variable: " ++ x -- なかった場合
typeOf env (Lam x tx e) = do
    ty <- typeOf ((x, tx): env) e -- 例えばfn x: int -> xなら、型環境に(x, TInt)を突っ込み、その上でxの型を評価する。するとTIntなので、結局TArrow TInt TInt
    return $ TArrow tx ty
typeOf env (e1 :@: e2) = do
    ty1 <- typeOf env e1 -- 関数（のはず）の型
    ty2 <- typeOf env e2 -- 引数（のはず）の型
    case ty1 of
        TArrow t1 t2 | t1 == ty2 -> return t2　-- 関数の仮引数の型とあってるかどうか
                        | otherwise -> Left $ "Type Mismatch. The expected argument type is " ++ (show t1) ++ ", but the actual type is " ++ show ty1
        _ -> Left $ "Type Mismatch. You can't apply the non-function " ++ show ty1  -- そうでないならエラー
typeOf env (e1 :+: e2) = do
    ty1 <- typeOf env e1
    ty2 <- typeOf env e2
    case (ty1, ty2) of
        (TInt, TInt) -> return $ TInt -- 両方TIntなら足してTIntになる
        _ -> Left $ "Type Mismatch. You can't add " ++ show ty1 ++ " value and " ++ show ty2　-- そうでないならエラー
typeOf _ (Int _) = Right TInt -- Intの型はTInt
typeOf env (Let x t e1 e2) = do
    ty <- typeOf env e1
    if ty == t then typeOf ((x, t):env) e2 else Left $ "Type Mismatch. You can't substitute " ++ show ty ++ " value to " ++ show t -- letのinの前の代入の部分で型が合わなければエラー

評価は以下。

eval1 :: Env -> Exp -> Either String Exp
eval1 _ (l@(Lam _ _ _)) = Right l
eval1 _ (Int i) = Right $ Int i
eval1 _ ((Int i) :+: (Int j)) = Right . Int $ i + j
eval1 env (e1 :+: e2) = do
    v1 <- eval1 env e1
    v2 <- eval1 env e2
    eval1 env $ v1 :+: v2
eval1 env (Var x) = case lookup x env of
    Just x' -> Right x'
    Nothing -> Left $ "Unbound Variable: " ++ x -- 型チェックが通ればこうはならないはず...
eval1 env (e1 :@: e2) = do
    v1 <- eval1 env e1
    v2 <- eval1 env e2
    apply env v1 v2
    where
        apply :: Env -> Exp -> Exp -> Either String Exp
        apply env_ (Lam x _ e) v = eval1 ((x, v):env_) e -- xにvを代入してeを評価
eval1 env (Let x _ e1 e2) = eval1 ((x, e1):env) e2 -- xにe1を代入してe2を評価

あとは

eval :: Exp -> Either String (Either String Exp)
eval e = eval1 [] e <$ typeOf [] e

で両方で型チェックと評価ができます。

パーサーはまだ雑ですが

import Text.Parsec
import Text.Parsec.String (Parser)

typeParser :: Parser Type
typeParser = try (TArrow <$> typeVarParser <* string "=>" <*> typeParser) <|> typeVarParser

typeVarParser :: Parser Type
typeVarParser = TInt <$ string "int"


termParser :: Parser Exp
termParser = try letinParser <|> try lamParser <|> try appParser <|> try plusParser <|> try numParser <|> varParser


lamParser :: Parser Exp
lamParser = Lam <$ char '(' <* string "fn" <* space <*> many1 letter
            <* spaces <* char ':' <* spaces <*> typeParser <* spaces
            <* string "->" <* spaces <*> termParser <* char ')'

appParser :: Parser Exp
appParser = do
    char '('
    t1 <- termParser
    spaces
    t2 <- termParser
    char ')'
    return $ t1 :@: t2

plusParser :: Parser Exp
plusParser = do
    char '('
    t1 <- termParser
    spaces
    char '+'
    spaces
    t2 <- termParser
    char ')'
    return $ t1 :+: t2

letinParser :: Parser Exp
letinParser = Let <$ string "let" <* spaces <*> many1 letter
            <* spaces <* char ':' <* spaces
            <*> typeParser <* spaces <* char '='
            <* spaces <*> termParser <* spaces <* string "in" <* spaces
            <*> termParser

varParser :: Parser Exp
varParser = Var <$> many1 letter

numParser :: Parser Exp
numParser = (Int . read) <$> many1 digit

parseTerm :: String -> Either ParseError Exp
parseTerm = parse termParser ""

とすると、以下が通ります。

run :: Either ParseError Exp -> Either String (Either String Exp)
run et = case et of
    Right e -> eval e 
    Left e -> Left $ show e

main :: IO ()
main = do
    print . run $ parseTerm "((fn x: int -> x) 0)" -- Right (Right (Int 0))
    print . run $ parseTerm "let x: int = 10 in (x + 1)" -- Right (Right (Int 11))
    print . run $ parseTerm "let y: int=>int = (fn x: int -> (x + 2)) in (y 1)" -- Right (Right (Int 3))

おわりに

この実装は以下のリファレンス
https://gist.github.com/bspaans/476685

とChatGPTの出力を参考にしました。
ChatGPTの出力は不十分でしたが、それでもかなり参考になりました。皆さんもChatGPTでラムダ計算をしましょう。

はじめに

実装

おわりに

Discussion