
\section{Conclusions ; Further Work} \label{s-cfw}

\subsubsection{Ease and Difficulty of using \HOLw}

Quoting \cite[\S 1]{homeier}, the logic of HOL and its type system has found
a ``sweet spot'', combining expressivity with ease of use.
Arguably, the key to this is that its type system is decidable, 
where typechecking involving first-order unification, which produces 
principal types for each subterm.

Typechecking in \HOLw\ does not have these advantages, and so, inevitably,
it can fail. 
% the typechecking algorithm can fail. 
As is usual in HOL (as with programming in Standard ML),
a type error is often detected far away from where the programmer's error
occurred. 
In \HOLw\ this also occurs, where the ``error'' is insufficient type
annotation.

One solution is to include more type annotations.
It is of course easy to get them wrong: if the computer can work them out, 
it generally gets them right, which is a considerable help for the user.

There are two sorts of type annotations: giving the type of a term
(as in HOL, and Standard ML), and giving an explicit type argument to a
function, where the function's type requires it.
These explicit type arguments seem to be particularly helpful to the type
checker, and several times we redefined functions to use them,
after finding difficulties in getting a term to typecheck.
In particular, we suggest that type arguments rather than
free type variables be used in a function definition
in the case of higher-order types (type constructors).

In entering a term, such type arguments may be omitted:
this is a marvellous feature, 
since inserting them all would be a considerable burden.
In particular, when a function is later redefined to have a type argument,
it is a great relief that one does not need to change every use of that
function.
It should be acknowledged here that \HOLw\ is backward compatible with HOL,
so that HOL code not using the new features will run unchanged.
This is immensely valuable, 
well worth the extra development effort that was doubtless required.


% Needed some tricks : 
% $A \Longrightarrow B$ fails,
% $B \Longrightarrow A \Longrightarrow B$ succeeds, 
% HOL well provided with useful functions (here \texttt{dest\_imp})

% Proof steps requiring term to be specified difficult (HOL or \HOLw\ issue?)

\subsubsection{Value and Capabilities of \HOLw}

It is clearly possible to prove useful results in \HOLw.  
While proving routine results about adjoint functors, we noticed,
unexpectedly, that at one point one of the usual assumptions had in fact
not been used. This gave us a result which was known, but not to us,
and this led to our discussion of minimal presentations of a pair
of adjoint functors.

Then we have been able to express and prove results simplifying the conditions
given by Barr \& Wells for compatibility of two monads $M$ and $N$,
showing that two of their conditions are redundant,
and make use in the proofs of the fact that we have one monad in the Kleisli
category of another monad.
Applying results about a monad directly to a monad in the Kleisli category used
both these new features of \HOLw: explicit type parameters, and higher-order
types.

However our formalisation of categories has been based on representing objects
as types in the \HOLw\ logic.  So far as we can see this does not provide a
way of expressing results about, for example, the Eilenberg-Moore
category of a monad, whose objects are constructed from objects \emph{and}
arrows of the original category, where these satisfy certain conditions.
This suggests attempting to model categories in a framework
with dependent types, such as Coq or Lego.
Our treatment of categories also has some formal limitations.
Since \HOLw\ is a set-based logic we have clearly not formally proved results
about categories whose collections of arrows are not sets.
And since we used \HOLw\ types as objects, our adjoint
functors were between categories with the same objects.
On the other hand, we have not taken advantage of these facts; 
all our proof steps are the same as in a proof
which formally applies to categories in general.

In considering distributive laws, we made use of the fact that there is a
monad, related to $N$, in the Kleisli category of $M$.  
Barr \& Wells show that there is a monad, a ``lifting'' of $M$, in the
Eilenberg-Moore category of $N$.
Since there a duality between the Kleisli and Eilenberg-Moore constructions
% (they are initial and terminal objects of a certain category) 
we suspect some connexion between these results, which we
have not yet identified.

\subsubsection{Acknowledgements}
I wish to thank Robin Cockett for helpful discussions about minimal
characterisations of pairs of adjoint functors, and
Michael Barr for discussions about distributive laws, including the
crucial observation about the duality between various compatibility conditions.
I wish to thank Peter Homeier and Michael Norrish for
their help with the use of \HOLw\ and HOL.
% their help with the use of \HOLw\ and HOL.
