Define a list using only the Hindley-Milner type system
Pairs

This encoding is the Church encoding of pairs. Similar techniques can encode booleans, integers, lists, and other data structures.

Under the context x:a; y:b, the term pair x y has the type (a -&gt; b -&gt; t) -&gt; t. The logical interpretation of this type is the following formula (I use standard mathematical notations: $\to$ is implication, $\vee$ is or, $\wedge$ is and, $\neg$ is negation; $\iff$ is equivalence of formulas):
$$ \begin{align}
  (a \to b \to t) \to t
  &amp; \quad\iff\quad \neg (\neg a \vee \neg b \vee t) \vee t \\
  &amp; \quad\iff\quad (a \wedge b \wedge \neg t) \vee t \\
  &amp; \quad\iff\quad (a \wedge b) \vee t \\
\end{align}
$$
Why “a and b or t”? Intuitively, because pair is a function that takes a function as an argument and applies it to the pair. There are two ways this can go: the argument function can make use of the pair, or it can produce a value of type t without using the pair at all.

pair is a constructor for the pair type and first and second are destructors. (These are the same words used in object-oriented programming; here the words have a meaning that is related to the logical interpretation of the types and terms that I won't go into here.) Intuitively, the destructors let you access what is in the object and the constructors pave the way for the destructor by taking as an argument a function that they apply to the parts of the object. This principle can be applied to other types.

Sums

The Church encoding of a discriminated union is essentially dual to the Church encoding of a pair. Where a pair has two parts that must be put together and you can choose to extract one or the other, you can choose to build the union in either of two ways and when you use it you need to allow for both ways. Thus there are two constructors, and there is a single destructor which takes two arguments.

let case w = λf. λg. w f g           case : ((a-&gt;t) -&gt; (b-&gt;t) -&gt; t) -&gt; (a-&gt;t) -&gt; (b-&gt;t) -&gt; t
  (* or simply let case w = w *)
let left x = λf. λg. f x             left : a -&gt; ((a-&gt;t) -&gt; (b-&gt;t) -&gt; t)
let right y = λf. λg. g x            right : b -&gt; ((a-&gt;t) -&gt; (b-&gt;t) -&gt; t)


Let me abbreviate the type (a-&gt;t) -&gt; (b-&gt;t) -&gt; t as SUM(a,b)(t). Then the types of the destructors and constructors are:

case : SUM(a,b)(t) -&gt; (a-&gt;t) -&gt; (b-&gt;t) -&gt; t
left : a -&gt; SUM(a,b)(t)
right : b -&gt; SUM(a,b)(t)


Thus

case (left x) f g → f x
case (rightt y) f g → g y


Lists

For a list, apply again the same principle. A list whose elements have the type a can be built in two ways: it can be an empty list, or it can be an element (the head) plus a list (the tail). Compared with pairs, there's a little twist when it comes to the destructors: you can't have two separate destructors head and tail because they would only work on non-empty lists. You need a single destructor, with two arguments, one of which is a 0-argument function (i.e. a value) for the nil case, and the other a 2-argument function for the cons case. Functions like is_empty, head and tail can be derived from that. Like in the case of sums, the list is directly its own destructor function.

let nil = λn. λc. n
let cons h t = λn. λc. c h t
let is_empty l = l true (λh. λt. false) 
let head l default = l default (λh. λt. h)
let tail l default = l default (λh. λt. t)


Each of these functions is polymorphic. If you work the types of these functions, you'll note than cons is not uniform: the type of the result is not the same as the type of the argument. The type of the result is a variable — it is more general than the argument. If you chain cons calls, the successive calls to build a list instantiate cons at different types. This is crucial to make lists work in the absence of recursive types. You can make heterogeneous lists that way. In fact, the types that you can express are not “list of $T$”, but “list whose first elements are of types $T_1,\ldots,T_n$”.

As you surmise, if you want to define a type that only contains homogeneous lists, you need recursive types. Why? Let's look at the type of a list. A list is encoded as a function which takes two arguments: the value to return on empty lists, and the function to compute the value to return on a cons cell. Let a be the element type, b be the type of the list, and c be the type returned by the destructor. The type of a list is

a -&gt; (a -&gt; b -&gt; c) -&gt; c


Making the list homogeneous is saying that if it's a cons cell, the tail has to have the same type as the whole, i.e. it adds the constraint

a -&gt; (a -&gt; b -&gt; c) -&gt; c = b


The Hindley-Milner type system can be extended with such recursive types, and in fact practical programming languages do that. Practical programming languages tend to disallow such “naked” equations and require a data constructor, but this is not an intrinsic requirement of the underlying theory. Requiring a data constructor simplifies type inference, and in practice tends to avoids accepting functions that are actually buggy but happen to be typable with some unintended constraint that causes a difficult-to-understand type error where the function is used. This is why, for example, OCaml accepts unguarded recursive types only with the non-default -rectypes compiler option. Here are the definitions above in OCaml syntax, together with a type definition for homogeneous lists using the notation for aliased recursive types: type_expression as 'a means that the type type_expression is unified with the variable 'a.

# let nil = fun n c -&gt; n;;
val nil : 'a -&gt; 'b -&gt; 'a = &lt;fun&gt;
# let cons h t = fun n c -&gt; c h t;;
val cons : 'a -&gt; 'b -&gt; 'c -&gt; ('a -&gt; 'b -&gt; 'd) -&gt; 'd = &lt;fun&gt;
# let is_empty l = l true (fun h t -&gt; false);;
val is_empty : (bool -&gt; ('a -&gt; 'b -&gt; bool) -&gt; 'c) -&gt; 'c = &lt;fun&gt;
# let head l default = l default (fun h t -&gt; h);;
val head : ('a -&gt; ('b -&gt; 'c -&gt; 'b) -&gt; 'd) -&gt; 'a -&gt; 'd = &lt;fun&gt;
# let tail l default = l default (fun h t -&gt; t);;
val tail : ('a -&gt; ('b -&gt; 'c -&gt; 'c) -&gt; 'd) -&gt; 'a -&gt; 'd = &lt;fun&gt;
# type ('a, 'b, 'c) ulist = 'c -&gt; ('a -&gt; 'b -&gt; 'c) -&gt; 'c;;
type ('a, 'b, 'c) ulist = 'c -&gt; ('a -&gt; 'b -&gt; 'c) -&gt; 'c
# is_empty (cons 1 nil);;
- : bool = false
# head (cons 1 nil) 0;;
- : int = 1
# head (tail (cons 1 (cons 2.0 nil)) nil) 0.;;
- : float = 2.

(* -rectypes is required for what follows *)
# type ('a, 'b, 'c) rlist = 'c -&gt; ('a -&gt; 'b -&gt; 'c) -&gt; 'c as 'b;;
type ('a, 'b, 'c) rlist = 'b constraint 'b = 'c -&gt; ('a -&gt; 'b -&gt; 'c) -&gt; 'c
# let rcons = (cons : 'a -&gt; ('a, 'b, 'c) rlist -&gt; ('a, 'b, 'c) rlist);;
val rcons :
  'a -&gt;
  ('a, 'c -&gt; ('a -&gt; 'b -&gt; 'c) -&gt; 'c as 'b, 'c) rlist -&gt; ('a, 'b, 'c) rlist =
  &lt;fun&gt;
# head (rcons 1 (rcons 2 nil)) 0;;
- : int = 1
# tail (rcons 1 (rcons 2 nil)) nil;;
- : 'a -&gt; (int -&gt; 'a -&gt; 'a) -&gt; 'a as 'a = &lt;fun&gt;
# rcons 1 (rcons 2.0 nil);;
Error: This expression has type
         (float, 'b -&gt; (float -&gt; 'a -&gt; 'b) -&gt; 'b as 'a, 'b) rlist = 'a
       but an expression was expected of type
         (int, 'b -&gt; (int -&gt; 'c -&gt; 'b) -&gt; 'b as 'c, 'b) rlist = 'c


Folds

Looking at this a bit more generally, what is the function that represents the data structure?


For a natural number: $n$ is represented as the function which iterates its argument $n$ times.
For a pair: $(x,y)$ is represented as a function which applies its argument to $x$ and $y$.
For a sum: $\mathrm{in}_i(x)$ is represented as a function which applies its $i$th argument to $x$.
For a list: $[x_1,\ldots,x_n]$ is represented as a function that takes two arguments, the value to return for the empty list and the function to apply to cons cells.


In general terms, the data structure is represented as its fold function. This is a general concept for data structures: a fold function is a higher-order function that traverses the data structure. There is a technical sense in which fold is universal: all “generic” data structure traversals can be expressed in terms of fold. That the data structure can be represented as its fold function shows this: all you need to know about a data structure is how to traverse it, the rest is an implementation detail.