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
Nothing constructor straightforwardly returns a
Maybe a. And
Just is a function from