\documentclass{article}
\flushbottom

\usepackage{color}
\newcommand{\authornote}[3]{{\color{#2} {\sc #1}: #3}}
\renewcommand{\authornote}[3]{}
\newcommand\simon[1]{\authornote{Simon}{red}{#1}}
\newcommand\ken[1]{\authornote{Ken}{blue}{#1}}
\newcommand\oleg[1]{\authornote{Oleg}{green}{#1}}

\usepackage[hyphens]{url}
\usepackage[sort&compress,numbers]{natbib}
\usepackage{comment}

\usepackage[compact]{fancyvrb1}
\DefineShortVerb{\|} % |
\DefineVerbatimEnvironment{code}{Verbatim}{xleftmargin=\parindent}
\RecustomVerbatimCommand{%
  \VerbatimInput}{VerbatimInput}{xleftmargin=\parindent}
\VerbatimFootnotes
 
\begin{document}

\title{Fun with type functions}
\author{Oleg Kiselyov \and Simon Peyton Jones \and Chung-chieh Shan}
\maketitle

\abstract{ Tony Hoare has always been a leader in writing down and
proving properties of programs.  To prove properties of programs
automatically, the most widely used technology today is by far the
ubiquitous type checker.  Alas, static type systems inevitably exclude
some good programs and allow some bad ones.  Thus motivated, we
describe some fun we have been having with Haskell, by making the type
system more expressive without losing the benefits of automatic proof
and compact expression.  Specifically, we offer a programmer's tour of
so-called \emph{type families}, a recent extension to Haskell that
allows functions on types to be expressed as straightforwardly
as functions on values.
This facility
makes it easier for programmers to effectively extend the compiler by
writing functional programs that execute during type-checking.

This paper gives a programmer's tour of type families as they are
supported in GHC.  
\par
{\small Source code for all the examples is available
at \url{http://research.microsoft.com/~simonpj/papers/assoc-types/fun-with-type-funs/fun-with-type-funs.zip}}
}
% \emph{We warmly encourage feedback on this draft, prior to publication.
% Please add comments to the Wiki page at \url{http://haskell.org/haskellwiki/Simonpj/Talk:FunWithTypeFunctions}.}

% Perhaps the most famous example of constructor polymorphism and type
% classes is monads.  We start by showing how to use type families to map
% monads to the types of their operations.  This mapping is essentially a
% type-level program that operates on a sum type, or rather, a sum kind.
% We then move on to recursive type-level programs, which can be used
% to write \emph{datatype-generic} code without boilerplate repetition.
% Finally, we use functions on \emph{phantom types} to refine and enforce
% specifications of program behavior.  Type families can thus be used for
% lightweight, compositional program verification [celebrate Hoare].

\section{Introduction}

The type of a function specifies (partially)
what it does.  Although weak as a specification language, 
static types have compensating virtues: they are
\begin{itemize}
\item \emph{lightweight}, so programmers use them;
\item \emph{machine-checked} with minimal programmer assistance;
\item \emph{ubiquitous}, so programmers cannot avoid them.
\end{itemize}
As a result, static type checking is by far the most widely used 
verification technology today.  

Every type system excludes some ``good'' programs, and permits
some ``bad'' ones.  
For example, a language that lacks polymorphism will reject this ``good''
program:
\begin{code}
f :: [Int] -> [Bool] -> Int
f is bs = length is + length bs
\end{code}
Why?  Because the |length| function cannot apply to both a list of |Int|s and a list
of |Bool|s.   The solution is to use a more sophisticated type system in which
we can give |length| a polymorphic type.

Conversely, most languages will accept the expression
\begin{code}
speed + distance
\end{code}
where |speed| is a variable representing speed, and |distance| represents distance,
even though adding a speed to a distance is as much nonsense as adding a
character to a boolean.

The type-system designer wants to
accommodate more good programs and exclude more bad ones, without going overboard
and losing the virtues mentioned above.
In this paper we describe \emph{type families}, 
an experimental addition to Haskell with precisely this goal.
We start by using type families to accommodate more good programs, then
turn in Section~\ref{s:phantom} to excluding more bad programs.
We focus on the programmer, and our style is informal and tutorial.
The technical background can be found elsewhere
\cite{chakravarty:assoc-data,chakravarty-synonyms,schrijvers-et-al:open-type-functions,chakravarty:indexed-families}.
The complete code described in the paper is available
\oleg{currently, in our DARCS repository. Should we find a better
  place for it?}.
That directory also contains the online version of the paper with
additional appendices, briefly describing the syntax of type functions
and the rules and pitfalls of their use. Appendix C gives an
alternative derivation of typed |sprintf| using
higher-order type-level functions.


\section{Associated types: indexing types by types}

Haskell has long offered two ways to express \emph{relations} on
types. Multiparameter type classes express arbitrary, many-to-many
relations, whereas type constructors express specifically
\emph{functional} relations, where one type (the `argument') uniquely
determines the other. For example, the relation between the type of a
list and the type of that list's elements is a functional relation,
expressed by the type constructor |[] :: * -> *|, which maps an
arbitrary type |a| to the type |[a]| of lists of |a|. A type
constructor maps its argument types \emph{uniformly}, incorporating them
into a more complex type without inspecting them.  Type functions, the
topic of this paper, also establish functional relations between types,
but a type function may perform case analysis on its argument types.

% For example,
% a monad might support operations on a specific, associated type, and
% a collection might be designed to contain elements of a specific,
% associated type.

For example, consider the relation between a monad that supports
mutable state and the corresponding type constructor for reference cells.
The |IO| monad
supports the following operations on reference cells of type |IORef a|: 
\begin{code}
newIORef   :: a -> IO (IORef a)
readIORef  :: IORef a -> IO a
writeIORef :: IORef a -> a -> IO ()
\end{code}
Similarly, the |ST s| monad supports
the analogous operations on reference cells of type |STRef s a|:
\begin{code}
newSTRef   :: a -> ST s (STRef s a)
readSTRef  :: STRef s a -> ST s a
writeSTRef :: STRef s a -> a -> ST s ()
\end{code}
It is tempting to overload these operations using
a multiparameter type class:
\begin{code}
class Mutation m r where
  newRef   :: a -> m (r a)
  readRef  :: r a -> m a
  writeRef :: r a -> a -> m ()

instance Mutation IO IORef where
  newRef = newIORef
  ...etc...
   
instance Mutation (ST s) (STRef s) where
  newRef = newSTRef
  ...etc...
\end{code}
This approach has two related disadvantages. First, the types of
|newRef| and the other class operations are
too polymorphic: one could declare an instance
such as
\begin{code}
instance Mutation IO (STRef s) where ...
\end{code}
even though we intend that the |IO| monad has \emph{exactly
 one} reference type, namely |IORef|.  Second, as a result, it is
extremely easy to write programs with ambiguous typings, such as
\begin{code}
readAndPrint :: IO ()
readAndPrint = do { r <- newRef 'x'; v <- readRef r; print v }
\end{code}
We know, from the type signature, 
that the computation is performed in the |IO| monad,
but type checker cannot select the type of |r|, since
the |IO| monad could have reference cells of many different types. Therefore,
we must annotate~|r| with its
type explicitly. Types are no longer lightweight when they
have to be explicitly specified even for such a simple function.

The standard solution to the second problem
is to use a \emph{functional dependency}:
\begin{code}
  class Mutation m r | m -> r where ...
\end{code}
The ``|m -> r|'' part says that every |m| is related to at most one~|r|.
Functional dependencies have become a much-used extension of Haskell,
and we return to a brief comparison in Section~\ref{s:related}.
Meanwhile, the main purpose of this paper is to explain an alternative approach
in which we express the functional dependency at the type level
in an explicitly functional way.

\subsection{Declaring an associated type} \label{s:mutation}

The class |Mutation| does not \emph{really} have two type parameters: it has 
one type parameter, associated with another type that is functionally dependent.  Type families
allow one to say this directly:
\VerbatimInput[firstline=-- Start basic,lastline=-- End basic]{Mutation.hs}
The |class| declaration now introduces a \emph{type function} |Ref| 
(with a specified kind) alongside the usual \emph{value functions}
such as |newRef| (each with a specified type).
Similarly, each |instance| declaration contributes a clause 
defining the type function at the instance type alongside a witness 
for each value function.

We say that |Ref| is a \emph{type family}, or an \emph{associated type} 
of the class |Mutation|.  It behaves like a function at the type
level, so we also call |Ref| a \emph{type function}.
Applying a type function uses the same syntax as applying a type
constructor: |Ref m a| above means to apply the type function |Ref|
to~|m|, then apply the resulting type constructor to~|a|.  

The types of |newRef| and |readRef| are now more perspicuous:
\begin{code}
newRef  :: Mutation m => a -> m (Ref m a)
readRef :: Mutation m => Ref m a -> m a
\end{code}
Furthermore, 
by omitting the functionally determined type parameter from |Mutation|, 
we avoid
the ambiguity problem exemplified by |readAndPrint| above.
When performing type inference for |readAndPrint|, the type of |r| is
readily inferred to be |Ref IO Char|, which the type checker reduces
to |IORef Char|.
In general, the type
checker reduces |Ref IO| to |IORef|, and |Ref (ST s)| to |STRef s|.

These type equalities aside, 
|Ref| behaves like any other type constructor,
and it may be used freely in type signatures and data type declarations.
For example, this declaration is fine:
\begin{code}
data T m a = MkT [Ref m a]
\end{code}
% 
% The value members of the class, such as |newRef|, witness the type-level
% association between |m| and |Ref m|.  However, unlike with
% multiparameter type classes, a type function can be applied without its
% class constraint in the context.  A trivial example is that the identity
% function has the type |Ref m a -> Ref m a| without |Mutation m =>| in
% front, because the definition |id x = x| does not use any value member
% of the |Mutation| class.

\subsection{Arithmetic}

In the class |Mutation| of Section~\ref{s:mutation},
we used an associated type to avoid a two-parameter type class, but that is 
not to say that associated types obviate multiparameter type
classes. By declaring associated types in multiparameter type classes,
we introduce type functions that take multiple arguments.
One compelling use of such type functions is to make type coercions implicit,
especially in arithmetic.  Suppose we want to be able to write |add a b|
to add two numeric values |a| and~|b| even if one is an |Integer| and the
other is a |Double| (without writing |fromIntegral| explicitly). We also want to
add a scalar to a vector represented by a list
without writing |repeat| explicitly to coerce the scalar to the
vector type. The result type should be the simplest that is compatible
with both operands.  We can express this intent using a two-parameter
type class, whose parameters are the argument types of |add|, and whose
associated type |SumTy| is the result:
\VerbatimInput[firstline=-- Start basic,lastline=-- End basic]{Coercion.hs}
In other words, |SumTy| is a two-argument type function that
maps the argument types of an addition to type of its result.
The three instance declarations explain how |SumTy| behaves on
arguments of various types.  We can then write 
|add (3::Integer) (4::Double)|
to get a result of type |SumTy Integer Double|, which is
the same as |Double|.

The same technique lets us conveniently build homogeneous lists out of
heterogeneous but compatible components:
\VerbatimInput[firstline=-- Start Cons,lastline=-- End Cons]{Coercion.hs}
With instances of this class similar to those of the class
|Add|, we can |cons| an |Integer| to a list of |Double|s
without any explicit conversion.

\subsection{Graphs}

\Citet{garcia-etal:comp-generic}  
compare the support for
generic programming offered by Haskell, ML, C++, C\#, and Java.
They give a table of qualitative
conclusions, in which Haskell is rated favourably in all respects except
associated types.  This observation
was one of the motivations for the work we describe here.
Now that GHC supports type functions, we can express their main
example, but we need an additional kind of associated type,
introduced with the |data| keyword, which is described in Section~\ref{s:assoc-data}
below: 
\VerbatimInput[firstline=-- Start]{Graph.hs}
The class |Graph| has two associated types, |Vertex| and |Edge|.
We show two representative instances. In |G1|, a graph is represented by
a list of its edges, and a vertex is represented by an |Int|.
In |G2|, a graph is represented by a mapping from
each vertex to a list of its immediate neighbours, a vertex is represented by
a |String|, and an |Edge| stores a weight (of type |Int|) as well as its end-points.  
As these instance declarations illustrate,
the declaration of a |Graph| instance is free to use the type functions |Edge|
and |Vertex|.

\subsection{Associated data types} \label{s:assoc-data}

The alert reader will notice in the class |Graph| that
the associated type for |Edge| is declared 
using ``|data|'' rather than ``|type|''.
Correspondingly, the |instance| declarations 
give a |data| declaration for |Edge|,
complete with data constructors |MkEdge1| and |MkEdge2|.
The reason for this use of |data| is somewhat subtle.  

A type constructor
such as~|Maybe| expresses a functional relation between types that
is \emph{injective}, mapping different argument types to
different results. For example, if a function takes an argument of type |Maybe t1|
and the argument has type |Maybe t2|, then |t1| and |t2| must be equal.
(A function $f$ is injective iff $f(x)=f(y) \Rightarrow x=y$.)
This
injectivity does not generally hold for type functions.
Consider this function to find the
list of vertices adjacent to the given vertex |v| in the graph |g|:
\begin{code}
neighbours g v = map tgt (outEdges g v)
\end{code}
We expect GHC to infer the following type:
\begin{code}
neighbours :: Graph g => g -> Vertex g -> [Vertex g]
\end{code}
Certainly, |outEdges| returns a |[Edge g1]| (for some type |g1|),
and |tgt| requires its argument to be of type |Edge g2| (for some type |g2|).
So, GHC's type checker requires that $\mathtt{Edge~ g1}\sim\mathtt{Edge~
  g2}$, where ``$\sim$'' means type equality.%
\footnote{``$=$'' is used for too many other things.}
Does that mean
that $\mathtt{g1}\sim\mathtt{g2}$, as intuition might suggest?  
Only if |Edge| is and associated |data| type.
If |Edge| were an associated
|type|, rather than |data|, we could have written these instances:
\begin{code}
instance Graph G3 where
  type Edge G3 = (Int,Int)
instance Graph G4 where
  type Edge G4 = (Int,Int)
\end{code}
so that $\mathtt{Edge~G3}\sim\mathtt{Edge~G4}$ even though |G3| and |G4| are distinct.
In that case, the inferred type of |neighbours| would be:
\begin{code}
neighbours :: (Graph g1, Graph g2, Edge g1 ~ Edge g2)
           => g1 -> Vertex g1 -> [Vertex g2]
\end{code}
Although correct,
this type is more general and complex than we want.
By declaring |Edge|
with |data|, we specify that |Edge| is injective,
that $\mathtt{Edge~g1}\sim\mathtt{Edge~ g2}$ indeed implies
$\mathtt{g1}\sim\mathtt{g2}$.  
GHC then infers the simpler type we want.

Why is |Edge| injective?  Consider these two sets of declarations.
\begin{code}
class Graph g where           | class Graph g where
  data Edge g                 |    type Edge g
                              |
instance Graph G5 where       | instance Graph G5 where
  data Edge G5 = A | B Int    |   type Edge G5 = EdgeG5
                              |
                              | data EdgeG5 = A | B Int
\end{code}
The left hand column declares |Edge| as an associated |data| type, while
the right hand column shows how do very-nearly-the-same thing using
an associated |type| synonym instead.
In the right hand column, the |instance| declaration 
defines |(Edge G5)| to be a fresh, arbitrarily-named, top-level data 
type |EdgeG5|.  If we invent a fresh data type for every such instance declaration,
then of course the type function 
|Edge| will be injective.  The |data| notation is simply syntactic
sugar that enforces this freshness, and hence guarantees injectivity.

In GHC, |type| families cannot be be guaranteed injective, even though in practice
they sometimes are.
A possible extension, not currently implemented, would be to 
allow the programmer optionally to specify (at the point of declaration) that 
an associated |type| synonym is injective,
and to \emph{check} that this property is maintained as each |instance| is added.

\subsection{Type functions are open} \label{s:open}

Value-level functions are \emph{closed} in the sense that
they must be defined all in one place.  For example, if one defines
\begin{code}
length :: [a] -> Int
\end{code}
then one must give the \emph{complete} definition of |length| in a single place:
\begin{code}
length []     = 0
length (x:xs) = 1 + length xs
\end{code}
It is not legal to put the two equations in different modules.

In contrast, a key property of type functions is that, 
like type classes themselves,
they are \emph{open} and can be extended with additional instances at any time.
For example, if next week we define
a new type |Age|, we can extend |SumTy| and |add| to work over |Age|
by adding an instance declaration:
\begin{code}
newtype Age = MkAge Int

instance Add Age Int where
  type SumTy Age Int = Age
  add (MkAge a) n = MkAge (a+n)
\end{code}
We thus can add an |Int| to an |Age|, but not an |Age| or |Float| to
an |Age| without another instance.
% \oleg{that is a good point, yet it is easily
%   circumvented if we difine the instance for Add for types Age and
%  Float. Perhaps we should say: critically, if one avoids defining
%   the instance for adding Age and Float, one hereby defines a
%   statically enforceable constraint that the values of the type Age
%   and Float cannot be added.}
% \simon{I added an ``...assuming...'', but I don't want to get too 
% deep into abstract data types.} 

\subsection{Type functions may be recursive} \label{s:recursive}

Just as the instance for |Show [a]| is defined in terms of |Show a|,
a type function is often defined by structural recursion on the input
type.  Here is an example, extending our earlier |Add| class with a new
instance:
\VerbatimInput[firstline=-- Start recursive,lastline=-- End recursive]{Coercion.hs}
Thus
\[
\mathtt{SumTy~Integer~[Double]} \enspace\sim\enspace
\mathtt{[SumTy~Integer~Double]} \enspace\sim\enspace
\mathtt{[Double]}.
\]
% 
% (To avoid the ambiguity of overlapping
%instances, we cannot define a general instance for |Add scalar [a]|;
% after all, there are two ways to add a vector to a matrix.)  

In a similar way, we may extend the |Mutation| example of
Section~\ref{s:mutation} to \emph{monad transformers}.
Recall that a monad transformer |t :: (*->*) -> (*->*)|
is a higher-order type constructor that takes a monad |m| into
another monad |t m|.
\begin{code}
class MonadTrans t where
  lift :: Monad m => m a -> t m a
\end{code}
At the value level, |lift| turns a monadic computation
(of type |m a|) into one in the transformed monad (of type |t m a|).
Now, if a monad |m| is an instance of |Mutation|, then we can make
the transformed monad |t m| into such an instance too:
\VerbatimInput[firstline=-- Start transformer]{Mutation.hs}
The equation for |Ref| says that the type of references in the transformed
monad is the same as that in the base monad.

\section{Optimised container representations}
\label{s:optimised}

A common optimisation technique is to represent data of different
types differently (rather than uniformly as character strings, for
example). This technique is best known when applied to container data.
For example, we can use the same array container to define a |Bool|
array and to define an |Int| array, yet a |Bool|
array can be stored more compactly and negated elementwise faster
when its elements are tightly packed as a bit vector.
C++ programmers use template meta-programming
to exploit this idea to great effect, for example in the Boost library
\cite{siek-etal:boost}.
The following examples show how to express the same idea in
Haskell, using type functions to map among the various concrete types
that represent the same abstract containers.

\subsection{Type-directed memoization}
\label{s:memo}

To memoise a function is to improve its future performance by recording
and reusing its past behaviour in a \emph{memo table} \cite{michie-memo}.
The memo table augments the concrete representation of the function
without affecting its abstract interface.
A typical
way to implement memoization is to add a lookup from the table on entry
to the function and an update to the table on exit from the function.
Haskell offers an elegant way to express memoization, because
we can use lazy evaluation to manage the lookup and update of the memo
table.  But type functions offer a new possibility:
\emph{the type of the memo table can be determined
automatically from the argument type 
of the memoised function}
\cite{hinze-generalizing,elliott:memo-functions}.

We begin by defining a type class |Memo|.  The constraint |Memo a| means that the
behaviour of a function from an argument type |a| to a result type~|w| can be represented as
a memo table of type |Table a w|, where |Table| is a type function that
maps a type to a constructor.

% Because |Table a| is declared using
% |data| rather than |type|, the type checker knows that if |Table a| and
% |Table b| are equal then |a| and |b| are also equal.
% [Can we motivate more strongly this use of associated constructors
% (i.e., what doesn't work if we were to use associated constructor
% synonyms)? ]
\VerbatimInput[firstline=-- Start class,lastline=-- Stop class]{Memo.hs}
For example, we can memoise any function from |Bool| by storing its two
return values as a lazy pair.  This lazy pair is the memo table.
\VerbatimInput[firstline=-- Start Bool,lastline=-- Stop Bool]{Memo.hs}
To memoise a function |f :: Bool -> Int|, we simply replace it by |g|:
\begin{code}
g :: Bool -> Int
g = fromTable (toTable f)
\end{code}
The first time |g| is applied to |True|, the Haskell implementation
computes the first component of the lazy pair (by applying |f| in turn
to |True|) and remembers it for future reuse.  Thus, if |f| is defined
by
\begin{code}
f True  = factorial 100
f False = fibonacci 100
\end{code}
then evaluating |(g True + g True)| will take barely half as much time as
evaluating |(f True + f True)|.

Generalising the |Memo| instance for |Bool|
above, we can memoise functions from any sum type, such as the
standard Haskell type |Either|:
\begin{code}
data Either a b = Left a | Right b
\end{code}
We can memoise a function from |Either a b| by 
storing a lazy pair of a memo table from~|a| and a memo table from~|b|.  
That is, we take advantage of the isomorphism
between the function type |Either a b -> w| and the product type |(a -> w, b -> w)|.
\VerbatimInput[firstline=-- Start sum,lastline=-- Stop sum]{Memo.hs}
Of course, we need to memoise functions from~|a| and
functions from~|b|; hence the ``|(Memo a, Memo b) =>|'' part of the
declaration.
Dually, we can
memoise functions from the product type |(a,b)| by storing
a memo table from~|a| whose entries are memo tables from~|b|.
That is, we take advantage of the currying isomorphism between the
function types
|(a,b) -> w| and |a -> b -> w|.
\VerbatimInput[firstline=-- Start product,lastline=-- Stop product]{Memo.hs}

\subsection{Memoisation for recursive types}

What about functions from recursive types, like lists?  No problem!  A list is a combination
of a sum, a product, and recursion:
\VerbatimInput[firstline=-- Start list,lastline=-- Stop list]{Memo.hs}
As in Section~\ref{s:memo}, the type function |Table| is
recursive. Since a list is either empty or not, |Table [Bool] w|
is represented by a pair (built with the data constructor |TList|), 
whose first component is
the result of applying the memoised function~|f| to the empty list,
and whose second component memoises applying~|f| to
non-empty lists.  A non-empty list |(x:xs)| belongs to a
product type, so the corresponding table maps each~|x| to a table that deals 
with~|xs|. We merely combine the memoization of functions
from sums and from products.

It is remarkable how laziness takes care of the recursion in the
type~|[a]|.  A memo table for a function~|f| maps \emph{every possible
argument} |x| of |f| to a result |(f x)|.  When the argument type is
finite, such as |Bool| or |(Bool,Bool)|, the memo table is finite as
well, but what if the argument type is infinite, such as |[Bool]|?
Then, of course, the memo table is infinite: in the instance declaration
above, we define |toTable| for~|[a]| not only using |toTable| for~|a|
but also using |toTable| for~|[a]| recursively.  Just as each value
|(f x)| in a memo table is evaluated only if the function is ever
applied to that particular~|x|, so each sub-table in this memo table is
expanded only if the function is ever applied to a list with that prefix.
So the laziness works at two distinct levels.

Now that we have dealt with sums, products, and recursion, we can deal with
any data type at all.  Even base types like |Int| or |Integer| can be handled by first 
converting them (say) to a list of digits, say |[Bool]|. Alternatively,
it is equally easy to give a specialised instance for |Table Integer| that uses
some custom (but infinite!)\ tree representation for |Integer|.

More generally, if we define |Memo| instances~-- once and for all~-- for
sum types, product types, and fixpoint types, then we can define a
|Memo| instance for some new type just by writing an isomorphism between
the new type and a construction out of sum types, product types, and
fixpoint types. These
boilerplate |Memo| instances can in fact be defined generically, with
the help of functional dependencies \cite{cunha-framework} or type
functions.%
\footnote{\url{http://hackage.haskell.org/cgi-bin/hackage-scripts/package/pointless-haskell}}

\begin{comment}
perhaps the most compelling example of type families that I
have seen. The example is quite specialised however, and requires
quite a bit of explanation (of catamorphisms and hylomorphisms).

From: Hugo Pacheco <hpacheco@gmail.com>
Date: Fri, 05 Dec 2008 23:18:37 +0000

Pointless Haskell a library for point-free programming with recursion
patterns that uses type synonym families to provide a view of data types as
the fixed points of  functors.
It defines two type functions

type family PF a :: * -> *             -- returns the pattern functor for a
data type
type family Rep (f :: * -> *) x :: *  -- returns the result type of applying
a functor to a type argument

that can be combined to derive the structurally equivalent sum of products
for some type:

type F a x = Rep (PF a) x

class Mu a where
    inn :: F a a -> a
    out :: a -> F a a

For Haskell polymorphic lists, we need to define:

type instance PF [a] = Const One :+: Const a :*: Id

instance Mu [a] where
    inn (Left _) = []
    inn (Right (x,xs)) = x:xs
    out [] = Left _L
    out (x:xs) = Right (x,xs)

Some of the typical recursion patterns are:

hylo :: Functor (PF b) => b -> (F b c -> c) -> (a -> F b a) -> a -> c
cata :: (Mu a,Functor (PF a)) => a -> (F a b -> b) -> a -> b
ana :: (Mu b,Functor (PF b)) => b -> (a -> F b a) -> a -> b

One simple example is the foldr (catamorphism) for calculating the length of
a list:

length :: [a] -> Int
length = cata (_L::[a]) f
    where f = zero \/ succ . snd

> length [1,2,3,4]
4


I have promoted the library into a cabal package (pointless-haskell) today
and am creating an homepage (
http://haskell.di.uminho.pt/wiki/Pointless+Haskell) with examples.
\end{comment}

\begin{comment}
Because we have only considered first-order argument types in the
memoization so far, it is actually not necessary for the |Memo| class to
expose the types of memo tables.  The functions |fromTable| and
|toTable| can be fused into a single function |memo| with the type of
the identity function:
\begin{code}
class Memo a where memo :: (a -> w) -> (a -> w)
\end{code}
However, when it comes to memoizing functions that take functions as
input, it becomes more important to expose the types of memo tables.
We will not discuss how to memoise such higher-order functions in this
paper, but the first step is to view the memoised function and its
argument as a pair of communicating processes, a view we turn to next.
\simon{Where is memoing higher-order functions this discussed??}
\oleg{We won't discuss it in the paper, although Ken has the code...}
\simon{I meant ``what can we cite?''.  If it's new stuff, maybe you can
put a blog post?  Or we could make it an Appendix to this paper, published
with the online version?}
\ken{I'll write the blog post.}
\end{comment}

\subsection{Generic finite maps}
\label{s:map}

A \emph{finite map} is a partial function from a domain of \emph{keys}
to a range of \emph{values}.  Finite maps can be represented using many
standard data structures, such as binary trees and hash tables, that
work uniformly across all key types.  
However, our memo-table development suggests another possibility,
that of representing a finite map using a memo table:
\begin{code}
type Map key val = Table key (Maybe val)
\end{code}
That is, we represent a \emph{partial} function from |key| to |val|
as a \emph{total} function from |key| to |Maybe val|.
But we get two problems. The smaller one is that whereas |Table|
did not need an |insert| method~-- once we construct the memo table, 
we never need to update it~-- |Map| needs |insert|
and many other methods including |delete| and |union|.
These considerations might lead us to add |insert|, |delete|, etc.\
to the |Table| interface, where they appear quite out of place.
A nicer alternative would be to define a sub-class of |Table|.

The second, more substantial problem is that |Table| is unnecessarily
inefficient in the way it represents keys that map to |Nothing|.
An extreme case is an \emph{empty} map whose key type is |Integer|.
An efficient finite map would represent an empty map as an empty trie,
so that the |lookup| operation returns immediately with |Nothing|. 
If instead we represent the
empty map as an (infinite) |Table| mapping every |Integer| to |Nothing|,
each lookup will explore a finite path in the potentially infinite tree, 
taking time proportional the number of bits in the |Integer|.  
Furthermore, looking up many |Integer|s in such a |Table| would 
force many branches of the |Table|, producing a large tree in memory, 
with |Nothing| in every leaf!
Philosophically, it seems nicer to distinguish the mapping of a key
to |Nothing| from the \emph{absence} of the mapping for that key. 

For these reasons, it
makes sense to implement Map afresh \cite{hinze-generalizing,hinze-etal:tidata}.
As with |Memo|, we define a class |Key| and an associated data type |Map|:
\VerbatimInput[firstline=-- Start class,lastline=-- Stop class]{Map.hs}
Now the instances follow in just the same way as before:
\VerbatimInput[firstline=-- Start instances,lastline=-- Stop instances]{Map.hs}
The fact that this is a \emph{finite} map makes the instance for |Int| easier than
before,
because we can simply invoke an existing data structure (a Patricia 
tree, for example) for finite maps keyed by |Int|:
\VerbatimInput[firstline=-- Start int,lastline=-- Stop int]{Map.hs}
Implementations of other methods (such as |insert| and |union|) and
instances at other types (such as lists) are left as exercises for the reader. 

Hutton describes another example with the same flavour \cite{hutton:paramorphism}.

% Similarly, we can put type synonyms inside type classes to define type
% functions that map
% \begin{itemize}
% \item collection types to the types of their elements \cite{jones-type,chakravarty-synonyms},
% \item 
% \item graph types to the types of their nodes and edges \cite{garcia-extended}.
% \end{itemize}
% \simon{I do not understand the paragraph that follows.  What does
% ``especially useful'' mean?  Isn't the Ref stuff above just such a case?}
% It is especially useful to define these mappings as type functions when
% the primary type is not polymorphic in the associated type so we cannot
% just define a type constructor that maps the associated type to the
% primary type.  For example, the element type of a bit vector must be
% |Bool|, and the node type of an adjacency matrix must be an array index
% type like |Integer|, so it does not make sense to define bit vectors or
% adjacency matrices as type constructors that apply to |Bool| or
% |Integer|.


\subsection{Session types and their duality}

We have seen a recursively defined correspondence between the
type of keys and the type of a finite map over those keys.
The key and the lookup function of a finite map can be
regarded as a pair of \emph{processes} that communicate in a particular way:
the key sends indices to the lookup, then the lookup responds with
the element's value.  
In this section, we generalise this correspondence to the relationship
between a pair of processes
that communicate with each other by sending and receiving values in
a \emph{session}.   

For example, consider the following definitions:
\VerbatimInput[firstline=-- Start init,lastline=-- Stop init]{Session.hs}
The function-like value |add_server| accepts two |Int|s in succession,
then prints ``Thinking'' before responding with an |Int|, their sum.
We call |add_server| a \emph{process}, whose interface protocol
is specified by its type -- so called \emph{session type}.
We write session types explicitly in
this section, but they can all be inferred.

We may couple two processes whose protocols are
complementary, or \emph{dual}:
\VerbatimInput[firstline=-- Start class,lastline=-- Stop class]{Session.hs}
Of course, to write down the definition of |run| we must also say what it
means to be dual.  Doing so is straightforward:
\VerbatimInput[firstline=-- Start instances,lastline=-- Stop instances]{Session.hs}
The type system guarantees that the protocols of the two processes match.
Thus, if we write a suitable client |add_client|, like
\VerbatimInput[firstline=-- Start add_client,lastline=-- Stop add_client]{Session.hs}
we may couple them
(either way around):
\begin{code}
> run add_server add_client
Thinking
Waiting
7
> run add_client add_server
Thinking
Waiting
7
\end{code}
However, |run| will not allow us to couple two processes that do not
have dual protocols. Suppose that we write a negation server:
\VerbatimInput[firstline=-- Start neg_server,lastline=-- Stop neg_server]{Session.hs}
Then |(run add_client neg_server)| will fail with a type error.
Just as the |Memo| class represents functions of type |a -> w| by memo
tables of the matching type |Table a w|, this |Session| class represents
consumers of type |a -> IO ()| by producers of the matching type |Dual a|.

These protocols do not allow past communication to affect the type and
direction of \emph{future} exchanges.  For example, it seems impossible to write
a well-typed server that begins by receiving a |Bool|, then performs
addition if |True| is received and negation if |False| is received.
However, we can express a protocol that chooses
between addition and negation (or more generally, a protocol that
chooses among a finite number of ways to continue).  We simply treat
such a binary choice as a distinct sort of protocol step.  The receiver
of the choice has a product type, whereas the sender has a sum type:
\VerbatimInput[firstline=-- Start choice,lastline=-- Stop choice]{Session.hs}
These additional instances let us define a combined addition-negation
server, along with a client that chooses to add.  The two new processes
sport (inferable) types that reflect their initial choice.
\VerbatimInput[firstline=-- Start combined,lastline=-- Stop combined]{Session.hs}
To connect |server| and |client|, we can evaluate either
|run server client| or |run client server|.
The session type of the client hides which of the two choices
the client eventually selects; the choice may depend on user input at run time, which
the type checker has no way of knowing. The type checker does
statically verify that the corresponding server can handle either choice.


With the instances defined above, each protocol allows only a finite
number of exchanges, so a server cannot keep looping until the client
disconnects.  This restriction is not fundamental: recursion in
protocols can be expressed, for example using an explicit fixpoint
operator at the type level \cite{pucella-tov:session-types}.

We can also separate the notion of a \emph{process} from
that of a \emph{channel}, and associate a protocol with the channel
rather than the process.  This and other variants have been explored
in other works
\cite{imai-session,pucella-tov:session-types, neubauer-implementation,sackman:session-types,ingram:session-types},
from which we draw the ideas of
this section in a simplified form.


In principle, we can require that |Dual| be an involution (that is,
|Dual| be its own inverse) by adding a \emph{equality constraint} as
a superclass of |Session|:
\begin{code}
class (Dual (Dual a) ~ a) => Session a where ...
\end{code}
We can then invoke |run| on a pair of processes without worrying about
which process is known to be the dual of which other process.
More generally, this technique lets us express bijections between types.
However, such equality superclasses are not yet implemented in the 
latest release of GHC (6.10).

\begin{comment}
Manuel pointed out how to encode bijections between types using type families:

class (T1 a ~ b, T2 b ~ a) => C a b where
  type T1 a
  type T2 b

instance C IPHeader IPAddress where
  type T1 IPHeader = IPAddress
  type T2 IPAddress = IPHeader

-------
class (T1 a ~ b, T2 b ~ a) => C a b
instance C IPHeader IPAddress
type family T1 a
type family T2 a
type instance T1 IPHeader = IPAddress
type instance T2 IPAddress = IPHeader

This setup will allow
    type instance T1 Int = Bool
    type instance T2 Bool = Char
but of course the constraint "C Int Bool" won't be satisfied.
\end{comment}

\section{Typed sprintf and sscanf}

We conclude the first half of the paper, about using type functions to
accommodate more good programs, with a larger example:
typed |sprintf| and |sscanf|.

A hoary chestnut for typed languages is the definition of |sprintf| and |sscanf|.
Although these handy functions are present in many languages (such as C and Haskell),
they are usually not type-safe: the type checker does
not stop the programmer from passing to |sprintf| more or fewer arguments
than required by the format descriptor.
The typing puzzle is that
we want
the following to be true:
\begin{code}
sprintf "Name=%s"         :: String -> String
sprintf "Age=%d"          :: Int -> String
sprintf "Name=%s, Age=%d" :: String -> Int -> String
\end{code}
That is, the \emph{type} of |(sprintf fs)| depends on the \emph{value} of
the \emph{format descriptor} |fs|.  Supporting such dependency directly requires a full-spectrum
dependently typed language, but there is a small literature of neat techniques
for getting close without such a language \cite{danvy-unparsing,hinze-formatting,asai:printf}.
Here we show one technique using type families. 
In fact, we accomplish something
more general: typed |sprintf| and |sscanf| \emph{sharing the same
format descriptor}.
Typed |sprintf| has received a lot more attention than typed
|sscanf|, and it is especially rare for an
implementation of both to use the same
format descriptor.

\subsection{Typed sprintf}

We begin with two observations:
\begin{itemize}
\item Format descriptors in C are just strings, which leaves the door wide
open for malformed descriptors that |sprintf| does not recognise
(e.g., |sprintf "%?"|).
The language of format descriptors is a small domain-specific language,
and the type checker should reject ill-formed descriptors.
\item 
In Haskell, we cannot make the type of |(sprintf f)| depend on the value of 
the format descriptor~|f|.  However,  using type functions, we can make 
it depend on the \emph{type} of |f|.  
\end{itemize}
Putting these two observations together suggests that we use a 
now-standard design pattern: a domain-specific language expressed using a 
generalised algebraic data type (GADT) indexed by a type argument.  Concretely,
we can define the type of format descriptors |F| as follows:
\VerbatimInput[firstline=-- Start fmt,lastline=-- Stop fmt]{PrintScanGADT.hs}
So |F| is a GADT with three constructors, |Lit|, |Val|, 
and |Cmp|.\footnote{``|Cmp|'' is short
for ``compose''.}
Our intention is that |(sprintf f)| should behave as follows:
\begin{itemize}
\item If |f| = |Lit s|, then print (that is, return as the output
  string) |s|.
\item If |f| = |Cmp f1 f2|, then print according to descriptor |f1| and continue 
according to descriptor |f2|.
\item If |f| = |Val r p|, then use the printer |p| to convert the first
argument to a string to print.  (The |r| argument is used for parsing
in Section~\ref{s:scanf} below.)
\end{itemize}
If |fmt :: F ty|, then the \emph{type} |ty| encodes the \emph{shape}
of the term |fmt|.  For example, given |int :: F (V Int)|,
we may write the following format descriptors:
\begin{code}
f_ld  = Lit "day"                            :: F L
f_lds = Cmp (Lit "day") (Lit "s")            :: F (C L L)
f_dn  = Cmp (Lit "day ") int                 :: F (C L (V Int))
f_nds = Cmp int (Cmp (Lit " day") (Lit "s")) :: F (C (V Int) (C L L))
\end{code}
In each case, the type encodes an abstraction of the value.
(We have specified the types explicitly, but they can be inferred.)
The types |L|, |V|, and |C| are type-level abstractions of the terms |Lit|, |Val|, and |Cmp|.
These types are uninhabited by any value, but they index values in the
GADT~|F|, and they are associated with other, inhabited types by two
type functions. We turn to these type functions next.

We want an interpreter |sprintf| for this domain-specific language,
so that:
\begin{code}
sprintf :: F f -> SPrintf f
\end{code}
where |SPrintf| is a type function that transforms the (type-level) format 
descriptor |f| to the type of |(sprintf f)|.  For example, the following should all work:
\begin{code}
sprintf f_ld         -- Result: "day"
sprintf f_lds        -- Result: "days"
sprintf f_dn 3       -- Result: "day 3"
sprintf f_nds 3      -- Result: "3 days"
\end{code}
It turns out that the most convenient approach
is to use continuation-passing style, at both the
type level and the value level.  At the type level,
we define |SPrintf| above using an auxiliary type function |TPrinter|.
Because |TPrinter| has no accompanying value-level operations,
a type class is not needed.  Instead, GHC allows the type
function to be defined directly, like this:\footnote{
GHC requires the alarming flag |-XAllowUndecidableInstances|
to accept the |(C f1 f2)| instance for |TPrinter|, because
the \emph{nested} recursive call to |TPrinter| does not ``obviously
terminate''.  Of course, every call to |TPrinter| does
terminate, because the second argument (where the nested recursive call is made)
is not scrutinised by any of the equations, but this is a non-local property that
GHC does not check.  The flag promises the compiler that |TPrinter| will
terminate; the worst that can happen if the programmer makes an erroneous promise is
that the type checker diverges.}
\VerbatimInput[firstline=-- Start TPrinter,lastline=-- Stop TPrinter]{PrintScanGADT.hs}
So |SPrintf| is actually just a vanilla type synonym, which calls the 
type function |TPrinter| with second parameter |String|.  Then |TPrinter|
transforms the type as required.  For example:
\begin{center}\begin{tabular}{rcl}
|SPrintf (C L (V Int))| & $\sim$ & |TPrinter (C L (V Int)) String| \\
 & $\sim$ & |TPrinter L (TPrinter (V Int) String)| \\
 & $\sim$ & |TPrinter (V Int) String| \\
 & $\sim$ & |Int -> String|
\end{tabular}\end{center}
At the value level, we proceed thus:
\VerbatimInput[firstline=-- Start printer,lastline=-- Stop printer]{PrintScanGADT.hs}
It is interesting to see how |printer| type-checks.
Inside the |Lit| branch, for example, we know that |f| is~|L|, and hence
that the desired result type |TPrinter f a| is |TPrinter L a|, or just~|a|.
Since |k str :: a|, the actual result type matches the desired one. Similar
reasoning applies to the |Val| and |Cmp| branches.

\subsection{Typed sscanf}
\label{s:scanf}

We can use the same domain-specific language of format descriptors
for parsing as well as printing.  That is, we can write
\begin{code}
sscanf :: F f -> SScanf f
\end{code}
where |SScanf| is a suitable type function.  For example, reusing the
format descriptors defined above, we may write:
\begin{code}
sscanf f_ld  "days long"   -- Result: Just ((), "s long")
sscanf f_ld  "das long"    -- Result: Nothing
sscanf f_lds "days long"   -- Result: Just ((), " long")
sscanf f_dn  "day 4."      -- Result: Just (((),4), ".")
\end{code}
In general, |sscanf f s| returns |Nothing| if the parse fails, and |Just (v,s')|
if it succeeds, where |s'| is the unmatched remainder of the input string,
and |v| is a (left-nested) tuple containing the parsed values.
The details are now fairly routine:
\VerbatimInput[firstline=-- Start parser,lastline=-- Stop parser]{PrintScanGADT.hs}

\subsection{Reflections}

We conclude with a few reflections on the design.
\begin{itemize}
\item Our |Val| constructor makes it easy to add printers for
new types.  For example:
\VerbatimInput[firstline=-- Start Dollars,lastline=-- Stop Dollars]{PrintScanGADT.hs}

\item Our approach is precisely that of Hinze \cite{hinze-formatting},
except that we use type functions and GADTs (unavailable when
Hinze wrote) to produce a much more elegant result.

\item It is (just) possible to take the domain-specific-language approach
\emph{without} using type functions, albeit with less clarity and greater
fragility \cite{kiselov:printf-gadt}.

\item Defining |F| as a GADT makes it easy to define new interpreters
beyond |sprintf| and |sscanf|, but hard to add new
format-descriptor combinators.  A dual approach
\cite{krishnamurthi-synthesizing}, which 
makes it easy to add new descriptors but hard to define new interpreters,
is to define |F| as a record of operations:
\begin{code}
data F f = F {
  printer :: forall a. (String -> a) -> TPrinter f a,
  parser  :: forall a. a -> String 
                         -> Maybe (TParser f a, String) }
\end{code}
Instead of being a GADT, |F| becomes a higher-rank data constructor~-- that is,
its arguments are polymorphic functions.
The type functions |TPrinter| and |TParser| are unchanged.
The format-descriptor combinators are no longer data constructors but
ordinary functions instead:
\begin{code}
lit :: String -> F I
lit str = F { printer = \k -> k str,
              parser  = parseLit str }

int :: F (V Int)
int = F { printer = \k i -> k (show i),
          parser  = parseVal reads }
\end{code}

\item
If we consider only |sprintf| or only |sscanf|, then the type-level format
descriptor is the result of \emph{defunctionalizing} a type-level
function, and |TPrinter| or |TParser| is the \emph{apply function}
\cite{reynolds-definitional-notes,danvy-defunctionalization}.
Considering |sprintf| and
|sscanf| together takes format descriptors out of the image of
defunctionalization.
\end{itemize}

In general, type functions let us easily express a parser that operates on
types (and produces corresponding values).  In this way, we can overlay
our own domain-specific, variable-arity syntax onto Haskell's type system.%
\footnote{\url{http://okmij.org/ftp/Haskell/types.html#polyvar-fn}}
For example, we can concisely express  XML documents,%
\footnote{\url{http://okmij.org/ftp/Haskell/typecast.html#solving-read-show}}
\begin{comment}
**** Solving the read.show problem, generating generic XML documents:
Niklas Broberg described the problem of constructing different
realisations of XML documents from data of different types. We wish to
write p (p "foo") and specify the desired type of the XML document,
like
         (p (p "foo")) :: XMLTree
         (p (p "foo")) :: IO ()  -- for writing out the XML document
The function p obviously has to be overloaded with the type p :: a -> xml.
However, p (p "foo") exhibits the show . read problem. What should be the
result type of the inner invocation of p?
    See Niklas Broberg's final implementation: the goal is to use the
    same xml code on the Web server and on the client. On the client,
    JavaScript is generated.
\end{comment}
linear algebra,%
\footnote{\url{http://okmij.org/ftp/Haskell/typecast.html#is-function-type}}
\begin{comment}
**** IsFunction: vector spaces of functions
The original problem by Jerzy Karczmarczuk: quantum abstract computations
         data Vec a = Vec (Array Int a) Int
         class Product a b c | a b -> c where
             (<*>) :: a -> b -> c
         instance (Num a) => Product a (Vec a) (Vec a) where
             (<*>) num (Vec a s) = Vec (fmap (* num) a) s
         test = 10 <*> (vector 10 [0..9])
\end{comment}
and even keyword arguments.%
\footnote{\url{http://okmij.org/ftp/Haskell/keyword-arguments.lhs}}

\section{Fun with phantom types}
\label{s:phantom}

Each type function above returns types that are actually used in the
value-level computations.  In other words, type functions are necessary
to type-check the overloaded functions above.  For example, it is
thanks to the type function |Ref| that the value functions |newIORef|
and |newSTRef| can be overloaded under the name |newRef|.  In contrast,
this section considers type functions that operate on 
so-called \emph{phantom types}.

Phantom types enforce distinctions among values with the same run-time
representation, such as numbers with different units \cite{kennedy-dimensions}
and strings for different XML elements.  Functions on
phantom types propagate these distinctions through a static
approximation of the computation.  Phantom types and functions on
them thus let us reason more precisely about a program's behaviour
before running it, essentially by defining additional type-checking
rules that refine Haskell's built-in ones.  The reader may find 
many applications of phantom types elsewhere 
\cite{hinze:fun,fluet:phantom,fluet:datatype-spec}; our focus here is on the
additional expressiveness offered by type families~-- to exclude more bad
programs.

\subsection{Pointer arithmetic and alignment}
\label{s:arithm}

The refined distinctions afforded by phantom types are especially useful in embedded and systems
programming, where a Haskell program (or code it generates) performs low-level operations
such as direct memory access and interacts with hardware device drivers
\cite{diatchki-strongly,kiselyov-resources}.  It is easy to use phantom
types to enforce access permissions (read versus write), but we take the
example of pointer arithmetic and alignment to illustrate the power of
type functions.

Many hardware operations require pointers that are
properly aligned (that is, divisible) by a statically known small
integer, even though every pointer, no matter how aligned, is
represented by a machine word at run time.
Our goal is to distinguish the types of differently aligned
pointers and thus prevent the use of misaligned pointers.

Before we can track pointer alignment, we first need to define natural
numbers at the type level.  The type |Zero| represents~0, and if the
type |n| represents~$n$ then the type |Succ n| represents $n+1$.
\VerbatimInput[firstline=-- Start Zero Succ,lastline=-- Stop Zero Succ]{Arithm.hs}
For convenience, we also define synonyms for small type-level numbers.
\begin{code}
type One   = Succ Zero
type Two   = Succ One
type Four  = Succ (Succ Two )
type Six   = Succ (Succ Four)
type Eight = Succ (Succ Six )
\end{code}
These type-level numbers belong to a class |Nat|, whose value member
|toInt| lets us read off each number as an |Int|:
\VerbatimInput[firstline=-- Start Nat,lastline=-- Stop Nat]{Arithm.hs}
In this code, |toInt| uses a standard Haskell idiom called \emph{proxy arguments}.
As
the underscores in its |instance|s show, |toInt| never examines its argument. 
Nevertheless, it must \emph{take} an argument, as a proxy that specifies
which instance to use.  Here is how one might call |toInt|:
\begin{code}
Prelude> toInt (undefined :: Two)
2
\end{code}
We use Haskell's built-in |undefined| value, and specify that it has type |Two|,
thereby telling the compiler which instance of |Nat| to use.  
There is exactly such a call in the |(Succ n)| instance of |Nat|, only
in that case the proxy argument is given the type~|n|, 
a lexically scoped type variable.

As promised above, we represent a pointer or offset as a machine word at
run time, but use a phantom type at compile time to track how aligned we
know the pointer or offset to be.
\VerbatimInput[firstline=-- Start wrappers,lastline=-- Stop wrappers]{Arithm.hs}
Thus a value of type |Pointer n| is an |n|-byte-aligned pointer; and a value
of type |Offset n| is a multiple of |n|.  For example, a |Pointer Four| is
a 4-byte-aligned pointer. |Pointer n| is defined as a |newtype| and so
the data constructor |MkPointer| has no run-time representation.
In other words,
the phantom-type alignment annotation imposes no run-time overhead.

To keep this alignment knowledge sound, the data constructors
|MkPointer| and |MkOffset| above must not be exported for direct use by
clients.  Instead, clients must construct |Pointer| and |Offset| values
using ``smart constructors''.  One such constructor is |multiple|:
\VerbatimInput[firstline=-- Start multiple,lastline=-- Stop multiple]{Arithm.hs}
So |(multiple i)| is the |i|-th multiple of the alignment specified
by the return type.  For example, 
evaluating |multiple 3 :: Offset Four| yields |MkOffset 12|, the
|3|rd multiple of a |Four|-byte alignment.

When a pointer is incremented by an offset, the resulting pointer is
aligned by the greatest common divisor (GCD) of the alignments of the
original pointer and the offset.  
To express this fact, we define a type
function |GCD| to compute the GCD of two type-level numbers.  Actually,
|GCD| takes three arguments: |GCD d m n| computes the GCD of |d+m| and
|d+n|.  We will define |GCD| in a moment, but assuming we have it
we can define |add|:
\VerbatimInput[firstline=-- Start add,lastline=-- Stop add]{Arithm.hs}
Thus, if |p| has the type |Pointer Eight| and |o| has the type |Offset Six|,
then |add p o| has the type |Pointer Two|.  

The type checker does not check that |x + y| is indeed aligned by the GCD\@.  Like
|multiple|, the function |add| is trusted code, and its type expresses
claims that its programmer must guarantee.  Once she does so, however,
the clients of |add| have complete security.
If |fetch32| is
an operation that works on 4-aligned pointers only, then we can give it
the type
\begin{code}
(GCD Zero n Four ~ Four) => Pointer n -> IO ()
\end{code}
In words, |fetch32| works on any
pointer whose alignment's GCD with~4 is~4.  It is then a type error to
apply |fetch32| to |add p o|, but it is acceptable to apply |fetch32|
to~|p|.

Because the type function |GCD| has no accompanying value-level
operations, we can define it without a type class:
\begin{code}
type family GCD d m n
type instance GCD d Zero Zero = d
type instance GCD d (Succ m) (Succ n) = GCD (Succ d) m n
type instance GCD Zero (Succ m) Zero = Succ m
type instance GCD (Succ d) (Succ m) Zero = GCD (Succ Zero) d m
type instance GCD Zero Zero (Succ n) = Succ n
type instance GCD (Succ d) Zero (Succ n) = GCD (Succ Zero) d n
\end{code}

\subsection{Tracking state and control in a parameterised monad}

Because actions in Haskell are values as well, phantom types can be used
to enforce properties on actions and control flow as well as on values and
data flow.  In particular, we can express the preconditions and
postconditions of monadic actions by generalising monads to
\emph{parameterised monads} \cite{atkey-parameterised}.  A parameterised
monad is a type constructor that takes three arguments, reminiscent of
a Hoare triple: an initial state, a final state, and the type of values
produced by the action.  As shown in the following class definition
(generalising the |Monad| class), a pure action does not change the
state, and concatenating two actions identifies the final state of the
first action with the initial state of the second action.
\VerbatimInput[firstline=-- Start PMonad,lastline=-- Stop PMonad]{Lock.hs}
The precise meaning of states depends on the particular parameterised
monad: they could describe files open, time spent, or the shape of
a managed heap \cite{kiselyov-resources}.
In this example, we use a parameterised monad to
track the locks held among a given (finite) set.

A lock can be acquired only if it is not currently held, and released
only if it is currently held.  Furthermore, no lock is held at the
beginning of the program, and no lock should be held at the end.  We
encode a set of locks and whether each is held by a type-level list of
booleans.  The spine of the list is made of |Cons| cells and |Nil|; each
element of the list is either |Locked| or |Unlocked|.  For example,
suppose we are tracking three locks.  If only the first and last are
held, then the state is the type
|Cons Locked (Cons Unlocked (Cons Locked Nil))|.
\VerbatimInput[firstline=-- Start phantoms,lastline=-- Stop phantoms]{Lock.hs}
The run-time representation of our parameterised monad is simply that of
Haskell's |IO| monad, so it is easy to implement a |PMonad| instance.
\VerbatimInput[firstline=-- Start actions,lastline=-- Stop actions]{Lock.hs}
It is also easy to lift an |IO| action that does not affect locks
to become a |LockM| action
whose initial and final states are the same and arbitrary.
\VerbatimInput[firstline=-- Start lput,lastline=-- Stop lput]{Lock.hs}

To manipulate boolean lists at the type level, we define type functions
|Get| and |Set|. Given a type-level natural number |n| and a list |p|,
the type |Get n p| is the |n|-th element of that list, and
the type |Set n e p| is the result of replacing the |n|-th 
element of~|p| by~|e|.
The first element of a list is indexed by |Zero|.  It is a type error if
the element does not exist because the list is too short.
\VerbatimInput[firstline=-- Start GetSet,lastline=-- Stop GetSet]{Lock.hs}

We represent a lock as a mutex handle (here caricatured by an |Int|),
with a phantom type~|n| attached to identify the lock at compile time.
The phantom type~|n| is an index into a type-level list.
\VerbatimInput[firstline=-- Start Lock,lastline=-- Stop Lock]{Lock.hs}
The data constructor introduced by the |newtype| declaration has no
run-time representation and so this wrapping imposes no run-time
overhead. We make one lock, |lock1|, for the sake of
further examples.
\VerbatimInput[firstline=-- Start lock1,lastline=-- Stop lock1]{Lock.hs}

We can now define actions to acquire and release locks.
The types of the actions reflect their constraints on the state.
\VerbatimInput[firstline=-- Start locking,lastline=-- Stop locking]{Lock.hs}
In the type of |acquire|, the constraint |Get n p ~ Unlocked| is the
\emph{precondition} on the state before acquiring the lock: the
lock to be acquired must not be already held. The final state
of the |LockM| action returned by |acquire| specifies the \emph{postcondition}: the
lock just acquired is |Locked|. For the |release| action, the pre- and
postconditions are the converse. To keep the example simple, we
do not manipulate any real locks; rather, we print our intentions.

At the top level, a |LockM| action is executed by applying the function
|run| to turn it into an |IO| action.  The type of |run| below requires
that the action begin and end with no lock held among three available.
\VerbatimInput[firstline=-- Start run,lastline=-- Stop run]{Lock.hs}
For example, given any action~|a|, the action |with1 a| defined below
acquires lock~1, performs~|a|, then releases lock~1 and returns the
result of~|a|.
\VerbatimInput[firstline=-- Start with1,lastline=-- Stop with1]{Lock.hs}
Therefore, we can execute |run (with1 (lput "hello"))| by itself.
\begin{code}
> run (with1 (lput "hello"))
acquire Lock 1
hello
release Lock 1
\end{code}
Multiple locks can be held at the same time and need not be released in
the opposite order as they were acquired.  However, the type system
prevents us from nesting |with1| inside |with1|, because such an action
would try to acquire lock~1 twice.  Indeed, the expression
|run (with1 (with1 (lput "hello")))| does not type-check.  We also
cannot acquire a lock without releasing it subsequently.  For example,
the expression |run (acquire lock1)| is rejected.

We can also introduce actions that do not change the state of
locks yet require that a certain lock be held:
\VerbatimInput[firstline=-- Start critical1,lastline=-- Stop critical1]{Lock.hs}
An attempt to run such an action without holding the required lock, as
in |run critical1|, is rejected by the type checker.
On the other hand, the program |run (with1 critical1)| type
checks and can be successfully executed. Likewise, we can define
potentially blocking actions, to be executed only when a lock is not
held; the type checker will then prevent such
actions within a critical section protected by the lock.



\subsection{Keeping the kinds straight}

It will not have escaped the reader's notice that we are
doing \emph{untyped} functional programming at the type level. 
For example, the kind of |GCD| is 
\begin{code}
GCD :: * -> * -> * -> *
\end{code}
so the compiler would accept the nonsensical type |(GCD Int Zero Bool)|.
The same problem occurs with |Pointer n| and other types defined in
this section.
We can alleviate the problem using the |Nat n| constraint. For
example, we could define |Pointer n| as
\begin{code}
newtype Nat n => Pointer n = MkPointer Int
\end{code}
so that, for example, |Pointer Bool| becomes invalid and will raise a
compile-time error. The constraint |Nat n| is a 
\emph{kind predicate}, specifying the set of types that constitute
natural numbers -- just as the type |Int|
specifies a set of values.

We wish for the convenience and discipline of algebraic data kinds
when writing type-level functions, just as we are accustomed to
algebraic data types in conventional, term-level programs. We could
find a way to `lift' the ordinary data type declaration
\begin{code}
data N = Zero | Succ N
\end{code}
to the kind level. Alternatively, we may want to declare algebraic 
data kinds like this:
\begin{code}
data kind N = Zero | Succ N
\end{code}
Here |N| is a kind constant and |Zero| and |Succ| are type constructors.
Now |GCD| could have the kind
\begin{code}
GCD :: N -> N -> N -> N
\end{code}
Similarly, |Pointer| and |Offset| should both have kind |N -> *|. Much
the same applies in the discussion of state and control, where we would
rather write:
\begin{code}
data kind ListLS = Nil | Cons LockState ListLS
data kind LockState = Locked | Unlocked
\end{code}
then give a decent kind to |Get|:
\begin{code}
Get :: N -> ListS -> LockState
\end{code}
Furthermore, unlike the earlier examples in which it was crucial that
our type functions were open (Section~\ref{s:open}), type functions
such as |GCD| and |Get| are \emph{closed}, in that all their
equations are given in one place.

These are shortcomings of GHC's current implementation, but there is
no technical difficulty with algebraic data kinds, and indeed 
they are fully supported by the Omega language \cite{sheard:future}.

\subsection{Type-preserving compilers}

A popular, if incestuous, application of Haskell is for writing compilers.
If the object language is statically typed, then one can index a
GADT by a phantom type
to ensure that only well-typed object programs can be represented
in the compiler \cite{pj+:simple-gadt}:
\begin{code}
data Exp a where
  Enum :: Int -> Exp Int
  Eadd :: Exp Int -> Exp Int -> Exp Int
  Eapp :: Exp (a->b) -> Exp a -> Exp b
  ...
\end{code}
Now an optimiser and an evaluator might have types
\begin{code}
optimise :: Exp a -> Exp a
evaluate :: Exp a -> a
\end{code}
which compactly express the facts that (a) the optimiser need only deal with
well-typed object terms, (b) optimising a term does not change its
type, and (c) evaluating a term yields a value of the correct type.

But what about transforming programs into continuation-passing style?
In that case, the
type of the result term is a \emph{function of} the type of the argument term:
\begin{code}
cpsConvert :: Exp a -> Exp (CpsT a)
\end{code}
Here |CpsT| maps a type~|a| to its
CPS-converted version \cite{meyer-continuation}.
\citeauthor{guillemette-monnier:cps} express |CpsT| as a type-level function
\cite{guillemette-monnier:cps}, whereas
\citeauthor{carette-finally-jfp} show how to do without type-level
functions \cite{carette-finally-jfp}.

\section{Related work and reflections} \label{s:related}

The goal of type families is to build on the
success of static type systems, by extending their power and expressiveness
without losing their brevity and comprehensibility to programmers.
(Of course, there is an implicit tension between these goals, and the
reader will have to judge how successful we have been.)  There are other
designs with similar goals:
\begin{itemize}
\item Functional dependencies took the Haskell community by storm when
Mark Jones introduced them \cite{jones-type}, because they met a
real need.  
Many, perhaps all, of the examples in this tutorial can
also be programmed using functional dependencies, but the programming
style at the type level feels like logic programming rather than
functional programming.
The reader may find a programmer's-eye comparison of the two
approaches in \cite{chakravarty-synonyms}.
Jones showed recently how the stylistic question can be at least
partly addressed by a notational device \cite{jones:fundeps2} but,
more fundamentally, the interaction of
functional dependencies with other type-level features such as existentials and
GADTs is not well understood and possibly problematic.
In fact, one may see type families as a way to understand functional
dependencies in these more general settings.

\item Omega \cite{sheard:future} is a prototype programing language
that specifically aims to provide the programmer with type-level
computation.
It goes quite a bit further than GHC's type families
(for example, Omega has an infinite tower of kinds and supports closed
type functions), but lacks type classes and much of the other Haskell
paraphernalia.  Omega comes with a number of excellent 
papers giving many a motivating example
\cite{sheard:programming-omega,sheard:generic-prog-omega,sheard:meta-prog-omega}.
\end{itemize}

These designs, along with GHC's type families, can be thought of as
helping programmers prove more interesting theorems that characterise
their programs.  Meanwhile, the theorem-proving and type-theory
community has been drawing from its long history of type-level
computation to help mathematicians write more interesting programs that
witness their theorems \cite{bove-dybjer:deptypes}.

The motivation for type-level
computations comes from the Curry-Howard correspondence
\cite{howard-formulae,girard-proofs} that underlies
Martin-L{\"o}f's intuitionistic type theory: propositions are types, and
proofs are terms.  The more expressive a type system, the more
propositions we can state and prove in~it, such as properties
involving numbers and arithmetic.  Hence expressive languages such as
those of NuPRL, Coq, Epigram, and Agda permit types involving
numbers and arithmetic. For example, the following type in Agda states
that addition is commutative:
\begin{code}
(n m : Nat) -> n + m == m + n
\end{code}
To prove this proposition is to write a term of this type, and
to check the proof is the job of the type checker.
To do its job, the type checker may need to simplify
a type like |(Zero + m)| to~|m|, so type checking involves
type-level computations.  Because a proof checker should always
terminate, it is natural to insist that type-level computations
also always terminate.

Since proof assistants based on type theory implement a
(richly typed) $\lambda$-calculus, they can be used to
program -- that is, to write terms that compute interesting values,
not just inhabit interesting types.
To this end, an expressive type system lets us state and prove more
interesting properties about programs~-- of the sort we
have shown in this paper. Tools such as Coq, Epigram, and
Agda thus cater increasingly to the use of theorem proving
for practical programming.
This convergence of theory and practice renews our commitment to
Tony Hoare's ideal of simple, reliable software.

\section*{Acknowledgements}

We would like to thank people who responded to our invitation to suggest
interesting examples of programming with type families, or commented on
a draft of the paper:
Lennart Augustsson,
Neil Brown,
Toby Hutton, 
Ryan Ingram,
Chris Kuklewicz,
Dave Menendez,
Benjamin Moseley,
Hugh Pacheco,
Conrad Parker,
Bernie Pope,
Tom Schrijvers,
Josef Svenningsson,
Paulo Tanimoto, 
Magnus Therning,
Ashley Yakeley,
and Brent Yorgey.

\bibliographystyle{mcbride}
\bibliography{typefun}


% ----------------------------------------------------------
\appendix 
\section*{Appendices}
These appendices will not appear in the published paper, only
in the online version.

\section{The Rules}

Here we summarise some rules governing type families.  The reader
may find more details elsewhere
\cite{chakravarty:assoc-data,chakravarty-synonyms,schrijvers-et-al:open-type-functions,chakravarty:indexed-families}.

The \emph{indices} of a type family are the arguments that 
appear to the left of the ``|::|'' in its kind signature.

\begin{enumerate}
\item Like ordinary Haskell |type| synonyms, a |type| family must always be saturated;
that is, it must be applied to all its type indices. 
For example:
\begin{code}
data D m = MkD (m Int)     -- So D :: (*->*) -> *

type family T a :: *       -- So T :: * -> *
f1 :: D T       -- ILLEGAL (unsaturated)

type family S a :: * -> *  -- So S :: * -> * -> *
f2 :: D (S a)   -- OK (saturated)

type family R a b :: *     -- So R :: * -> * -> *
f3 :: D (R a)   -- ILLEGAL (unsaturated)
\end{code}
This constraint does not apply to |data| families.

\item In a |type| |instance| or |data| |instance| declaration, any arguments that
are not type indices must be type variables.  For example:
\begin{code}
type family T a :: * -> *
type instance T Int b    = Int  -- OK
type instance T Int Bool = Int  -- Not allowed
type instance T a   Bool = Int  -- Not allowed
\end{code}

\item In an associated |type| or |data| declaration (i.e. one appearing nested in a
|class| declaration), the type indices must be a permutation of one or more of the
class variables.  For example:
\begin{code}
class C a b where
   type T1 a   :: *   	-- OK
   type T2 b   :: *   	-- OK
   type T3 b a :: *   	-- OK
   type T4 a c :: *   	-- Not OK; mentions 'c'
   type T5 a :: * -> *  -- OK
\end{code}

\item There is no difference between a type family declared as an associated type
of a class declaration, and a type family declared at top level.  For example, the
following are equivalent:
\begin{code}
class C1 a b where         |    type family T2 a :: *	   
  type T1 a :: *           |    class C2 a b where	   
  op :: a -> b -> Int      |      op :: a -> b -> Int	   
instance C1 Int Int where  |    type instance T2 Int = Bool
  type T1 Int = Bool       |    instance C2 Int Int where  
  op = ...                 |      op = ...		   
\end{code}
\end{enumerate}

\section{Pitfalls}

Type functions are powerful, but they can give rise to unexpected errors.
In this appendix we review some of the more common cases.

%% \oleg{Should we mention other pitfalls, e.g., potential divergence if
%%   undecidable instances extension is used? A different issue is the
%%   need for full dependent types. For example, consider a list
%%   whose type includes a type-level numeral describing the length of
%%   the list. Writing the function append requires a type function,
%%   the addition. But how to write the function filter on
%%   length-parameterized lists? How the signature of filter would look
%%   like?}

\subsection{Ambiguity}

One pitfall of type functions commonly mentioned on Haskell mailing lists
is a false expectation that they
are injective. As we discussed in Section~\ref{s:assoc-data}, 
type functions are, in general, not injective: if |F| is a type family,
then the fact |F t1| is the same as |F t2| does not imply that |t1|
and |t2| are the same (that fact is easy to see for the type function 
mapping any type to |Int|). Therefore, the type checker cannot
use the equality of |F t1| and |F t2| to equate |t1| and |t2|. 
\begin{comment}
For that reason, the type signature like
\begin{code}
f :: F a -> Int
\end{code}
(where |F| is a type function) is asking for trouble. Indeed, how to
instantiate this polymorphic function? The context of the application
of |f| can provide the type |F a|; since type functions are not
injective (let alone invertible) that does not help us at all to
determine the instantiation of the type variable |a|.
\end{comment}
The pitfall of the false expectation of injectivity of type functions
can be quite subtle. Consider the following example (abstracted from a
recent message on the Haskell-Cafe mailing list):
%% Haskell-Cafe
%% Peter Berry pwberry at gmail.com
%% Mon Apr 6 17:36:45 EDT 2009
\begin{code}
class C a where
  type F a :: *
  inj :: a -> F a
  prj :: F a -> a

-- bar :: (C a) => F a -> F a
bar x = inj (prj x)
\end{code}
That code type-checks; the inferred type signature is given in the
comments. The signature agrees with our expectation.
If we uncomment the signature, the type-checking fails:
\begin{verbatim}
foo.hs:8:17:
    Couldn't match expected type `F a' against inferred type `F a1'
    In the first argument of `prj', namely `x'
\end{verbatim}
It seems GHC does not like the signature it
itself inferred!  In fact, the bug here is that GHC should not have
accepted the signature-less |bar| in the first place, because
|bar| embodies an unresolvable ambiguity. To see the problem clearly,
let us assume the following instances of the class |C|:
\begin{code}
instance C Int where
    type F Int = Int
    inj = id
    prj = id

instance C Char where
    type F Char = Int
    inj _ = 0
    prj _ = 'a'
\end{code}
Given the application |bar (1::Int)|, which instance of |prj|
should the compiler choose: |prj:: Int -> Int| or |prj:: Int -> Char|?
The choice determines the result of |bar 1|: 1 or 0, respectively.
The application |bar (1::Int)| provides no information to 
help make this choice; in fact, \emph{no} context of |bar| usage can
resolve the ambiguity. The function |bar| is an instance of the
infamous read-show problem, the composition |show . read|, which
is just as ambiguous.

\begin{comment}
Type classes of Haskell98 already present a share of pitfalls; most
common is unresolved overloading: a polymorphic expression with
type-class constraints must be instantiated, but the context of the
expression is not specific enough to help instantiate type
variables and chose type-class instances. The most serious is
unresolvable overloading, a.k.a |read|-|show| problem, where no
no context can help instantiation.
Type functions exacerbate the problem.
\end{comment}

\subsection{Lack of inversion}

\simon{This is about inversion, not type vs data or injectivity, isn't it?
I.e. it would all apply for an injective type family, or for a data family.
So the initial sentence seems misleading to me.  Shall we skip straight to the ``In particular..''
part?}
Even if a type function (defined as a type family rather than a data
family) turns out to be injective, GHC will not notice that fact; in
particular, GHC will not try to invert such a type function. For
example, we may easily define addition of type-level naturals 
(\S\ref{s:arithm}) as a type family
\VerbatimInput[firstline=-- Start plus,lastline=-- Stop plus]{Arithm.hs}
The expression |tplus| has the monomorphic inferred type |Plus Two Three|
(with no constraints attached), and |toInt tplus| evaluates to |5|.
One may expect that a related |tplus'|
\begin{code}
tplus' x = if True then plus x (undefined::One) else tplus
\end{code}
will have a monomorphic type, too. However, GHC infers a polymorphic
type with a type equality constraint:
\begin{code}
tplus' :: (Succ (Succ (Succ Two)) ~ Plus m One) => m -> Plus m One
\end{code}
There is only a single type |m| (viz. |Four|) that satisfies the
constraint; one might hope that GHC would figure it out and resolve
the constraint. One should keep in mind that GHC is not a
general-purpose solver for arithmetic and other
constraints. The type families like |GCD| and |Plus| along with the type
equality let us write types with arbitrary arithmetic constraints over 
unbounded domain of type-level natural numbers. Solving these
constraints is an undecidable problem.



\section{Sprintf revisited}

In this appendix we explore yet another variant on |sprintf|, this 
one including \emph{higher order} type-level functions. Recall that
|sprintf| should take as an argument a format descriptor and zero or more
additional arguments. The number and the type of the additional
arguments~-- the values to format~-- depend on the type of the format
descriptor. The function |sprintf| should return the formatted
string. A format descriptor is an expression built by connecting primitive
descriptors such as |lit "str"| and |int| with a descriptor
composition operator |(^)|. For example,
\begin{code}
sprintf (lit "day")                      -- Result: "day",
sprintf (lit "day" ^ lit "s")            -- Result: "days",
sprintf (lit "day " ^ int) 3             -- Result: "day 3",
sprintf (int ^ lit " day" ^ lit "s") 3   -- Result: "3 days"
\end{code}

The specification immediately suggests the following naive implementation.
Since the format descriptor |lit "str"| denotes outputting (as the
result of |sprintf|) of the string |str|, |lit "str"| may just as well
be |str| itself. Thus |lit "str"| has the type |String|. 
The function |sprintf| is the identity then. The descriptor
|int| denotes receiving an integer and outputting it as a string, hence
|int| could be implemented as a function |show| of the type
|Int->String|. The composition of the format descriptors should
therefore concatenate the outputs of the descriptors. That is easy to
do if the two descriptors are |lit "str1"| and |lit "str2"|, in which
case we just concatenate |str1| and |str2|. When we compose |int|
and |lit "str1"|, we would like the composite format descriptor to be
|\x -> show x ++ "str"|. Thus, the left-associative
composition of two descriptors is type-directed:
\begin{code}
fmt1 ^ fmt2 = fmt1 ++ fmt2 
  when fmt1 :: String and fmt2 :: String
fmt1 ^ fmt2 = \x -> fmt1 x ++ fmt2 
  when fmt1 :: Int -> String and fmt2 :: String
fmt1 ^ fmt2 = fmt1 ++ \x -> fmt2 x
  when fmt1 :: String and fmt2 :: Int -> String
...
\end{code}
We have to analyse and induct on the types of both
arguments of |(^)|.

We can change the representation of descriptors so that we
need case analysis on the type of only one argument of |(^)|.
In the naive implementation, format descriptors have the general type
|t1 -> t2 -> ... -> String|.
The composition of the two descriptors have to `dive' under the layers
of |t1 -> t2 -> ...| in order to concatenate the underlying
|String|s~-- for \emph{both} descriptors. Let us change the
implementation: let |lit "str"| be a function that takes the current
output as the string and appends to it |str|:
\begin{code}
lit :: String -> (String -> String)
lit str = \s -> s ++ str
\end{code}
Likewise, |int| should receive the output so far, obtain an integer
and return the new output, with the formatted integer appended to the
current output:
\begin{code}
int :: String -> Int -> String
int = \s -> \x -> s ++ show x
\end{code}
Thus the formatters have the general type
|String -> t1 -> t2 -> ... -> String|.
With this implementation of the formatter, the composition of
formatters can be informally defined as
\begin{code}
fmt1 ^ fmt2 = \s -> fmt2 (fmt1 s)
  when fmt1 :: String -> String and fmt2 :: String -> t
fmt1 ^ fmt2 = \s -> \x -> fmt2 (fmt1 s x)
  when fmt1 :: String -> Int -> String and fmt2 :: String -> t
...
\end{code}
The formatter composition operation |(^)| needs case analysis
on the type of only one argument, which is straightforward with the
help of an ordinary, one-parameter type class. Here is the first attempt:
\begin{code}
class FCompose a where
    (^) :: (String -> a) -> (String -> b) -> (String -> ???)
\end{code}
What is the return type of |(^)| should be however? It is obvious that
|???| must depend on both |a| and |b|. The informal definition shows
that if |a| is |String|, |???| is just |b|. If |a| is
|Int->String| however, then |???| is |Int -> b|. In general, if |a| is
|t1 -> t2 -> ... String|, then |???| must be
|t1 -> t2 -> ... b|. We can try to use associated type synonyms to
express such a result type:
\begin{code}
class FCompose a where
    type Result a :: * -> *
    (^) :: (String -> a) -> (String -> b) -> (String -> Result a b)

instance FCompose String where
    type Result String b = b
    (^) f1 f2 = ...

instance FCompose c => FCompose (a -> c) where
    type Result (a -> c) b = a -> Result c b
    (^) f1 f2 = ...
\end{code}
Alas, for technical reasons this attempt doesn't work: |Result a| is
defined as having one type parameter and yielding an existing type
(constructor or a function) of the kind |* -> *|. After all, |Result|
is the type \emph{synonym}. Therefore, the definition of |Result|
associated with the instance |FCompose String| is invalid as 
|Result String| is not defined to be a synonym of an existing 
type constructor or
a function of the kind |* -> *|. To get around that, we resort to type
families, which are free from such restrictions. Here is the final,
working implementation:

\begin{code}
data I
class FCompose a where
  type Result a
  (^) :: (String -> a) -> (String -> b) ->
         (String -> TApply (Result a) b)

instance FCompose String where
  type Result String = I
  (^) f1 f2 = \s -> f2 (f1 s)

instance FCompose c => FCompose (a -> c) where
  type Result (a -> c) = a->Result c
  (^) f1 f2 = \s -> \x -> ((\s -> f1 s x) ^ f2) s
\end{code}
The associated type synonym |Result a| `computes' a type function
(more precisely, a functor) mapping a type |b| to a type containing |b|.
To be precise, |Result a| is a type that \emph{represents} a functor. The
language of representations is trivial: the type |I| represents the
identity functor, and the type |T1 -> I| represents 
the functor that takes a type |b| to a type |T1 -> b|. In other words,
|T1 -> F| represents the \emph{functional composition} of the functors
|(T1 ->)| and |F|. The type family |TApply F x| \emph{interprets} the
mini-language of functor representations and performs the application of
the corresponding functor to a type |x|:

\begin{code}
type family TApply functor x
type instance TApply I x = x
type instance TApply (a -> c) x = a -> TApply c x
\end{code}
Essentially, |TApply| is a \emph{higher-order} type function.

The function |sprintf| is then a simple wrapper over the format
descriptor:
\begin{code}
sprintf:: (String -> t) -> t
sprintf fmt = fmt ""
\end{code}


\end{document}

================ Stuff about containers and address ====================

\begin{comment}
\subsection{Smash your boilerplate}

\simon{Begin remarks:}
I don't find this section at all convincing. 
For a start, it's a very different technique (using a singleton
data type as a function name at type and value level).  And it 
doesn't even work very well; notably consider
\begin{code}
  data Employee = Emp Salary Name Age
\end{code}
Now I need to write boilerplate for |IncSal|, but |HideSal| doesn't work
at all, since the type isn't parametric enough.

What is the point you are trying make here?  Is it something to do with
``computing the result type''?  If so, is this the best example.  Maybe
printf?
\simon{End Remarks}
\oleg{Hmm, perhaps you are right. Printf is a much simpler example for
  computing the result type; Hinze used functors, but we can do much
  better. I can write the code shortly, if not today, at the latest on
  Wed.}


Datatype-generic programming offers a larger natural example, in which
recursion at the type level follows recursion at the value level.
Suppose that our company maintains its payroll using a |Salary| type:
\VerbatimInput[firstline=-- Start Salary,lastline=-- Stop Salary]{Generic.hs}
For simplicity, suppose that the salary and name of each employee is
stored as a pair of type |(Salary,String)|.  The payroll data structure
may be a large organisational hierarchy with different types for
departments and subsidiaries.  We want to traverse this data structure
and apply various transformations throughout such as hiding all
salaries, giving everyone a raise, and capitalising all names.  Each of
these transformations affects the type of the payroll in a different
way, but we want to write the code to traverse the payroll only once.

The function gmap generalises fmap
to the cases when the transformed type is not the last
type argument in the expression, or when transforming on several types
at the same type. For example, when applying a transformer that
transformed all Bool to Ints and and Char to strings to the values of
(Tree Bool Double) and (Tree Char Bool).
	  http://okmij.org/ftp/Haskell/generics.html#Smash

Because conventional traversal combinators such as |map| and |fmap| are
higher-order functions only at the value level, they cannot express the
fact that salary-hiding turns the type |(Salary,String)| into the type
|((),String)| (and the type |(Salary,Salary)| into the type |((),())|)
whereas name-capitalising keeps the types the same.  Also, to keep who
makes more money than whom a secret, it may not suffice to replace each
salary by~|()|; we may also need to scramble lists or maps that used to
be sorted or indexed by salary.  For our traversal code to allow
transformations (put differently, callback functions) with all this
flexibility, it needs to be a higher-order function at both the type
level and the value level.  Because only first-order type functions are
available to us, we need to represent transformations as first-order
types, using defunctionalization
\cite{reynolds-definitional-notes,danvy-defunctionalization} at the type level.

To begin, we define a two-parameter type class |Apply|.  The constraint
|Apply f a| means that a value of type~|f| is a transformation that
applies (using the value function |apply|) to a value of type~|a| and
yields a result of type |Result f a|.
\VerbatimInput[firstline=-- Start Apply,lastline=-- Stop Apply]{Generic.hs}
We represent the hide-salary and increment-salary transformations using
the singleton types |HideSal| and |IncSal|.  When applied to |Salary|
values, they yield results of different types~-- |()| and |Salary|,
respectively~-- but they both leave
|Char| values intact.
\VerbatimInput[firstline=-- Start HideSal IncSal,lastline=-- Stop HideSal IncSal]{Generic.hs}
To apply any transformation to a container, such as a pair or a list, is
to apply it to each component.
\VerbatimInput[firstline=-- Start containers,lastline=-- Stop containers]{Generic.hs}
The crucial flexibility that type functions afford us is that, starting
with a pair type such as |(Salary,String)|, the same transformation may
map each component into an unrelated type.  For example, we can evaluate
\begin{code}
apply HideSal [(Salary 42, "Alice"), (Salary 23, "Bob")]
\end{code}
to hide Alice and Bob's salaries.
The result is |[((),"Alice"), ((),"Bob")]|,
whose type |[((),String)]| is computed entirely
at compile time.

\subsection{Indexing into nested containers}

\simon{I don't find this section very perspicuous either.
Now that we have the earlier material, do we need this, or
are you trying to make a separate point?}
\oleg{I think it is an \emph{interesting} generalisation of printf; it
  is worth showing as a non-trivial application, just to give a taste
  of things possible with this approach.}
\simon{But what is the difference from the earlier examples?  Even
from {\tt Mutation}?  The container type depends on the index type in
precisely the same way that the reference type depends on the monad type.  No?}
\end{comment}

\begin{comment}
As a first example, let us focus on multidimensional lists and define an
overloaded function that replaces an element given its address,
a sequence of |Int| indices whose length must match the dimensionality
of the list.  More concretely, we want a function |replace| that has all
of the following
types:
\begin{code}
               Int    ->    [e]    -> e ->    [e]
          (Int,Int)   ->   [[e]]   -> e ->   [[e]]
     (Int,(Int,Int))  ->  [[[e]]]  -> e ->  [[[e]]]
(Int,(Int,(Int,Int))) -> [[[[e]]]] -> e -> [[[[e]]]]
\end{code}
This goal is easy to achieve using a type function that maps the address
type and the element type to the container type:
\VerbatimInput[firstline=-- Start uncurried,lastline=-- Stop uncurried]{Replace.hs}
We can use the |replace| function as follows.
\begin{code}
> replace (3::Int) "world" 'X'
"worXd"
> replace (1::Int,3::Int) ["hello","world"] 'X'
["hello","worXd"]
> replace (0::Int,(1::Int,3::Int)) [["hello","world"]] 'X'
[["hello","worXd"]]
\end{code}

It is just a bit trickier to write a version of |replace| that
takes its index arguments in the curried way.  In other words, we can
also write an overloaded function |replace'| with all of the following
types:
\begin{code}
                                e     -> e ->     e
                     Int ->    [e]    -> e ->    [e]
              Int -> Int ->   [[e]]   -> e ->   [[e]]
       Int -> Int -> Int ->  [[[e]]]  -> e ->  [[[e]]]
Int -> Int -> Int -> Int -> [[[[e]]]] -> e -> [[[[e]]]]
\end{code}
(The first type above is for replacing the entirety of a zero-dimensional
list.)  The problem of deciding whether |replace'| has a given type (and,
if so, producing the corresponding value) is to \emph{parse} the list of
curried argument types.  With 3 items of lookahead, this parsing can be
performed deterministically.  For example, if the type is of the form
|Int -> w1 -> w2 -> w3|, then the type cannot be the first one above.
Our solution (elided here) thus defines a 3-parameter type class
|Curried w1 w2 w3| such that |replace'| has the type |w1 -> w2 -> w3|.%
\footnote{\url{http://okmij.org/ftp/Haskell/puzzle-cps.hs}
\url{http://www.haskell.org/pipermail/haskell-cafe/2006-November/019475.html}}

\section{Towards richer types}

Thus far we have focused on data structures, but type families are good
for a variety of other related applications, as we discuss in this 
section.  The common pattern is that we compute one type from another
in a non-parametric way.
\end{comment}

\end{document}