#### 27 Sep 2018

Thanks to Iceland Jack for this one. This post is me turning Iceland Jack’s thread into a blog post. To define an Algebraic Data Type (ADT) in Haskell we use the `data`

keyword. Data declarations consist of two constructors, a type constructor and a data, or value, constructor.

data MyType = Something ^ ^ type constructor data constructor

Both constructors may have zero or more arguments. The example above has zero arguments, and so is called a nullary constructor. The Bool type is an example of a nullary datatype:

data Bool = True | False

Here is the syntax for a non-nullary data type.

data MyType a b c = Something a b c ^ ^ constructor args constructor args

It is the same as the nullary one, except that the type- and data constructors have parameters following them. An example of a non-nullary datatype would be the Maybe type. The type constructor `Maybe`

has one argument `a`

, and the `Just`

data constructor has one argument also.

data Maybe a = Nothing | Just a ^ ^ arg to Maybe arg to Just

Now what is not apparent from this syntax is what exactly a non-nullary data constructor is: what exactly is `Just`

and how does it work?

The answer is that `Just`

is a function. In fact, all data constructors are functions. This means we can pass them into other functions, pattern match on them, return them, and so on.

Now the unfortunate thing about ADTs is that it is not obvious to see that we are dealing with functions. Fortunately, if we use the syntax from Generalised Algebraic Data Types (GADT), it does become apparent. Let’s rewrite `Maybe`

in the syntax of GADTs.

data Maybe :: Type -> Type where Nothing :: Maybe a Just :: a -> Maybe a

This says that the type `Maybe`

is also a function from a Type to a Type, which makes sense because `Maybe`

is polymorphic on some type `a`

. The `Nothing`

constructor straightforwardly returns a `Maybe a`

. And `Just`

is a function from `a`

to `Maybe a`

.