How to Implement Sum Type Semantic Rules in a Haskell Lambda Calculus Interpreter?

Question

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:

1. How should I extend the isvalue, step, and typeof functions to handle Inl, Inr, and Case expressions?
2. What modifications are necessary for the substitution function subst to support these constructs?

Any help or examples would be greatly appreciated!!!!!!!!!!

Answer 1

I'll provide a few hints.

isvalue (Inl _) = True
isvalue (Inr _) = True
isvalue (Case _ _ _) = True

These are wrong. For instance, Inr (Add (Num 1) (Num 3)) is not a value. Case .... is never a value.

typeof (Inl ...) can not be sensibly defined. For instance, typeof (Inl BTrue) should be TSum TBool t for all ts, which makes no sense. Dealing with such polymorphic types is tricky. I'd recommend you instead add the "other" type to the syntax, e.g. allowing Inl TInt BTrue so that it has type TSum TBool TInt.

Case Expr Expr Expr is not faithful to the syntax you posted, since you forgot the bound variables in the two branches. Consider something like Case Expr String Expr String Expr for case e of inl x => e' | inr y => e''. (Alternatively, you could use the syntax case e (\x -> e) (\y -> e) so that you keep Case Expr Expr Expr, but you need to adapt the typing rules from the ones you posted.)

subst x n (Lam v t b) = Lam v t (subst x n b)

This is correct only when n has no free variables, e.g. a value. Are you assuming that? Otherwise we need to watch out for captured variables.

subst x n (Inl b) = Inl (subst x n b)
subst x n (Inr b) = Inr (subst x n b) 

This looks ok.

subst x n (Case e1 e2 e3) = Case (subst x n e1)(subst x n e2)(subst x n e3)

This should be adapted to the new Case definition given above. The same comments for the Lam case also apply here.