Example of a type level function that is not a type constructor

Question

What is unique to a "type constructor" concept in Haskell compared to other type-level functions?

As far as I know they:

• allow user to apply arguments to them during compilation
• result in a simple type (not a constraint for example) after supplying finite number of arguments

Answer 1

There are two common usages of the phrase "type constructor". Some people use them for any type with an arrow kind; but the Haskell report uses it pretty consistently in a different way, so I'll talk about that definition.

Constructors are created by data and newtype declarations, and are the single new name introduced at the type level by these declarations. Here are some examples of type constructors:

Either
Maybe
[]
Bool

Whoops, did you notice that last one? That's right, there's nothing about the phrase "type constructor" that implies it must be able to take arguments. Bool is a type-level name introduced by a data declaration -- hence is a type constructor. Here are some examples of types which are not constructors:

Maybe Int
a -> b
Either ()
m -- even if we know, say, Monad m holds

Whoops, did you notice those last two? That's right, going in the other direction, there's nothing about being able to take further type arguments that makes you be a type constructor. Each of Either and () are constructors, but the application of Either to () isn't, because it's not a single type-level name created by a data or newtype declaration. Similarly, m is a type variable, not a constructor -- its meaning isn't fixed by any data or newtype declaration.

Besides constructors and variables, there is one other kind of type-level name in standard Haskell: type aliases. There are two main differences between type aliases and constructors:

1. Constructors are injective, aliases may not be. If FooC a b c and FooC a' b' c' are the same type, and FooC is a constructor, then a and a' are the same type, b and b' are the same type, and c and c' are the same type. Contrast

   type FooA a = String
   

   in which FooA () and FooA Bool are the same type, even though () and Bool are not the same type.

2. Constructors may be partially applied, type aliases cannot be. For example, if you write

   type BarA a = Maybe a
   

   then StateT Int BarA () is not valid -- BarA must always be given its type argument immediately -- even though StateT Int Maybe () is. Of course, with

   type BarEtaA = Maybe
   

   then StateT Int BarEtaA () is valid again, because the alias BarEtaA doesn't need any arguments before it expands to its defined value of Maybe.

There are some other small differences between aliases and constructors, but they are not fundamental (and are relaxed by suitable GHC extensions).

There's just one difference between constructors and variables that I can think of in standard Haskell, namely their interaction with the typeclass mechanism. Specifically, instances must be of the form instance <class> (<constructor> <variable> <variable> <variable> ...) where ... and constraints/contexts must be of the form <class> (<constructor> <variable> <variable> ...) => .... These restrictions are relaxed by suitable GHC extensions.

Extended Haskell as implemented by GHC also includes two other forms of defined type-level names, type families and data families, that mix some of the above properties. The names defined by data families are very similar to constructors (they are injective and they can be partially applied) while the names defined by type families are very similar to aliases (they are not guaranteed to be injective and they cannot be partially applied). The chief difference is that they can do "type-level pattern matching" in which there are multiple definitions that apply in different cases. A full description probably won't fit in a StackOverflow answer, but the manual describes them and links to several lengthy papers discussing them.