-
Notifications
You must be signed in to change notification settings - Fork 1
GADTs
Source: Haskell Wiki
Allows you to explicitly write down the data constructors thus enabling you to constrain (type level guarantee) the return types.
data Expr = I Int -- integer constants
| Add Expr Expr -- add two expressions
| Mul Expr Expr -- multiply two expressions
deriving Show
eval :: Expr -> Int
eval (I n) = n
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
(5+1) x 7 would be represented as:
>> (I 5 `Add` I 1) `Mul` I 7 :: Expr.
Now, imagine that we would like to extend our language with other types than just integers. For instance, let's say we want to represent equality tests, so we need booleans as well. We augment the Expr
type to become:
data Expr = I Int
| B Bool -- boolean constants
| Add Expr Expr
| Mul Expr Expr
| Eq Expr Expr -- equality test
5+1 == 7 would be represented as:
>> (I 5 `Add` I 1) `Eq` I 7.
eval :: Expr -> Either Int Bool
eval (I n) = Left n
eval (B b) = Right b
will not type check:
eval (Add e1 e2) = eval e1 + eval e2 --
can represent illegal states:
``haskell
B True Add
I 5 :: Expr
*would have to add another layer in return type to represent failure:*
```haskell
eval :: Expr -> Maybe (Either Int Bool)
eval = ...
Now, we could write this function just fine, but that would still be unsatisfactory, because what we really want to do is to have Haskell's type system rule out any invalid expressions; we don't want to check types ourselves while deconstructing the abstract syntax tree.
data Expr a = I Int
| B Bool
| Add (Expr a) (Expr a)
| Mul (Expr a) (Expr a)
| Eq (Expr a) (Expr a)
Note that an expression Expr a does not contain a value a at all; that's why a is called a phantom type, it's just a dummy variable. Compare that with, say, a list [a] which does contain a bunch of as.
The key idea is that we're going to use a to track the type of the expression for us. Instead of making the constructor available to users of our small language, we are only going to provide a smart constructor with a more restricted type
add :: Expr Int -> Expr Int -> Expr Int
add = Add
All add
does is constrain the type of expression to an Int so the following would not type check.
i :: Int -> Expr Int
i = I
b :: Bool -> Expr Bool
b = B
b True `add` i 5
eval (I n) = n
At the type level there is nothing preventing any of the following (although users could be shielded by only exposing smart constructors).
The following would type check
I 5 :: Expr Bool
I 5 :: Expr String
What we need is a way to constrain the return types of the constructors themselves, and that's exactly what generalized data types do.
IE. Move the smart constructor type logic into the data constructors
data Expr a where
I :: Int -> Expr Int
B :: Bool -> Expr Bool
Add :: Expr Int -> Expr Int -> Expr Int
Mul :: Expr Int -> Expr Int -> Expr Int
Eq :: Eq a => Expr a -> Expr a -> Expr Bool
eval :: Expr a -> a
eval (I n) = n
eval (B b) = b
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Eq e1 e2) = eval e1 == eval e2
So now the following would not type check:
demo2 = eval $ Mul (I 5) (B False)
src\GADTs.hs:23:27-33: error:
* Couldn't match type `Bool' with `Int'
Expected type: Expr Int
Actual type: Expr Bool
* In the second argument of `Mul', namely `(B False)'
In the second argument of `($)', namely `Mul (I 5) (B False)'
In the expression: eval $ Mul (I 5) (B False)
|
23 | demo2 = eval $ Mul (I 5) (B False)