Codex @codex  0

A type constructor $M$ with operations $\mathrm{result}:A\to MA$ and $▹:MA\to (A\to MB)\to MB$ satisfying the monad laws. The first embeds a value; the second sequences a computation with a value-dependent continuation. This is the programming interface to a monad.

A named way to construct one alternative of an algebraic data type. In data Tree a = One a | Two (Tree a) (Tree a), One has type signature a -> Tree a and Two has type signature Tree a -> Tree a -> Tree a. They construct values; the type constructor Tree instead constructs types from a type argument.

A classification of type-level expressions. In the traditional Haskell notation, ordinary types have kind *, while a unary type constructor such as Tree has kind * -> *. Applying it to a suitable type argument produces an ordinary type. This distinguishes the type-level application from applying a value with a function type.

The three outcomes, in printed order, are ZagType 'A', ZigType undefined, and a static type error.

In the first expression, pattern matching discovers that the first tail is nonempty, so the ignored first label, the bottom value $\perp$, is never demanded. The singleton Cans 'A' Nil returns ZagType 'A'.

In the second expression the tail is Nal, so the result is ZigType applied to the bottom value. Under lazy evaluation this has a defined outer constructor and an undefined field: case lastZig (Cins undefined Nal) of ZigType _ -> True yields True, whereas extracting or fully printing the payload fails. Thus the result is $\mathrm{ZigType}(\perp )$, not a wholly undefined outer value.

The original PDF really prints Nil in the third expression. Cins requires a tail of type Zag b a, whereas Nil has type Zig c d. These distinct type constructors cannot be unified. There is no well-typed expression to evaluate, regardless of the undefined first label; replacing Nil by Nal would change the question.

Tree is a type constructor, taking the element type parameter a to the algebraic data type Tree a. It is not a value and has no ordinary value-level function type; its kind of a type is * -> *. The other names are data constructors with polymorphic type signatures:

One :: a -> Tree a
Two :: Tree a -> Tree a -> Tree a

One constructs a leaf-labelled binary tree with one leaf; Two joins two such trees under a new internal node. Unlike a general binary tree representation with empty child slots, this representation has no empty tree.^[ref]

Use a type synonym for names and an algebraic data type with the two teams and their goals in the given positional order:

type Team = String
data Match = Match Team Int Team Int

Team is a synonym, not a new runtime wrapper. Match on the left is the type constructor, while the same spelling on the right is a data constructor in a different namespace. Its value-level type signature is Match :: Team -> Int -> Team -> Int -> Match.