Generalized Algebraic Datatypes

The use of GADT derives from advanced constraints on types. This sort of includes

• template specification in C++
• concepts/traits with static assert/compile time check in C++/Rust

GADT uses constructors to lift information about concrete type passed to constructor to its type. For example, in naive ADT

1

data Expr a = LiteralInt Int | Literal a

The problem here is that Expr a does not enforce LiteralInt :: Expr Int; also, unlike defining type classes, we connot constrain a with certain conditions. Like, it’ll report error if we want to only those satisfying Eq a can be passed to Expr a.

In this case, we have to use GADT, which allows template parameter constraints, just like concepts in C++, and trait, static_assert in Rust.

So now, our target can be achieved:

1
2
3

data Expr a where
  LiteralInt :: Int -> Expr Int
  Literal :: (Eq a) => a -> Expr a

The LiteralInt can be regarded as template specification, and Literal constructor now has a constraint Eq a =>, which limits the types that are passed to Expr.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

data NE =
  NotEqual

data Expr a where
  LiteralInt :: Int -> Expr Int
  Literal :: (Eq a) => a -> Expr a

-- Error: does not satisfy Eq NE
-- result = Literal NotEqual

-- result :: Expr Bool
result = Literal True

-- r2 :: Expr Integer
r2 = Literal 1

-- rint :: Expr Int
rint = LiteralInt 1

Moreover, you can make constructor wrap more argument and pack them together as a single datatype.

1
2

data Expr a where
  Pair :: Expr a -> Expr b -> Expr (a, b)