diff --git a/thesis.bib b/thesis.bib index 9a2b801..342888c 100644 --- a/thesis.bib +++ b/thesis.bib @@ -359,6 +359,14 @@ year = 2019 } +@phdthesis{Saleh19, + author = {Amr Hany Saleh}, + title = {Efficient Algebraic Effect Handlers}, + school = {KU Leuven, Belgium}, + year = 2019 +} + + # Asynchronous effects @article{AhmanP21, author = {Danel Ahman and diff --git a/thesis.tex b/thesis.tex index b866210..5b4879e 100644 --- a/thesis.tex +++ b/thesis.tex @@ -16062,20 +16062,83 @@ effect. \subsection{Future work} \paragraph{Operating systems via effect handlers} -\begin{itemize} - \item Signal handling. - \item Implement an actual operation system using handlers. - \item Re-implement the case study in other programming languages. - \item Prove the UNIX with handlers correct. -\end{itemize} - -\begin{itemize} - \item Efficiency of nested handlers. - \item Effect-based optimisations. - \item Equational theories. - \item Parallel and distributed programming with effect handlers. - \item Multi-handlers. -\end{itemize} +In the \UNIX{} case study we explored the paradigmatic reading of +\emph{effect handlers as composable operating systems} in practice by +composing a \UNIX{}-like operating system out of several effects and +handlers. Obviously, the resulting system \OSname{} has been +implemented in the combined core calculus consisting of $\HCalc$, +$\SCalc$, and $\HPCalc$ calculi. There also exists an actual runnable +implementation of it in Links. It would be interesting to implement +the system in other programming languages with support for effect +handlers as at the time of writing most languages with effect handlers +have some unique trait, e.g. lexical handlers, special effect system, +etc. Ultimately, re-implementing the case study can help collect more +data points about programming with effect handlers, which can +potentially serve to inform the design of future effect +handler-oriented languages. + +I have made no attempts at formally proving the correctness of +\OSname{} with respect to some specification. Although, I have +consciously opted to implement \OSname{} using standard effects with +well-known equations. Furthermore, the effect handlers have been +implemented such that they ought to respect the equations of their +effects. Thus, perhaps it is possible to devise an equational +specification for the operating system and prove the implementation +correct with respect to that specification. + +One important feature that is arguably missing from \OSname{} is +external signal handling. Effect handlers as signal handlers is not a +new idea. In a previous paper we have outlined an idea for using +effect handlers to handle POSIX signals~\cite{DolanEHMSW17}. Signal +handling is a delicate matter as signals introduce a form of +preemption, thus some care needs to be taken to ensure that the +interpretation of a signal does not interrupted by another signal +instance. The essence of the idea is to have a \emph{mask} primitive, +which is a form of critical section for signals that permits some +block of code to suppress signal interruptions. A potential starting +point would be to combine \citeauthor{AhmanP21}'s calculus of +asynchronous effects with $\HCalc$ to explore this idea more +formally~\cite{AhmanP21}. + +Another interesting thought is to implement an actual operating system +using effect handlers. Although, it might be a daunting task, the idea +is maybe not so far fetched. With the advent of effect handlers in +OCaml~\cite{SivaramakrishnanDWKJM21} it may be possible for MirageOS +project~\cite{MadhavapeddyS14}, which is a unikernel based operating +system written in OCaml, to take advantage of effect handlers to +implement features such as concurrency. + +\paragraph{Effect-based optimisations} In this dissertation I have not +considered any effect-based optimisations. However if effect handler +oriented programming is to succeed in practice, then runtime +performance will matter. Optimisation of program structure is one way +to improve runtime performance. At our disposal we have the effect +system and the algebraic structure of effects and handlers. +% +Taking advantage of the information provided by the effect system to +optimise programs is an old idea that has been explored previously in +the literature~\cite{KammarP12,Kammar14,Saleh19}. +% +Other work has attempted to exploit the algebraic structure of (deep) +effect handlers to fuse nested handlers~\cite{WuS15}. +% +An obvious idea is to apply these lines of work to the handler calculi +of Chapter~\ref{ch:unary-handlers}. +% +Moreover, I hypothesise there is untapped potential in the combination +of effect-dependent analysis with respect to equational theories to +optimise effectful programs. A potential starting point for testing +out this hypothesis is to take \citeauthor{LuksicP20}'s a core +calculus where effects are equipped with equations~\cite{LuksicP20} +and combine it with techniques for effect-dependent +optimisations~\cite{KammarP12}. + +% \begin{itemize} +% \item Efficiency of nested handlers. +% \item Effect-based optimisations. +% \item Equational theories. +% % \item Parallel and distributed programming with effect handlers. +% \end{itemize} \paragraph{Multi handlers} In this dissertation I have solely focused on so-called \emph{unary} handlers, which handle a \emph{single} @@ -16109,6 +16172,23 @@ handlers only get amplified in the setting of multi handlers. \item Multi-handlers. \end{itemize} +\paragraph{Typed CPS for effect handlers} The image of each +translation developed in Chapter~\ref{ch:cps} is untyped. Typing the +translations may provide additional insight into the semantic content +of the translations. Effect forwarding poise a challenge in typing the +image. In order to encode forwarding we need to be able to +parametrically specify what a default case does. +% +The Appendix B of the paper by \citet{HillerstromLAS17} outlines a +possible typing for the CPS translation for deep handlers. The +extension we propose to our row type system is to allow a row type to +be given a \emph{shape} (something akin to +\citeauthor{BerthomieuS95}'s tagged types~\cite{BerthomieuS95}), which +constrains the form of the ordinary types it contains. Whether this +idea is formally sound and whether it extends to shallow handlers +remains to be investigated. + + \section{On the expressive power of effect handlers} %% %% Conclusions and Future work