C be a functor.
Section 6 concludes the paper giving some final remarks. 2. Mathematical Framework Our approach to genericity is based on the category-theoretic modelling of types and programs. g. [2, 18]). In this section we review the relevant concepts around the categorical approach to recursive types [23, 25, 21] and its application to program calculation [24, 27, 11, 22, 5]. The category-theoretic explanation of (recursive) types is based on the idea that types constitute objects of a category C, programs are modelled by arrows of the category, and type constructors are functors on C.
As described above, there is the added restriction that any data which this function accepts must have the given constructor, otherwise pattern matching will fail at run-time. This cannot be enforced in the current system. A type system with constructor subtyping  could help here. Compilation. Constructor cases are implemented using a slight modification of the structure type encoding and specialisation process introduced in Section 2. We demonstrate the scheme on our example Expr datatype. For each constructor, a type synonym is introduced, identifying the type of the constructor case with the type it is constructing: type ConCase_ Var = Expr type ConCase_App = Expr type ConCase_Lambda Expr type ConCase_Let Expr.