
\section{Introduction}

Type classes are a fabulously useful idea. Although the motivation for their introduction to Haskell was to support ad-hoc polymorphism, on a conceptual level their utility is more general. Type classes define sets of types, usually with some common property. For example @Eq@ defines the set of types that can be compared for equality, and @Show@ is the set of types that can be converted to some textual representation. Both @Eq@ and @Show@ operate on types of kind @*@, that is the types of values. Constructor classes \cite{jones:constructor-classes} generalise this to higher kinds. For example, the @Monad@ class applies to constructors of kind @* -> *@ such as @IO@, @List@ and @Maybe@. 

A natural question is whether there are other kinds of types that we could usefully apply type classes to. This is indeed the case! Although kinds in Haskell are (possibly nullary) functions of the value kind @*@, in our own language Disciple we also have  region, effect and closure types, and their associated kinds. The aim of this paper is to explore the design space of type classes as applied to types of these extra kinds. We discuss their utility in Disciple, and how they interact when combined in the same language.

We make the following contributions:

\begin{itemize}
\item	We reprise the use of @Const@ and @Mutable@ constraints on region types \CITE to support mutability polymorphism. We show how the addition of ad-hoc overloading requires the @DeepConst@ and @DeepMutable@ constraints that apply to all the regions in a larger type.

\item	We show how lazy evaluation can be safely introduced into language that supports mutability polymorphism. We do this by requiring suspended applications to be pure, which we enforce with the @Pure@ class that applies to effect types.

\item	We show that in the presence of mutability polymorphism, overloading standard functions such as @copy@ and @update@ requires a built-in @Shape@ constraint that constrains the value structure of a type to match another, but allows the region, effect and closure information to differ.

\item	Applying the @Shape@ constraint to data types that contain functions requires us to keep track of which parameters of that type are in \emph{material} and \emph{immaterial} positions. Materiality is related to the notion of ``phantom types'', and we show how to compute this information from an arbitrary data type definition.

\item	In a default strict language where only a small percentage of applications are suspended, tracking which objects can possibly be thunks leads to optimisation opportunities during code generation. We show how to use @Lazy@ and @Direct@ constraints on region types to achieve this.

\item	Including a polymorphic suspension operator then requires that we introduce the @HeadLazy@ constraint, which indicates that the outer-most constructor of a data type may be represented as a thunk.

\item	The @Pure@ constraint when applied to an effect type requires that effect to be the least element, which we write as @!0@. For closure types, the corresponding constraint is @Empty@ which requires that a function does not reference variables from its closure. We discuss potential applications for this constraint in our parallel array library Repa, as well as in Erlang style languages for distributed computing.


\end{itemize}

In a related paper \CITE we show how to manage the plain @Const@, @Mutable@ and @Pure@ constraints in a System-F style core language. In contrast, this paper focuses on the source language, and the benefits the programmer can gain by using them. We also believe this is the first paper to discuss constraints such as @Shape@, @Direct@, @Lazy@, @HeadLazy@ and @Empty@.

\TODO{Briefly mention related work}
