The type “” is usually written as and finite lists x1x2...xn are written as x1x2...xn. We can define operations on recursive types by inductive definitions where pattern matching supports the convenient separation of the different cases. For instance, the concatenation operation “” on polymorphic lists can be defined as follows (the optional type declaration in the first line specifies that “” takes two lists as input and produces an output list, where all list elements are of the same unspecified type):