UTLC++

UTLC++.hs

{-# LANGUAGE LambdaCase, OverloadedStrings #-}

import Data.String

type Name = String

data Expr
    = V Name
    | Lam Name Expr
    | Either Bool Expr -- "False = Left, True = Right"
    | Both (Expr, Expr)
    | Expr :$ Expr
    | Proj Bool Expr -- "False = fst, True = snd"
    | Match Expr Name (Expr, Expr) -- same name in both arms for simplicity
    deriving Show

evaluate :: [(String, Maybe Expr)] -> Expr -> Expr
evaluate env = let eval = evaluate env in \case
    V name
        -> maybe (error name) (maybe (V name) id) (lookup name env)

    Lam name expr
        -> Lam name (evaluate ((name, Nothing) : env) expr)

    Either bool expr
        -> Either bool (eval expr)

    Both (expr1, expr2)
        -> Both (eval expr1, eval expr2)

    (Lam name expr1) :$ expr2
        -> evaluate ((name, Just (eval expr2)) : env) expr1

    Proj bool (Both (expr1, expr2))
        -> eval (if bool then expr2 else expr1)

    Match (Either bool expr1) name (expr2, expr3)
        -> evaluate ((name, Just (eval expr1)) : env) (if bool then expr3 else expr2)

    Both (expr1, expr2) :$ expr3
        -> Both (eval (expr1 :$ expr3), eval (expr2 :$ expr3))

    Proj bool (Lam name expr)
        -> eval $ Lam name (Proj bool expr)

    Either bool expr1 :$ expr2
        -> Either bool (eval (expr1 :$ expr2))

    Match (Lam name1 expr1) name2 (expr2, expr3)
        -> eval $ Lam name1 (Match expr1 name2 (expr2, expr3)) -- shadowing??

    Proj bool1 (Either bool2 expr)
        -> Either bool2 (eval (Proj bool1 expr))

    Match (Both (expr1, expr2)) name (expr3, expr4)
        -> Both (eval $ Match expr1 name (expr3, expr4), eval $ Match expr2 name (expr3, expr4))

    expr1 :$ expr2
        -> let e = eval expr1 in if neutral env e then e :$ (eval expr2) else eval (e :$ expr2)

    Proj bool expr
        -> let e = eval expr in if neutral env e then Proj bool e else eval (Proj bool e)

    Match expr1 name (expr2, expr3)
        -> let e = eval expr1 in if neutral env e then Match e name (evaluate ((name, Nothing) : env) expr2, evaluate ((name, Nothing) : env) expr3) else eval (Match e name (expr2, expr3))

neutral :: [(Name, Maybe Expr)] -> Expr -> Bool
neutral env = \case
    V name         -> case lookup name env of Nothing -> error name; Just Nothing -> True; Just (Just _) -> False
    expr :$ _      -> neutral env expr
    Proj _ expr    -> neutral env expr
    Match expr _ _ -> neutral env expr
    _              -> False

eval :: Expr -> Expr
eval = evaluate []

instance IsString Expr where
    fromString = V

main = print example >> print (eval example)

example = Both (Lam "a" "a", Lam "b" "b") :$ Lam "a" (Lam "b" "a")