COMP3141
Software System Design and Implementation (18s1)

# Code (Week 7)

## 1 Arithmetic Expression Language, take 1

Note that most of the code of eval is about unpacking the result values, and handling errors (even though the error handling code is minimal: in practice, you should check which subexpression went wrong, and possibly print that expression so the user knows what went wrong)

```module SimpleExpr where

data Expr
= BConst Bool
| IConst Int
| Times  Expr Expr
| Less   Expr Expr
| And    Expr Expr
| If     Expr Expr Expr
deriving (Show)

{- equivalently, using GADT style notation:

data Expr where
BConst :: Bool                 -> Expr
IConst :: Int                  -> Expr
Times  :: Expr -> Expr         -> Expr
Less   :: Expr -> Expr         -> Expr
And    :: Expr -> Expr         -> Expr
If     :: Expr -> Expr -> Expr -> Expr

-}

data Result
= IVal Int
| BVal Bool
deriving (Show)

eval :: Expr -> Result
eval (IConst n)
= IVal n
eval (BConst b)
= BVal b
eval (Times ex1 ex2)
= case (eval ex1, eval ex2) of
(IVal n1, IVal n2) -> IVal (n1 + n2)
(_,  _)            -> error "illegal expr"

eval (Less ex1 ex2)
= case (eval ex1, eval ex2) of
(IVal n1, IVal n2) -> BVal (n1 < n2)
(_, _)             -> error "illegal expr"

eval (And ex1 ex2)
= case (eval ex1, eval ex2) of
(BVal b1, BVal b2) -> BVal (b1 && b2)
(_, _)             -> error "illegal expr"

eval (If cond thenEx elseEx)
= case eval cond of
BVal True  -> eval thenEx
BVal False -> eval elseEx
_          -> error "illegal expr"

```

## 2 Arithmetic Expression Language, take 2

Here, we defined two distinct types of expressions: `IExpr`, which evaluate to integer values, and `BExpr`, which evaluate to boolean values. The upside is that we don't need to dynmically check whether an expression evaluated to the correct type. On the other hand, we need two data constructors for if-expressions, depending on the type of the branches. Even for this very simple language, this means duplicating code. For a more complex language, this is not feasible.

```module IBExpr where

data IExpr
= IConst Int
| Times  IExpr IExpr
| IIf    BExpr IExpr IExpr
deriving (Show)

data BExpr
= BConst Bool
| And   BExpr BExpr
| Less  IExpr IExpr
| BIf   BExpr BExpr BExpr
deriving (Show)

evalBExpr :: BExpr -> Bool
evalBExpr (BConst b)
= b
evalBExpr (And ex1 ex2)
= evalBExpr ex1 && evalBExpr ex2
evalBExpr (Less ex1 ex2)
= evalIExpr ex1 < evalIExpr ex2
evalBExpr (BIf cond thenExpr elseExpr)
| evalBExpr cond = evalBExpr thenExpr
| otherwise      = evalBExpr elseExpr

evalIExpr :: IExpr -> Int
evalIExpr (IConst n)
= n
evalIExpr (Times ex1 ex2)
= evalIExpr ex1 * evalIExpr ex2
evalIExpr (IIf cond thenExpr elseExpr)
| evalBExpr cond = evalIExpr thenExpr
| otherwise      = evalIExpr elseExpr

```

## 3 Arithmetic Expression Language, take 3

Using generalised algebraic data types, we can parametrise the expression with a type, and express the fact that different constructors return different expression types. This way, the type checker can statically ensure that the expressions are type correct, as in our second attempt. This time, however, we don't need different versions of the if-constructor, because we can express the fact that both branches have to have the same type without commiting to a particular type.

```{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE KindSignatures #-}
module Expr where

-- this is a 'generalised algebraic data type':
-- not all the date constructors return the same
-- result type:
data Expr a where
BConst :: Bool                             -> Expr Bool
IConst :: Int                              -> Expr Int
Times  :: Expr Int  -> Expr Int            -> Expr Int
Less   :: Expr Int  -> Expr Int            -> Expr Bool
And    :: Expr Bool -> Expr Bool           -> Expr Bool
If     :: Expr Bool -> Expr a    -> Expr a -> Expr a

-- try and replace IConst and BConst with a single
-- constructor 'Const' for constants of any type.
-- Change the definition of 'eval' accordingly.

deriving instance Show (Expr a)

-- No checking necessary, as the type checker ensures
-- that the invariants are observed
eval :: Expr a -> a
eval (BConst b) = b
eval (IConst n) = n
eval (Times e1 e2)
= eval e1 * eval e2
eval (Less e1 e2)
= eval e1 < eval e2
eval (And e1 e2)
= eval e1 && eval e2
eval (If cond e1 e2)
| eval cond = eval e1
| otherwise = eval e2

```

## 4 Untyped printf implementation

```{-# LANGUAGE GADTs #-}
module Printf where

-- untyped format string, written in GADT style
data Format where
X ::                     Format
I :: Format           -> Format
S :: Format           -> Format
L :: String -> Format -> Format

data Args
= IntArg Int
| StrArg String

-- construct the printf string (partial function)
printf :: Format -> [Args] -> String
printf X [] = ""
printf (I restformat) (IntArg n : restArgs)
= show n ++ printf restformat restArgs
printf (S restformat) (StrArg str : restArgs)
= str ++ printf restformat restArgs
printf (L str restformat) args
= str ++ printf  restformat args
printf _ _
= error "format string and argument mismatch"

example :: String
example
= printf (S (L " is " (I  (L " years old" X))))
[StrArg "Joe", IntArg 5]
```

2018-06-14 Thu 18:28