Data Constructors Are Functions

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.