~ohad-kammar/ohads-thesis/trunk

\Chapter{Conclusion}{But before you come to any conclusions\\%
Try walking in my shoes}{Depeche Mode}\chapterlabel{conclusion}

\nocats{}We set out to establish the existence of a general applicable
theory of Gifford-style type-and-effect systems. In the first part of
the thesis, we presented a spectrum of type-and-effect models
accounting for set-theoretic models, domain theoretic models,
algebraic models, and logical relations model. Our general account
culminated in the categorical conservative restriction construction,
establishing that semantics for type-and-effect systems arise as a
\emph{property} of an algebraic model, rather than a separately
specified structure. In the second part of the thesis, we presented
our theory's account of the various aspects of effect-dependent
optimisations, ranging from the syntax of type-and-effect systems,
through its semantics, the soundness and completeness of the
optimisation process, modular treatment of optimisation validity, and
a use case for synthesising sound and complete validity decision
procedures. We report that, once the semantic constructions were in
place, each of these areas required little effort to fit within the
theory, and we expect other aspects of type-and-effect systems to
follow suit.

The algebraic approach provides a valuable and general point of view,
resulting in: the connection between effect operations and effect
sets; the conservative restriction construction; the free lifting
construction; optimisation classification and discovery of new
optimisations; criteria for the validity of abstract optimisations;
and methods to derive the validity of optimisations for combinations
of effects modularly.

The use of CBPV  highlights the
interplay between functional constructs and effects. We advocate its
use as a fundamental lambda-calculus involving computational
effects. The categorical language greatly helped the organisation of this work, by
allowing much reuse of concepts and proofs. It was also crucial in
seeing the connection with F\"uhrmann's work, and unifying it with
Benton et al.'s.

Further work abounds:
\begin{description}
\item[Generality.]Our claim for generality will be much strengthened by
  generalising the logical relations argument of \corollaryref{free
    lifting} from its current (set-theoretic) presentation models to
  the (categorical) algebraic models. Doing so will tie the
  conservative restriction construction to the original
  non-hierarchical semantics. We conjecture that by imposing
  sufficiently strong conditions on the factorisation system
  $\pair\Epi\Mono$ of the enriching category, the $\Mono$-morphisms
  behave as predicates and allow us to generalise the proof.

  Going further, we would then like to generalise the constructions in
  \partref{optimisations} from the set-theoretic case to the
  categorical case. However, such generalisation will require more
  syntactic views of enriched Lawvere
  theories~\cite{plotkin:some-varieties-of-equational-logic}.
\item[Applicability.]We would like to incorporate more facets of
  type-and-effect analysis into our theory. An immediate first step
  is to incorporate Plotkin and Pretnar's \defterm{effect
    handlers}~\cite{plotkin-pretnar:effect-handlers-conference,
    plotkin-pretnar:effect-handlers-journal} so our theory can account
  for exception handlers. We foresee no problem in doing so in light
  of our work equipping a calculus of effect handlers with a
  type-and-effect system~\cite{kammar-lindley-oury:handlers-in-action}
  and Bauer and Pretnar's type-and-effect system for the Eff
  programming
  language~\cite{bauer-pretnar:an-effect-system-for-algebraic-effects-and-handlers}.

  Effect reconstruction is of immediate importance. It should be
  possible to derive general algorithms for type-and-effect
  annotation.  Our semantics can then be used to give semantics to
  such programs.  Levy's translations of call-by-value and
  call-by-name into CBPV could then be used to generalise
  call-by-value type-and-effect systems and discover novel
  call-by-name type-and-effect systems.  Another closely related
  direction is \emph{region
    inference}~\cite{birkedal-tofte:a-constraint-based-region-inference-algorithm}. Bauer
  and Pretnar's work on effect
  handlers~\cite{bauer-pretnar:an-effect-system-for-algebraic-effects-and-handlers}
  suggests region inference may generalise from memory accesses to
  arbitrary algebraic effects.

