I’m working on a lambda calculus interpreter in Haskell, and I need help implementing semantic rules for sum types. Below is a simplified version of my code with lexer, interpreter, and typechecker modules.
Lexer.hs
module Lexer where
import Data.Char
data Ty = TBool
| TNum
| TFun Ty Ty
| TSum Ty Ty
deriving (Show, Eq)
data Expr = BTrue
| BFalse
| Num Int
| Add Expr Expr
| And Expr Expr
| If Expr Expr Expr
| Var String
| Lam String Ty Expr
| App Expr Expr
| Paren Expr
| Eq Expr Expr
| Inl Expr
| Inr Expr
| Case Expr Expr Expr
deriving (Show, Eq)
data Token = TokenTrue
| TokenFalse
| TokenNum Int
| TokenAdd
| TokenAnd
| TokenIf
| TokenThen
| TokenElse
| TokenVar String
| TokenLam
| TokenColon
| TokenArrow
| TokenLParen
| TokenRParen
| TokenBoolean
| TokenNumber
| TokenEq
| TokenInl
| TokenInr
| TokenCase
| TokenBar
| TokenOf
deriving Show
isToken :: Char -> Bool
isToken c = elem c "->&|="
lexer :: String -> [Token]
lexer [] = []
lexer ('+':cs) = TokenAdd : lexer cs
lexer ('\':cs) = TokenLam : lexer cs
lexer (':':cs) = TokenColon : lexer cs
lexer ('(':cs) = TokenLParen : lexer cs
lexer (')':cs) = TokenRParen : lexer cs
lexer (c:cs) | isSpace c = lexer cs
| isDigit c = lexNum (c:cs)
| isAlpha c = lexKW (c:cs)
| isToken c = lexSymbol (c:cs)
lexer _ = error "Lexical error: caracter inválido!"
lexNum :: String -> [Token]
lexNum cs = case span isDigit cs of
(num, rest) -> TokenNum (read num) : lexer rest
lexKW :: String -> [Token]
lexKW cs = case span isAlpha cs of
("true", rest) -> TokenTrue : lexer rest
("false", rest) -> TokenFalse : lexer rest
("if", rest) -> TokenIf : lexer rest
("then", rest) -> TokenThen : lexer rest
("else", rest) -> TokenElse : lexer rest
("Bool", rest) -> TokenBoolean : lexer rest
("Number", rest) -> TokenNumber : lexer rest
("inl", rest) -> TokenInl : lexer rest
("inr", rest) -> TokenInr : lexer rest
("case", rest) -> TokenCase : lexer rest
("of", rest) -> TokenOf : lexer rest
(var, rest) -> TokenVar var : lexer rest
lexSymbol :: String -> [Token]
lexSymbol cs = case span isToken cs of
("->", rest) -> TokenArrow : lexer rest
("&&", rest) -> TokenAnd : lexer rest
("==", rest) -> TokenEq : lexer rest
("|", rest) -> TokenBar : lexer rest
_ -> error "Lexical error: símbolo inválido!"
Interpreter.hs
module Interpreter where
import Lexer
subst :: String -> Expr -> Expr -> Expr
subst x n b@(Var v) = if v == x then
n
else
b
subst x n (Lam v t b) = Lam v t (subst x n b)
subst x n (App e1 e2) = App (subst x n e1) (subst x n e2)
subst x n (Add e1 e2) = Add (subst x n e1) (subst x n e2)
subst x n (And e1 e2) = And (subst x n e1) (subst x n e2)
subst x n (If e e1 e2) = If (subst x n e) (subst x n e1) (subst x n e2)
subst x n (Paren e) = Paren (subst x n e)
subst x n (Eq e1 e2) = Eq (subst x n e1) (subst x n e2)
subst x n (Inl b) = Inl (subst x n b)
subst x n (Inr b) = Inr (subst x n b)
subst x n (Case e1 e2 e3) = Case (subst x n e1)(subst x n e2)(subst x n e3)
subst x n e = e
isvalue :: Expr -> Bool
isvalue BTrue = True
isvalue BFalse = True
isvalue (Num _) = True
isvalue (Lam _ _ _) = True
isvalue (Inl _) = True
isvalue (Inr _) = True
isvalue (Case _ _ _) = True
isvalue _ = False
step :: Expr -> Maybe Expr
step (Add (Num n1) (Num n2)) = Just (Num (n1 + n2))
step (Add (Num n1) e2) = case step e2 of
Just e2' -> Just (Add (Num n1) e2')
_ -> Nothing
step (Add e1 e2) = case step e1 of
Just e1' -> Just (Add e1' e2)
_ -> Nothing
step (And BTrue e2) = Just e2
step (And BFalse _) = Just BFalse
step (And e1 e2) = case step e1 of
Just e1' -> Just (And e1' e2)
_ -> Nothing
step (If BTrue e1 _) = Just e1
step (If BFalse _ e2) = Just e2
step (If e e1 e2) = case step e of
Just e' -> Just (If e' e1 e2)
_ -> Nothing
step (App e1@(Lam x t b) e2) | isvalue e2 = Just (subst x e2 b)
| otherwise = case step e2 of
Just e2' -> Just (App e1 e2')
_ -> Nothing
step (App e1 e2) = case step e1 of
Just e1' -> Just (App e1' e2)
_ -> Nothing
step (Paren e) = Just e
step (Eq e1 e2) | isvalue e1 && isvalue e2 = if e1 == e2 then
Just BTrue
else
Just BFalse
| isvalue e1 = case step e2 of
Just e2' -> Just (Eq e1 e2')
_ -> Nothing
| otherwise = case step e1 of
Just e1' -> Just (Eq e1' e2)
_ -> Nothing
step e = Just e
eval :: Expr -> Expr
eval e | isvalue e = e
| otherwise = case step e of
Just e' -> eval e'
_ -> error "Interpreter error!"
Typechecker.hs
module TypeChecker where
import Lexer
type Ctx = [(String, Ty)]
typeof :: Ctx -> Expr -> Maybe Ty
typeof _ BTrue = Just TBool
typeof _ BFalse = Just TBool
typeof _ (Num _) = Just TNum
typeof ctx (Add e1 e2) = case (typeof ctx e1, typeof ctx e2) of
(Just TNum, Just TNum) -> Just TNum
_ -> Nothing
typeof ctx (And e1 e2) = case (typeof ctx e1, typeof ctx e2) of
(Just TBool, Just TBool) -> Just TBool
_ -> Nothing
typeof ctx (If e e1 e2) =
case typeof ctx e of
Just TBool -> case (typeof ctx e1, typeof ctx e2) of
(Just t1, Just t2) -> if t1 == t2 then
Just t1
else
Nothing
_ -> Nothing
_ -> Nothing
typeof ctx (Var v) = lookup v ctx
typeof ctx (Lam v t1 b) = let Just t2 = typeof ((v, t1):ctx) b
in Just (TFun t1 t2)
typeof ctx (App t1 t2) = case (typeof ctx t1, typeof ctx t2) of
(Just (TFun t11 t12), Just t2) -> if t11 == t2 then
Just t12
else
Nothing
_ -> Nothing
typeof ctx (Eq e1 e2) = case (typeof ctx e1, typeof ctx e2) of
(Just t1, Just t2) -> if t1 == t2 then
Just TBool
else
Nothing
_ -> Nothing
typeof ctx (Paren e) = typeof ctx e
typecheck :: Expr -> Expr
typecheck e = case typeof [] e of
Just _ -> e
_ -> error "Type error"
I want to add semantic rules for sum types (Inl, Inr, and Case) to my interpreter and type checker. Could you guide me on how to correctly implement the semantic rules for these constructs?
Here are my specific questions:
- How should I extend the isvalue, step, and typeof functions to handle Inl, Inr, and Case expressions?
- What modifications are necessary for the substitution function subst to support these constructs?
Any help or examples would be greatly appreciated!!!!!!!!!!