Disjoint sums

We can define several constructors in a type:

data Nat = Zero | Succ Nat

$Zero$ and $Succ$ are constructors. In this case they are not polymorphic, but we can define polymorphic constructors.

data Seq a = Empty | Cons a (Seq a)

The constructors are $Empty$ and $Cons$, and are polymorphic.

Constructors are used to build terms, what distinguishes a constructor from a function is that there is no definition associated to a constructor, and constructors can be used in patterns.