\item[Additional effects.]Another direction is to better fit
  additional computational effects into the algebraic theory of
  effects in the first step, and then into our theory of
  type-and-effect systems. Notions of locality, particularly local
  state, are very important.  It may be possible to make use of work
  on the algebraic treatment of locality, e.g., Plotkin and
  Power~\cite{plotkin-power:notions-of-computation-determine-monads},
  Melli\`es~\cite{mellies:segal-condition-meets-computational-effects},
  and
  Staton~\cite{staton:two-cotensors-in-one:presentations-of-algebraic-theories-for-local-state-and-fresh-names,
    staton:instances-of-computational-effects} to obtain a more
  general optimisation theory. This should enable incorporating the work of Benton
  et al. on dynamic
  allocation~\cite{benton-kennedy-beringer-hofmann:transformations-with-dynamic-allocation}.
  Interestingly, it should also incorporate
  Staton's account for logic
  programming~\cite{staton:an-algebraic-presentation-of-predicate-logic}.
  Incorporating higher-order
  store~\cite{benton-kennedy-beringer-hofmann:transformations-ho-store}
  would require solving recursive domain
  equations~\cite{abramsky-jung:domain-theory,
    levy:possible-world-semantics-for-general-storage-in-call-by-value}.
  We are also very interested in accounting for parallelism, as in Gifford's
  work~\cite{lucassen-gifford:polymorphic-effect-systems}.
\end{description}
We outline further work arising from each chapter:
\begin{description}
\item[Algebraic operations.] In \chapterref{operations} we
  considered only Eilenberg-Moore \cbpv{} models. It would be
  interesting to generalise our account to arbitrary \cbpv{} models.
\item[Models.] While we used categorical language to formulate our
  models, we did not consider any \emph{category of models}. It would
  be interesting to identify the appropriate notions of morphisms for
  each of our model classes. We could then formulate the relationship
  between our different categories of models using categorical notions
  like isomorphism and equivalence of categories.  More speculatively,
  categories of models would also include categorical constructions
  such as limits and colimits, and would perhaps give an abstract
  account of our conservative restriction construction.
\item[Lawvere theories.] As we noted on page~\pageref{mismatch between
  lawvere theories and presentations}, there is a mismatch between
  presentations and Lawvere theories: presentations allow us to have
  arbitrarily infinite parameter types, whereas $\regcard$-Lawvere
  theories are restricted by the cardinal $\regcard$. It is possible
  that there are other equivalent descriptions of algebraic theories
  that avoid this mismatch.  Melli\`es\footnote{Paul-Andr\'e
    Melli\`es, private communication, 2013.} suggests there might be a
  connection with monads with
  arities~\cite{berger-mellies-weber:monads-with-arities-and-their-associated-theories}.

  Another shortcoming of our account is the large amount of
  intimidating commutative diagrams. We obtained these proofs by
  translating proofs devised in our own variant of string
  diagrams~\cite{baez-stay:rosetta-stone} for symmetric monoidal
  closed categories. As we are not aware of any standard notation for
  string diagrams of (symmetric) monoidal closed categories, we
  decided to use the widely familiar commutative diagrams. (See
  Selinger~\cite{selinger:a-survey-of-graphical-languages-for-monoidal-categories}
  for a survey of such notations.) We leave to further work to recast
  our proofs in a familiar string diagrammatic form.

  In this context, Fiore\footnote{Marcelo P.~Fiore, private
    communication, 2013.}  suggested to us to use \defterm{monoidal
    actions} instead of enrichment. Fiore conjectures that monoidal
  actions produce a more pleasant theory of generalised Lawvere
  theories that does not involve as complicated commutative
  diagrams. We leave the investigation of his suggestion to further
  work.

  Atkey used parameterised
  monads~\cite{atkey:parameterised-notions-of-computation} to account
  for type-and-effect systems, and more generally,
  capabilities~\cite{atkey:algebras-for-parameterised-monads}. It
  would be interesting to investigate whether parameterised monads
  have a parameterised notion of Lawvere theories, and whether these
  can be used to extend our theory to the parameterised case.
\item[Algebraic models.]Our construction of a factorisation system of
  enriched Lawvere theories from a given factorisation in the
  enriching category is unsatisfactory, as we do not have an explicit
  characterisation of the left orthogonality class of
  $\FunctorFact\Mono$. Our free lifting construction suggests this
  class may have to coincide with its subclass $\FunctorFact\Epi$ of
  all morphisms whose $\mV,\oI$ components are $\Epi$-morphisms, as is
  certainly the case in $\Set$. Thus we are interested to find out
  whether $\FunctorFact\Epi$ may be a proper subclass of the left
  orthogonality class and under what conditions they coincide.

\item[Presentation models.]We would like to give a syntactic
  generalisation of presentation models to complement enriched Lawvere
  theories. However, the appropriate generalisation of equational
  logic has not yet been
  developed~\cite{plotkin:some-varieties-of-equational-logic}. It is
  possible that Staton's notion of parameterised
  theories~\cite{staton:instances-of-computational-effects} would
  serve this purpose.

\item[Predicate models.]Our notion of predicate models is general
  enough to include Benton et al.'s relational models. It is important
  to recast their models in terms of predicate models and compare them
  with the conservative restriction construction.

  Our free lifting construction is a form of inductive lifting. It
  would be interesting to compare it to other lifting constructions,
  most notably Katsumata's
  categorical-$\top\top$-lifting~\cite{katsumata:a-semantic-formulation-of-TT-lifting-and-logical-predicates-for-computational-metalanguage,
    katsumata:relating-computational-effects-by-TT-lifting-journal} and
  Larrecq et al.'s use of
  sconing~\cite{larrecq-lasota-nowak:logical-relations-for-monadic-types-arxive,
    larrecq-lasota-nowak:logical-relations-for-monadic-types-journal}.

\item[Intermediate language.]Despite having the domain-theoretic
  machinery in place (see \chapterref{recursion}), we did not incorporate
  recursion into our source language in order to focus on the shortest
  account towards effect-dependent optimisation. However, not
  accounting for recursion detracts from our applicability. Thus, an
  immediate next step is to give semantics to a \mail{} variant with
  recursion~\cite{kammar-plotkin:algebraic-foundations-for-effect-dependent-optimisations}
  using our recursion models. To achieve establish the connection with
  the conservative restriction model, we use a continuous variant of
  our free lifting construction.

  Another limitation of our intermediate language is caused by
  restricting arities to be of ground type. Generalising arities to
  non-ground types may involve recursive domain equations, as in the
  hypothesised treatment of higher-order store.

\item[Optimisations.] The logic we used for our optimisations is a
  simple equational logic --- we have only considered equations
  between terms. It seems straightforward to devise a richer
  effect-dependent counterpart to Plotkin and Pretnar’s
  logic~\cite{plotkin-pretnar:a-logic-for-algebraic-effects,
    pretnar:thesis}. Another direction is an effect-dependent account of
  refinement types, starting with Denney's thesis~\cite{denney:thesis}.

  We did not fully treat the local algebraic optimisations, those
  optimisations that originate from particular equations in the
  Lawvere theory. A full treatment would present a systematic
  translation from equations in the Lawvere theory into equations
  between program phrases, as Plotkin and Pretnar's
  logic~\cite{plotkin-pretnar:a-logic-for-algebraic-effects}.

  We did not supply any of the $36$ proofs justifying the equivalent
  conditions for the global algebraic optimisations in
  \figureref{fig:abstract}. We conjecture that there is a more basic
  description of these global optimisations using quantification over
  terms in the presentation $\mL_{\e}$. This desription may lead to a meta-theory of these optimisations.
  By exposing this syntax, we
  could generate both pristine and utilitarian forms mechanically from
  the more basic description. Their equivalence to the algebraic
  characterisation (and to each other using structural rules only)
  could then prove wholesale 27 of the proof obligations. The remaining
  $9$ obligations are the equivalence of the monadic condition and
  either of the other characterisations.  This basic description of
  the global optimisations would also allow us to uniformly define the
  notion of \defterm{operation-wise validity}, rather than give an
  ad-hoc definition for each of the optimisations.

\item[Combining effects.]  We concentrated on the more common sum and
  tensor combinators. Hyland and Power's distributive combination of
  theories~\cite{hyland-power:discrete-lawvere-theories-and-computational-effects}
  (used for combining ordinary and probabilistic computation) should
  be investigated too.

  The combination of write-only state and non-determinism should be
  re-examined in light of \exampleref{non conservativity of nondeterminism
    tensor write-only}.

\item[Use case]We are interested in a tensor analogue of the sum
  conservativity theorem~\theoremref{coproduct
    conservativity}. However, in light of \exampleref{non
    conservativity of nondeterminism tensor write-only} where we
  combined write-only state and non-determinism, we cannot hope to a
  sufficient condition that encompasses all practical cases.

Our \Haskell{} model for validating the completeness of our
decision procedures is limited by the \Haskell{} type system. We are
therefore interested in a similar model in a
dependently-typed programming language, such as
Idris~\cite{brady:idris---systems-programming-meets-full-dependent-types},
Agda~\cite{norell:thesis} or the Coq~\cite{coq:manual} proof
assistance, which seem more suitable for this purpose.
\end{description}

We aspire to change the effect systems discussion. Rather than
proceeding from case to case by analogy, we hope that the generality
and applicability of our approach will provide a first step on the way
to obtaining a scientifically-based engineering methodology to
type-and-effect systems.