When you have phantom types, you get can catch logically illegal functions in the type itself. You can create constructors for types so that you can't create illegal expressions.
-----------------
data Expr = Num Int -- atom
| Str String -- atom
| Op BinOp Expr Expr -- compound
deriving (Show)
data BinOp = Add | Concat
deriving (Show)
data Expr1 a = Num1 Int -- atom
| Str1 String -- atom
| Op1 BinOp (Expr1 a) (Expr1 a) -- compound
deriving (Show)
addition :: Expr1 Int -> Expr1 Int -> Expr1 Int
addition (Num1 a) (Num1 b) = Num1 $ a + b
createNum :: Int -> Expr
createNum a = Num a
createStr :: String -> Expr
createStr a = Str a
createNum1 :: Int -> Expr1 Int
createNum1 a = Num1 a
createStr1 :: String -> Expr1 String
createStr1 a = Str1 a
sumExpr :: Expr -> Expr -> Expr
sumExpr a b = Op Add a b
sumExpr1 :: Expr1 Int -> Expr1 Int -> Expr1 Int
sumExpr1 a b = Op1 Add a b
-----------------
With the above, you can create expressions that make no sense in real life (like adding/concating a number to a string ). When I execute this in GHCI, I get the following
--------
λ> sumExpr (createNum 1) (createStr "a")
Op Add (Num 1) (Str "a")
λ> sumExpr1 (createNum1 1) (createStr1 "a")
<interactive>:342:26-39:
Couldn't match type ‘[Char]’ with ‘Int’
Expected type: Expr1 Int
Actual type: Expr1 String
In the second argument of ‘sumExpr1’, namely ‘(createStr1 "a")’
In the expression: sumExpr1 (createNum1 1) (createStr1 "a")
λ>
--------
From the above, it is clear that as long as we write constructors taking into account the types (called smart-constructors), we can prevent expressions from being created. I do admit that this makes it a bit tedious as we would have to write the constructors by hand, but we get type level guarantees.
I think GADTs are much better for things like this for specifying the constructors, but you'd still have to write sumExpr1 in program.