Other theses

code/State.hs

@@ -0,0 +1,124 @@
+{- A Haskell version of the companion code for "State of effectful programming".
+   Tested with GHCi 8.6.5. -}
+import Control.Monad.ST (runST)
+import Data.STRef       (newSTRef, readSTRef, writeSTRef)
+-- State monad
+newtype State s a = State { runState :: s -> (a,s) }
+
+-- | State is a functor
+instance Functor (State s) where
+  fmap f m = State (\st -> let (x, st') = runState m st in
+                           (f x, st'))
+
+-- | State is an applicative functor
+instance Applicative (State s) where
+  pure x = State (\st -> (x, st))
+  m1 <*> m2 = State (\st -> let (f, st') = runState m1 st in
+                            runState (fmap f m2) st')
+
+-- | State is a monad
+instance Monad (State s) where
+  return = pure
+  m >>= k = State (\st -> let (x, st') = runState m st in
+                          runState (k x) st')
+
+-- | State operations
+get :: () -> State s s
+get () = State (\st -> (st, st))
+
+put :: s -> State s ()
+put st = State (\st' -> ((), st))
+
+-- Continuation monad
+newtype Cont r a = Cont { runCont :: (a -> r) -> r }
+
+-- | Cont is a functor
+instance Functor (Cont r) where
+  fmap f k = Cont (\g -> runCont k (\x -> g (f x)))
+
+-- | Cont is an applicative functor
+instance Applicative (Cont r) where
+  pure x  = Cont (\k -> k x)
+  k <*> k' = Cont (\r -> runCont k
+                   (\k'' -> runCont k'
+                     (\x -> r (k'' x))))
+
+-- | Cont is a monad
+instance Monad (Cont r) where
+  return  = pure
+  m >>= k = Cont (\k' -> runCont m
+                   (\x -> runCont (k x)
+                     (\y -> k' y)))
+
+-- | State operations
+
+getk :: () -> Cont (State s a) s
+getk () = Cont (\k -> State (\st -> runState (k st) st))
+
+putk :: s -> Cont (State s a) ()
+putk st' = Cont (\k -> State (\st -> runState (k ()) st'))
+
+-- Free monad
+data Free f a = Return a
+              | Op (f (Free f a))
+
+-- | Free is a functor
+instance Functor f => Functor (Free f) where
+  fmap f (Return x) = Return (f x)
+  fmap f (Op y)     = Op (fmap (fmap f) y)
+
+-- | Free is an applicative functor
+instance Functor f => Applicative (Free f) where
+  pure  = Return
+  (Return f) <*> xs = fmap f xs
+  (Op f)     <*> xs = Op (fmap (\g -> g <*> xs) f)
+
+-- | Free is a monad
+instance Functor f => Monad (Free f) where
+  return = Return
+  (Return x) >>= k = k x
+  (Op y)     >>= k = Op (fmap (\m' -> m' >>= k) y)
+
+-- | Auxiliary function for constructing operation nodes
+do' :: Functor f => f a -> Free f a
+do' op = Op (fmap Return op)
+
+-- Instantiate Free with state
+data FreeState s r = Get (s -> r)
+                   | Put s (() -> r)
+
+-- | FreeState is a functor
+instance Functor (FreeState s) where
+  fmap f (Get k) = Get (\st -> f (k st))
+  fmap f (Put st' k) = Put st' (\() -> f (k ()))
+
+-- | State operations
+get' :: () -> Free (FreeState s) s
+get' () = do' (Get (\x -> x))
+
+put' :: s -> Free (FreeState s) ()
+put' st = do' (Put st (\() -> ()))
+
+-- | State handler
+runState' :: s -> Free (FreeState s) a -> (a, s)
+runState' st0 (Op (Get k))    = runState' st0 (k st0)
+runState' st0 (Op (Put st k)) = runState' st (k ())
+runState' st0 (Return x)      = (x, st0)
+
+-- Generic state example
+incrEven :: Monad m => (() -> m Int, Int -> m ()) -> () -> m Bool
+incrEven (get, put) () = get () >>= (\st -> put (1 + st) >>= (\() -> return (even st)))
+
+runExamples :: Int -> [(String, (Bool, Int))]
+runExamples st0 = map (\(s, f) -> (s, f st0)) examples
+  where examples = [ ("builtin state", \st -> runST $ do
+                         st' <- newSTRef st
+                         v   <- readSTRef st'
+                         writeSTRef st' (v + 1)
+                         v'  <- readSTRef st'
+                         return (even v, v'))
+                   , ("pure state passing", \st -> (even st, st + 1))
+                   , ("state monad", \st -> runState (incrEven (get, put) ()) st)
+                   , ("continuation monad", \st -> runState (runCont (incrEven (getk, putk) ())
+                                                              (\x -> State (\st -> (x, st)))) st)
+                   , ("free monad", \st -> runState' st (incrEven (get', put') ())) ]

code/state.ml

@@ -0,0 +1,396 @@
+(* Companion for "State of effectful programming"
+   Tested with OCaml 4.10.0+multicore. *)
+
+(* Generic direct-style incr_even *)
+let even : int -> bool
+  = fun n -> n mod 2 = 0
+
+let incr_even : (unit -> int) * (int -> unit) -> unit -> bool
+  = fun (get, put) () ->
+  let st = get () in
+  put (1 + st);
+  even st
+
+(* Delimited control *)
+module Prompt : sig
+  type 'a t
+  val make : unit -> 'a t
+  val reify : 'a t -> (('b -> 'a) -> 'a) -> 'b
+  val install : 'a t -> (unit -> 'a) -> 'a
+end = struct
+  type 'a t = {
+      install : (unit -> 'a) -> 'a;
+      reify : 'b. (('b -> 'a) -> 'a) -> 'b
+    }
+
+  let make (type a) () =
+    let module M = struct
+        effect Prompt : (('b -> a) -> a) -> 'b
+      end
+    in
+    let reify f = perform (M.Prompt f) in
+    let install f =
+      match f () with
+      | x -> x
+      | effect (M.Prompt f) k -> f (continue k)
+    in
+    { install; reify }
+
+  let install { install; _ } = install
+  let reify { reify; _ } = reify
+  let resume k v = continue k v
+end
+
+module type CTRL = sig
+  type ans
+  val reset : (unit -> ans) -> ans
+  val shift : (('a -> ans) -> ans) -> 'a
+end
+
+module Ctrl(R : sig type ans end) : sig
+  include CTRL with type ans = R.ans
+end = struct
+  type ans = R.ans
+
+  let p : ans Prompt.t = Prompt.make ()
+
+  let reset m =
+    Prompt.install p m
+
+  let shift f =
+    Prompt.reify p
+      (fun k ->
+        Prompt.install p
+          (fun () ->
+            f (fun x ->
+                Prompt.install p
+                  (fun () -> k x))))
+end
+
+module CtrlState
+         (S : sig type s end)
+         (R : sig type ans end): sig
+  type s = S.s
+  type ans = s -> R.ans * s
+
+  val get : unit -> s
+  val put : s -> unit
+
+  val run : (unit -> R.ans) -> ans
+end = struct
+  type s = S.s
+  type ans = s -> R.ans * s
+  module Ctrl = Ctrl(struct type nonrec ans = ans end)
+
+  let get ()  = Ctrl.shift (fun k -> fun st -> k st st)
+  let put st' = Ctrl.shift (fun k -> fun st -> k () st')
+
+  let run m =
+    Ctrl.reset
+      (fun () ->
+        let x = m () in
+        fun st -> (x, st))
+end
+
+module CtrlIntState = CtrlState(struct type s = int end)(struct type ans = bool end)
+
+(* Monadic programming *)
+module type MONAD = sig
+  type 'a t
+  val return : 'a -> 'a t
+  val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+end
+
+(** State monad **)
+module type STATE_MONAD = sig
+  type ans
+  type s
+  include MONAD
+
+  val get : unit -> s t
+  val put : s -> unit t
+  val run : (unit -> ans t) -> s -> ans * s
+end
+
+module StateMonad(S : sig type s end)(R : sig type ans end): sig
+  include STATE_MONAD with type s = S.s
+                       and type ans = R.ans
+end = struct
+  type ans = R.ans
+  type s = S.s
+  type 'a t = s -> 'a * s
+
+  let return : 'a -> 'a t
+    = fun x -> fun st -> (x, st)
+
+  let (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+    = fun m k -> fun st ->
+      let (x, st') = m st in
+      k x st'
+
+  let get : unit -> s t
+    = fun () st -> (st, st)
+
+  let put : s -> unit t
+    = fun st st' -> ((), st)
+
+  let run : (unit -> ans t) -> s -> ans * s
+    = fun m st -> m () st
+end
+
+module IntStateMonad = StateMonad(struct type s = int end)(struct type ans = bool end)
+
+(** Continuation monad **)
+module type CONTINUATION_MONAD = sig
+  type r
+  include MONAD with type 'a t = ('a -> r) -> r
+end
+
+module ContinuationMonad(R : sig type ans end): sig
+  include CONTINUATION_MONAD with type r = R.ans
+end = struct
+  type r = R.ans
+  type 'a t = ('a -> r) -> r
+
+  let return : 'a -> 'a t
+    = fun x -> fun k -> k x
+
+  let (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+    = fun m k -> fun c ->
+      m (fun x -> k x c)
+end
+
+module ContinuationStateMonad
+         (S : sig type s end)
+         (R : sig type ans end): sig
+  type s = S.s
+  type ans = R.ans
+  include CONTINUATION_MONAD with type r = s -> ans * s
+
+  val get : unit -> s t
+  val put : s -> unit t
+  val run : (unit -> ans t) -> s -> ans * s
+end = struct
+  type s = S.s
+  type ans = R.ans
+  module ContinuationMonad : CONTINUATION_MONAD with type r = s -> ans * s
+    = ContinuationMonad(struct type nonrec ans = s -> ans * s end)
+  include ContinuationMonad
+
+  let get : unit -> s t
+    = fun () -> fun k -> fun st -> k st st
+
+  let put : s -> unit t
+    = fun st' -> fun k -> fun st -> k () st'
+
+  let run : (unit -> R.ans t) -> s -> R.ans * s =
+    fun m st -> m () (fun x -> fun st -> (x, st)) st
+end
+
+module ContinuationIntStateMonad
+  = ContinuationStateMonad(struct type s = int end)(struct type ans = bool end)
+
+(** Free monad **)
+module type FUNCTOR = sig
+  type 'a t
+  val fmap : ('a -> 'b) -> 'a t -> 'b t
+end
+
+module type FREE_MONAD = sig
+  type 'a op
+  type 'a free = Return of 'a
+               | Op of 'a free op
+
+  include MONAD with type 'a t = 'a free
+
+  val do' : 'a op -> 'a free
+end
+
+module FreeMonad(F : FUNCTOR) : sig
+  include FREE_MONAD with type 'a op = 'a F.t
+end = struct
+  type 'a op = 'a F.t
+  type 'a free = Return of 'a
+               | Op of 'a free F.t
+
+  type 'a t = 'a free
+
+  let return : 'a -> 'a t
+    = fun x -> Return x
+
+  let rec (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+    = fun m k ->
+    match m with
+    | Return x -> k x
+    | Op y -> Op (F.fmap (fun m' -> m' >>= k) y)
+
+  let do' : 'a F.t -> 'a free
+    = fun op -> Op (F.fmap (fun x -> Return x) op)
+end
+
+module type FREE_STATE = sig
+  type s
+  type 'r opsig = Get of (s -> 'r)
+                | Put of s * (unit -> 'r)
+  include FUNCTOR with type 'r t = 'r opsig
+end
+
+module FreeState(S : sig type s end) = struct
+  type s = S.s
+  type 'r opsig = Get of (s -> 'r)
+                | Put of s * (unit -> 'r)
+  type 'r t = 'r opsig
+
+  let fmap : ('a -> 'b) -> 'a t -> 'b t
+    = fun f op ->
+    match op with
+    | Get k -> Get (fun st -> f (k st))
+    | Put (st', k) -> Put (st', fun st -> f (k ()))
+end
+
+module FreeIntStateMonad: sig
+  include STATE_MONAD with type s = int
+                       and type ans = bool
+end = struct
+
+  module rec FreeIntState : FREE_STATE with type s = int
+    = FreeState(struct type s = int end)
+  and FreeIntStateMonad : FREE_MONAD with type 'r op = 'r FreeIntState.opsig
+    = FreeMonad(FreeIntState)
+
+  open FreeIntState
+  include FreeIntStateMonad
+
+  type s = int
+  type ans = bool
+
+  let get : unit -> s t
+    = fun () -> do' (Get (fun st -> st))
+
+  let put : s -> unit t
+    = fun st -> do' (Put (st, fun () -> ()))
+
+  let rec run : (unit -> ans t) -> s -> ans * s
+    = fun m st ->
+    match m () with
+    | Return x          -> (x, st)
+    | Op (Get k)        -> run (fun () -> k st) st
+    | Op (Put (st', k)) -> run k st'
+end
+
+(** Monadic reflection **)
+module Reflect
+         (M : MONAD)
+         (R : sig type ans end): sig
+  type ans = R.ans
+
+  val reify : (unit -> ans) -> ans M.t
+  val reflect : 'a M.t -> 'a
+
+end = struct
+  type ans = R.ans
+  effect Reflect : 'a M.t -> 'a
+
+  let reify : (unit -> ans) -> ans M.t
+    = fun f ->
+    let open M in
+    match f () with
+    | x -> return x
+    | effect (Reflect m) k -> m >>= (continue k)
+
+  let reflect : 'a M.t -> 'a
+    = fun m ->
+    perform (Reflect m)
+end
+
+module ReflectIntStateMonad
+  = Reflect(IntStateMonad)(struct type ans = bool end)
+
+module ReflectIntState = struct
+  open ReflectIntStateMonad
+
+  let get : unit -> int
+    = fun () -> reflect (IntStateMonad.get ())
+
+  let put : int -> unit
+    = fun st -> reflect (IntStateMonad.put st)
+
+  let run : (unit -> bool) -> int -> bool * int
+    = fun m st -> IntStateMonad.run (fun () -> reify m) st
+end
+
+(* Generic monadic incr_even *)
+module MonadExample(T : STATE_MONAD with type s = int) = struct
+  let incr_even : unit -> bool T.t
+    = fun () ->
+    let open T in
+    (get ()) >>= (fun st -> put (1 + st)
+             >>= (fun () -> return (even st)))
+end
+
+(** Effect handlers **)
+module type STATE_HANDLER = sig
+  type s
+
+  val get : unit -> s
+  val put : s -> unit
+  val run : (unit -> 'a) -> s -> 'a * s
+end
+
+module StateHandler(S : sig type s end) : STATE_HANDLER with type s = S.s = struct
+  type s = S.s
+
+  effect Put : s -> unit
+  let put st = perform (Put st)
+
+  effect Get : unit -> s
+  let get () = perform (Get ())
+
+  let run
+    = fun m st ->
+    let f = match m () with
+      | x -> (fun st -> (x, st))
+      | effect (Put st') k -> (fun st -> continue k () st')
+      | effect (Get ()) k -> (fun st -> continue k st st)
+    in f st
+end
+
+module IntStateHandler = StateHandler(struct type s = int end)
+
+let run_examples () =
+  let examples = [
+      "builtin", (fun st ->
+        let st = ref st in let v = !st in st := 1 + v; (even v, !st));
+      "pure state passing", (fun st -> (even st, 1 + st));
+      "shift/reset", (fun st ->
+        CtrlIntState.run (incr_even CtrlIntState.(get, put)) st);
+      "state monad", (fun st ->
+        let module MonadStateExample = MonadExample(IntStateMonad) in
+        IntStateMonad.run MonadStateExample.incr_even st);
+      "continuation monad", (fun st ->
+        let module ContinuationMonadExample = MonadExample(ContinuationIntStateMonad) in
+        ContinuationIntStateMonad.run ContinuationMonadExample.incr_even st);
+      "free monad", (fun st ->
+        let module FreeMonadExample = MonadExample(FreeIntStateMonad) in
+        FreeIntStateMonad.run FreeMonadExample.incr_even st);
+      "monadic reflection", (fun st ->
+        ReflectIntState.run (incr_even ReflectIntState.(get, put)) st);
+      "state handler", (fun st ->
+        IntStateHandler.run (incr_even IntStateHandler.(get, put)) st) ]
+  in
+  List.map (fun (s, f) -> (s, f 4)) examples
+(* module IntStateMRefl : MREFL with type ans := bool and type 'a t = 'a IntState.t
+ *   = MRefl(struct type ans = bool end)(IntState)
+ * 
+ * let get () = IntStateMRefl.reflect (IntState.get ())
+ * let put st = IntStateMRefl.reflect (IntState.put st)
+ * let run m st = IntState.run (IntStateMRefl.reify m) st
+ * 
+ * let even : int -> bool
+ *   = fun n -> n mod 2 = 0
+ * 
+ * let incr_even : unit -> bool
+ *   = fun () ->
+ *   let st = get () in
+ *   put (1 + st);
+ *   even st *)

code/unix.links

@@ -45,8 +45,6 @@ module Queue {
   fun singleton(x) { enqueue(x, empty) }
 }
 
-
-
 ##
 ## Environment
 ##
@@ -106,6 +104,27 @@ fun usermgr(user, envs, m) {
 ## Basic IO
 ##
 typename FileDescr = Int;
+typename FileCursor = Int;
+
+module File {
+  typename T = [String];
+
+  sig empty : T
+  var empty = [];
+
+  sig read : (FileCursor, T) ~> Option(String)
+  fun read(start, file) {
+    switch (drop(start, file)) {
+      case []     -> None
+      case x :: _ -> Some(x)
+    }
+  }
+
+  sig write : (String, FileCursor, T) ~> T
+  fun write(contents, fptr, file) {
+    take(fptr, file) ++ [contents] ++ drop(fptr, file)
+  }
+}
 
 sig stdout : FileDescr
 var stdout = 1;
@@ -113,7 +132,7 @@ var stdout = 1;
 sig puts : (FileDescr,String) {Puts:(FileDescr,String) -> () |_}-> ()
 fun puts(fd, s) { do Puts(fd, s) }
 
-sig basicIO : (Comp(a, {Puts:(FileDescr,String) -> () |e})) {Puts{_} |e}~> [String]
+sig basicIO : (Comp(a, {Puts:(FileDescr,String) -> () |e})) {Puts{_} |e}~> File.T
 fun basicIO(m) {
   handle(m()) {
     case Return(_) -> []
@@ -121,8 +140,6 @@ fun basicIO(m) {
   }
 }
 
-# TODO: implement file space.
-
 ##
 ## Generic state handling.
 ##
@@ -153,118 +170,125 @@ var stderr = 2;
 sig eof : String
 var eof = "\x00";
 
-sig gets : (FileDescr) {Gets:(FileDescr) -> String |_}-> String
-fun gets(fd) { do Gets(fd) }
+typename Mode = [|Read|Write|];
 
-typename Mode = [|Create|Append|];
+typename FileDescr = Int;
+typename INode = (loc:Option(Int),refc:Int);
 
-sig fopen : (Mode, String) {Fopen:(Mode, String) -> FileDescr |_}-> FileDescr
-fun fopen(mode, filename) { do Fopen(mode, filename) }
+typename INodeTable = [(INode, File.T)];
+typename FileTable  = [(Mode, INode)];
+typename 
 
-sig fclose : (FileDescr) {Fclose:(FileDescr) -> () |_}-> ()
-fun fclose(fd) { do Fclose(fd) }
+# sig gets : (FileDescr) {Gets:(FileDescr) -> String |_}-> String
+# fun gets(fd) { do Gets(fd) }
 
-typename File = Queue.T(String);
+# sig fopen : (Mode, String) {Fopen:(Mode, String) -> FileDescr |_}-> FileDescr
+# fun fopen(mode, filename) { do Fopen(mode, filename) }
 
-sig emptyFile : File
-var emptyFile = Queue.empty;
+# sig fclose : (FileDescr) {Fclose:(FileDescr) -> () |_}-> ()
+# fun fclose(fd) { do Fclose(fd) }
 
-sig writeFile : (String, File) -> File
-fun writeFile(s, file) { Queue.enqueue(s, file) }
+# typename File = Queue.T(String);
 
-sig readFile : (File) ~> (String, File)
-fun readFile(file) {
-  switch (Queue.dequeue(file)) {
-    case (None, file) -> (eof, file)
-    case (Some(s), file) -> (s, file)
-  }
-}
+# sig emptyFile : File
+# var emptyFile = Queue.empty;
 
-typename FileTable = [(FileDescr, File)];
-typename FileStore = [(String, FileDescr)];
-typename FileSystem = (next:Int,ft:FileTable,fs:FileStore);
+# sig writeFile : (String, File) -> File
+# fun writeFile(s, file) { Queue.enqueue(s, file) }
 
-sig defaultFileSystem : () -> FileSystem
-fun defaultFileSystem() {
-  var defaultTable = [ (stdin , emptyFile)
-                     , (stdout, emptyFile)
-                     , (stderr, emptyFile) ];
+# sig readFile : (File) ~> (String, File)
+# fun readFile(file) {
+#   switch (Queue.dequeue(file)) {
+#     case (None, file) -> (eof, file)
+#     case (Some(s), file) -> (s, file)
+#   }
+# }
 
-  var defaultStore = [ ("stdin" , stdin)
-                     , ("stdout", stdout)
-                     , ("stderr", stderr) ];
+# typename FileTable = [(FileDescr, File)];
+# typename FileStore = [(String, FileDescr)];
+# typename FileSystem = (next:Int,ft:FileTable,fs:FileStore);
 
-  (next=3,ft=defaultTable,fs=defaultStore)
-}
+# sig defaultFileSystem : () -> FileSystem
+# fun defaultFileSystem() {
+#   var defaultTable = [ (stdin , emptyFile)
+#                      , (stdout, emptyFile)
+#                      , (stderr, emptyFile) ];
 
-sig lookupFile : (FileDescr, FileSystem) ~> File
-fun lookupFile(fd, fsys) {
-   switch (lookup(fd, fsys.ft)) {
-     case Nothing -> error("err: No such file(" ^^ intToString(fd) ^^ ")")
-     case Just(file) -> file
-   }
-}
+#   var defaultStore = [ ("stdin" , stdin)
+#                      , ("stdout", stdout)
+#                      , ("stderr", stderr) ];
 
-sig replaceFile : (FileDescr, File, FileSystem) ~> FileSystem
-fun replaceFile(fd, file, fsys) {
-  var ft = modify(fd, file, fsys.ft);
-  (fsys with ft = ft) # TODO handle nonexistent file.
-}
+#   (next=3,ft=defaultTable,fs=defaultStore)
+# }
 
-sig createFile : (String, FileSystem) -> (FileDescr, FileSystem)
-fun createFile(filename, fsys) {
-  var fd = fsys.next;
-  (fd, (next = fd + 1, fs = (filename, fd) :: fsys.fs, ft = (fd, emptyFile) :: fsys.ft))
-}
+# sig lookupFile : (FileDescr, FileSystem) ~> File
+# fun lookupFile(fd, fsys) {
+#    switch (lookup(fd, fsys.ft)) {
+#      case Nothing -> error("err: No such file(" ^^ intToString(fd) ^^ ")")
+#      case Just(file) -> file
+#    }
+# }
 
-sig openFile : (Mode, String, FileSystem) ~> (FileDescr, FileSystem)
-fun openFile(mode, filename, fsys) {
-  var (fd, fsys') = switch (lookup(filename, fsys.fs)) {
-      case Nothing -> createFile(filename, fsys)
-      case Just(fd) -> (fd, fsys)
-  };
-  switch (mode) {
-    case Create -> error("erase")
-    case Append -> (fd, fsys')
-  }
-}
+# sig replaceFile : (FileDescr, File, FileSystem) ~> FileSystem
+# fun replaceFile(fd, file, fsys) {
+#   var ft = modify(fd, file, fsys.ft);
+#   (fsys with ft = ft) # TODO handle nonexistent file.
+# }
 
-sig closeFile : (File) ~> File
-fun closeFile((=front,=rear)) {
-  (front=front ++ reverse(rear), rear=[])
-}
+# sig createFile : (String, FileSystem) -> (FileDescr, FileSystem)
+# fun createFile(filename, fsys) {
+#   var fd = fsys.next;
+#   (fd, (next = fd + 1, fs = (filename, fd) :: fsys.fs, ft = (fd, emptyFile) :: fsys.ft))
+# }
 
-sig allowState : (() {Get-,Put- |e}~> a) -> () {Get:s,Put:(s) -> () |e}~> a
-fun allowState(f) { (f : (() {Get:s,Put:(s) -> () |e}~> a) <- (() {Get-,Put- |e}~> a)) }
+# sig openFile : (Mode, String, FileSystem) ~> (FileDescr, FileSystem)
+# fun openFile(mode, filename, fsys) {
+#   var (fd, fsys') = switch (lookup(filename, fsys.fs)) {
+#       case Nothing -> createFile(filename, fsys)
+#       case Just(fd) -> (fd, fsys)
+#   };
+#   switch (mode) {
+#     case Create -> error("erase")
+#     case Append -> (fd, fsys')
+#   }
+# }
 
-sig fileIO : (Comp(a, {Get-,Put-,Gets:(FileDescr) -> String,Puts:(FileDescr,String) -> (),Fclose:(FileDescr) -> (),Fopen:(Mode,String) -> FileDescr |e})) {Get:() {}-> FileSystem,Put:(FileSystem) -> (),Gets{_},Puts{_},Fclose{_},Fopen{_} |e}~> a
-fun fileIO(m) {
-  handle(allowState(m)()) {
-    case Gets(fd, resume) ->
-      var fsys = get();
-      var (ch, file) = readFile(lookupFile(fd, fsys));
-      put(replaceFile(fd, file, fsys)); resume(ch)
-    case Puts(fd, ch, resume) ->
-      var fsys = get();
-      var fsys' = replaceFile(fd, writeFile(ch, lookupFile(fd, fsys)), fsys);
-      put(fsys'); resume(())
-    case Fopen(mode, filename, resume) ->
-      var fsys = get();
-      var (fd, fsys') = openFile(mode, filename, fsys);
-      put(fsys'); resume(fd)
-    case Fclose(fd, resume) ->
-      var fsys = get();
-      var fsys' = replaceFile(fd, closeFile(lookupFile(fd, fsys)), fsys);
-      put(fsys'); resume(())
-  }
-}
+# sig closeFile : (File) ~> File
+# fun closeFile((=front,=rear)) {
+#   (front=front ++ reverse(rear), rear=[])
+# }
 
-sig redirect : (Comp(a, {Puts:(FileDescr,String) -> () |e}), FileDescr) {Puts:(FileDescr,String) -> () |e}~> a
-fun redirect(m, fd) {
-  handle(m()) {
-    case Puts(_,s,resume) -> resume(puts(fd, s))
-  }
-}
+# sig allowState : (() {Get-,Put- |e}~> a) -> () {Get:s,Put:(s) -> () |e}~> a
+# fun allowState(f) { (f : (() {Get:s,Put:(s) -> () |e}~> a) <- (() {Get-,Put- |e}~> a)) }
+
+# sig fileIO : (Comp(a, {Get-,Put-,Gets:(FileDescr) -> String,Puts:(FileDescr,String) -> (),Fclose:(FileDescr) -> (),Fopen:(Mode,String) -> FileDescr |e})) {Get:() {}-> FileSystem,Put:(FileSystem) -> (),Gets{_},Puts{_},Fclose{_},Fopen{_} |e}~> a
+# fun fileIO(m) {
+#   handle(allowState(m)()) {
+#     case Gets(fd, resume) ->
+#       var fsys = get();
+#       var (ch, file) = readFile(lookupFile(fd, fsys));
+#       put(replaceFile(fd, file, fsys)); resume(ch)
+#     case Puts(fd, ch, resume) ->
+#       var fsys = get();
+#       var fsys' = replaceFile(fd, writeFile(ch, lookupFile(fd, fsys)), fsys);
+#       put(fsys'); resume(())
+#     case Fopen(mode, filename, resume) ->
+#       var fsys = get();
+#       var (fd, fsys') = openFile(mode, filename, fsys);
+#       put(fsys'); resume(fd)
+#     case Fclose(fd, resume) ->
+#       var fsys = get();
+#       var fsys' = replaceFile(fd, closeFile(lookupFile(fd, fsys)), fsys);
+#       put(fsys'); resume(())
+#   }
+# }
+
+# sig redirect : (Comp(a, {Puts:(FileDescr,String) -> () |e}), FileDescr) {Puts:(FileDescr,String) -> () |e}~> a
+# fun redirect(m, fd) {
+#   handle(m()) {
+#     case Puts(_,s,resume) -> resume(puts(fd, s))
+#   }
+# }
 
 ##
 ## Processes
@@ -331,70 +355,70 @@ fun whoami() { getenv("USER") }
 ##
 
 # Tags puts with the name of the current user.
-sig provenance : (Comp(a, {Getenv:(String) -> String,Puts:(FileDescr,String) -> () |e})) {Getenv:(String) -> String,Puts:(FileDescr,String) -> () |e}~> a
-fun provenance(m) {
-  handle(m()) {
-    case Puts(fd, s, resume) ->
-      var user = whoami();
-      resume(do Puts(fd, user ^^ "> " ^^ s))
-  }
-}
+# sig provenance : (Comp(a, {Getenv:(String) -> String,Puts:(FileDescr,String) -> () |e})) {Getenv:(String) -> String,Puts:(FileDescr,String) -> () |e}~> a
+# fun provenance(m) {
+#   handle(m()) {
+#     case Puts(fd, s, resume) ->
+#       var user = whoami();
+#       resume(do Puts(fd, user ^^ "> " ^^ s))
+#   }
+# }
 
-# An example of everything plugged together: a time-shared 'Hello World'.
-sig example : () {Fork:Bool,Getenv:(String) -> String,Su:(User) -> (),Puts:(FileDescr,String) -> (),Yield:() |_}~> ()
-fun example() {
-  var pid = fork();
-  var () = {
-    if (pid) redirect(fun(){puts(stdout, "dummy")}, stderr)
-    else if (fork()) su(Alice)
-    else su(Bob)
-  };
-  var user = whoami();
-  puts(stdout, "Hello World!");
-  var uid = getenv("UID");
-  echo("My UID is " ^^ uid);
-  (if (amiroot()) { yield(); echo(user ^^ " is running as root.") } else ());
-  echo("My home dir is /home/" ^^ user)
-}
+# # An example of everything plugged together: a time-shared 'Hello World'.
+# sig example : () {Fork:Bool,Getenv:(String) -> String,Su:(User) -> (),Puts:(FileDescr,String) -> (),Yield:() |_}~> ()
+# fun example() {
+#   var pid = fork();
+#   var () = {
+#     if (pid) redirect(fun(){puts(stdout, "dummy")}, stderr)
+#     else if (fork()) su(Alice)
+#     else su(Bob)
+#   };
+#   var user = whoami();
+#   puts(stdout, "Hello World!");
+#   var uid = getenv("UID");
+#   echo("My UID is " ^^ uid);
+#   (if (amiroot()) { yield(); echo(user ^^ " is running as root.") } else ());
+#   echo("My home dir is /home/" ^^ user)
+# }
 
-# Wiring of handlers.
-sig init : () {Fork{_},Getenv{_},Su{_},Puts{_},Yield{_} |_}~> [String]
-fun init() {
-  basicIO(fun() {
-    schedule(fun() {
-      usermgr(Root, envs, fun() {
-        provenance(example)
-      })
-    })
-  })
-}
+# # Wiring of handlers.
+# sig init : () {Fork{_},Getenv{_},Su{_},Puts{_},Yield{_} |_}~> [String]
+# fun init() {
+#   basicIO(fun() {
+#     schedule(fun() {
+#       usermgr(Root, envs, fun() {
+#         provenance(example)
+#       })
+#     })
+#   })
+# }
 
-sig example' : () {Fork:Bool,Fclose:(FileDescr) -> (),Fopen:(Mode,String) -> FileDescr,Getenv:(String) -> String,Su:(User) -> (),Puts:(FileDescr,String) -> (),Yield:() |_}~> ()
-fun example'() {
-  var pid = fork();
-  var () = {
-    if (pid) redirect(fun(){puts(stdout, "dummy")}, stderr)
-    else if (fork()) su(Alice)
-    else su(Bob)
-  };
-  var user = whoami();
-  var fd = fopen(Append, user ^^ ".txt");
-  puts(fd, "Hello World!");
-  var uid = getenv("UID");
-  echo("My UID is " ^^ uid);
-  (if (amiroot()) { yield(); echo(user ^^ " is running as root.") } else ());
-  echo("My home dir is /home/" ^^ user);
-  fclose(fd)
-}
+# sig example' : () {Fork:Bool,Fclose:(FileDescr) -> (),Fopen:(Mode,String) -> FileDescr,Getenv:(String) -> String,Su:(User) -> (),Puts:(FileDescr,String) -> (),Yield:() |_}~> ()
+# fun example'() {
+#   var pid = fork();
+#   var () = {
+#     if (pid) redirect(fun(){puts(stdout, "dummy")}, stderr)
+#     else if (fork()) su(Alice)
+#     else su(Bob)
+#   };
+#   var user = whoami();
+#   var fd = fopen(Append, user ^^ ".txt");
+#   puts(fd, "Hello World!");
+#   var uid = getenv("UID");
+#   echo("My UID is " ^^ uid);
+#   (if (amiroot()) { yield(); echo(user ^^ " is running as root.") } else ());
+#   echo("My home dir is /home/" ^^ user);
+#   fclose(fd)
+# }
 
 
-sig init' : (FileSystem) {Fclose{_},Fopen{_},Fork{_},Get{_},Getenv{_},Gets{_},Put{_},Puts{_},Su{_},Yield{_}|_}~> ((), FileSystem)
-fun init'(fsys) {
-  runState(fsys, fun() {
-    fileIO(fun() {
-      schedule(fun() {
-        usermgr(Root, envs, example')
-      })
-    })
-  })
-}
+# sig init' : (FileSystem) {Fclose{_},Fopen{_},Fork{_},Get{_},Getenv{_},Gets{_},Put{_},Puts{_},Su{_},Yield{_}|_}~> ((), FileSystem)
+# fun init'(fsys) {
+#   runState(fsys, fun() {
+#     fileIO(fun() {
+#       schedule(fun() {
+#         usermgr(Root, envs, example')
+#       })
+#     })
+#   })
+# }

code/unix2.links

@@ -680,3 +680,18 @@ fun tcphandshakeFail() {
     performTCP(tcpserver, 84, sfd, cfd)
   }
 }
+
+#
+# Grep
+#
+#sig grep : (String) {Await:Char,Yield:(Char) -> () |_}~> ()
+fun grep(str) {
+  var cs = explode(str);
+  fun match(c,cs) {
+    switch (cs) {
+      case c' :: cs' ->
+        if (c == '\n') fail()
+        if (c == c') 
+    }
+  }
+}

macros.tex

@@ -140,6 +140,8 @@
 
 \newcommand{\Cong}{\mathrm{cong}}
 
+\newcommand{\AlgTheory}{\ensuremath{\mathcal{T}}}
+
 %% Handler projections.
 \newcommand{\mret}{\mathrm{ret}}
 \newcommand{\mops}{\mathrm{ops}}

thesis.bib

@@ -3445,4 +3445,34 @@
   pages     = {114--136},
   publisher = {Springer},
   year      = {1999}
+}
+
+# Intensional type theory
+@book{MartinLof84,
+  author    = {Per Martin{-}L{\"{o}}f},
+  title     = {Intuitionistic type theory},
+  series    = {Studies in proof theory},
+  volume    = {1},
+  publisher = {Bibliopolis},
+  year      = {1984}
+}
+
+# Unison language
+@misc{Chiusano20,
+  author = {Paul Chiusano and others},
+  title  = {{Unison} language reference},
+  year = 2020,
+  note = {Revision \href{https://github.com/unisonweb/unisonweb-org/tree/cb9a1988731451311eeb372f69e9b9f576aa02d3/src/data/docs/language-reference}{cb9a198}}
+}
+
+# Effect handlers in C
+@inproceedings{Leijen17b,
+  author    = {Daan Leijen},
+  title     = {Implementing Algebraic Effects in {C} - "Monads for Free in {C}"},
+  booktitle = {{APLAS}},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {10695},
+  pages     = {339--363},
+  publisher = {Springer},
+  year      = {2017}
 }

thesis.tex

@@ -458,11 +458,6 @@ I dub \emph{effect handler oriented programming}.
 % not every control phenomenon is equal in terms of programmability and
 % expressiveness.
 
-% % \section{This thesis in a nutshell}
-% % In this dissertation I am concerned only with
-% % \citeauthor{PlotkinP09}'s deep handlers, their shallow variation, and
-% % parameterised handlers which are a slight variation of deep handlers.
-
 \section{Why first-class control matters}
 From the perspective of programmers first-class control is a valuable
 programming feature because it enables them to implement their own
@@ -808,7 +803,10 @@ emergence of monads as a programming abstraction began when
 \citet{Moggi89,Moggi91} proposed to use monads as the mathematical
 foundation for modelling computational effects in denotational
 semantics. \citeauthor{Moggi91}'s view was that \emph{monads determine
-  computational effects}. This view was put into practice by
+  computational effects}. The key property of this view is that pure
+values of type $A$ are distinguished from effectful computations of
+type $T~A$, where $T$ is the monad representing the effect(s) of the
+computation. This view was put into practice by
 \citet{Wadler92,Wadler95}, who popularised monadic programming in
 functional programming by demonstrating how monads increase the ease
 at which programs may be retrofitted with computational effects.
@@ -869,10 +867,17 @@ different computational effects. In the following subsections we will
 see three different instantiations with which we will implement global
 mutable state.
 
+Monadic programming is a top-down approach to effectful programming,
+where the concrete monad structure is taken as a primitive which
+controls interactions between effectful operations.
+% Monadic programming is a top-down approach to effectful programming,
+% where we start with a concrete framework in which we can realise
+% effectful operations.
+%
 The monad laws ensure that monads have some algebraic structure, which
-programmers can use when reasoning about their monadic programs, and
-optimising compilers may take advantage of the structure to emit more
-efficient code for monadic programs.
+programmers can use when reasoning about their monadic
+programs. Similarly, optimising compilers may take advantage of the
+structure to emit more efficient code.
 
 The success of monads as a programming idiom is difficult to
 understate as monads have given rise to several popular
@@ -1285,13 +1290,13 @@ operations using the state-passing technique.
 %
 \[
   \bl
-    \runState : (\UnitType \to \Free\,(\FreeState~S)\,A) \to S \to A \times S\\
+    \runState : (\UnitType \to \Free\,(\FreeState~S)\,R) \to S \to R \times S\\
     \runState~m~st \defas
       \Case\;m\,\Unit\;\{
       \ba[t]{@{}l@{~}c@{~}l}
          \return~x      &\mapsto& (x, st);\\
-         \OpF\,(\Get~k) &\mapsto& \runState~st~(\lambda\Unit.k~st);\\
-         \OpF\,(\Put\,\Record{st';k}) &\mapsto& \runState~st'~k
+         \OpF\,(\Get~k) &\mapsto& \runState\,(\lambda\Unit.k~st)~st;\\
+         \OpF\,(\Put\,\Record{st';k}) &\mapsto& \runState~k~st'
       \}\ea
   \el
 \]
@@ -1311,8 +1316,8 @@ that this interpretation of get and put satisfies the equations of
 Definition~\ref{def:state-monad}.
 %
 
-By instantiating $S = \Int$ we can use this interpreter to run
-$\incrEven$.
+By instantiating $S = \Int$ and $R = \Bool$ we can use this
+interpreter to run $\incrEven$.
 %
 \[
   \runState~\incrEven~4 \reducesto^+ \Record{\True;5} : \Bool \times \Int
@@ -1323,7 +1328,7 @@ effect handlers.
 
 \subsection{Back to direct-style}
 \dhil{The problem with monads is that they do not
-  compose. Cite~\citet{Espinosa95}, \citet{VazouL16}}
+  compose. Cite~\citet{Espinosa95}, \citet{VazouL16} \citet{McBrideP08}}
 %
 Another problem is that monads break the basic doctrine of modular
 abstraction, which we should program against an abstract interface,
@@ -1426,43 +1431,96 @@ $R = \Bool$ and $S = \Int$.
 \subsubsection{Handling state}
 %
 At the start of the 00s decade
-\citet{PlotkinP01,PlotkinP02,PlotkinP03} introduced \emph{algebraic
-  effects}, which is an approach to effectful programming that inverts
-\citeauthor{Moggi91}'s view such that \emph{computational effects
-  determine monads}. In their view a computational effect is given by
-a signature of effectful operations and a collection of equations that
-govern their behaviour, together they generate a free monad rather
-than the other way around.
+\citet{PlotkinP01,PlotkinP02,PlotkinP03} introduced algebraic theories
+of computational effects, or simply \emph{algebraic effects}, which
+inverts \citeauthor{Moggi91}'s view of effects such that
+\emph{computational effects determine monads}.  In their view a
+computational effect is described by an algebraic effect, which
+consists of a signature of abstract operations and a collection of
+equations that govern their behaviour, together they generate a free
+monad rather than the other way around.
+%
+Algebraic effects provide a bottom-up approach to effectful
+programming in which abstract effect operations are taken as
+primitive. Using these operations we may build up concrete structures.
 %
 In practical programming terms, we may understand an algebraic effect
 as an abstract interface, whose operations build the underlying free
 monad.
-
-By the end of the decade \citet{PlotkinP09,PlotkinP13} introduced
-\emph{handlers for algebraic effects}, which interpret computation
-trees induced by effectful operations in a similar way to runners of
-free monad interpret computation trees. A crucial difference between
-handlers and runners is that the handlers are based on first-class
-delimited control.
 %
-Practical programming with algebraic effects and their handlers was
-popularised by \citet{KammarLO13}, who demonstrated that algebraic
-effects and handlers provide a modular basis for effectful
-programming.
-
-%\dhil{Cite \citet{PlotkinP01,PlotkinP02,PlotkinP03,PlotkinP09,PlotkinP13}.}
+\begin{definition}
+  % A \emph{signature} $\Sigma$ is a collection of operation symbols
+  % $\ell : A \opto B \in \Sigma$. An operation symbol is a syntactic entity.
+  An algebraic effect is given by a pair
+  $\AlgTheory = (\Sigma,\mathsf{E})$ consisting of an effect signature
+  $\Sigma = \{(\ell_i : A \opto B)_i\}_i$ of typed operation symbols
+  $\ell_i$, whose interactions are govern by set of equations
+  $\mathsf{E}$.
+  %
+  We will not concern ourselves with the mathematical definition of
+  equation, as in this dissertation we will always fix
+  $\mathsf{E} = \emptyset$, meaning that the interactive patterns of
+  operations are unrestricted. As a consequence we will regard an
+  operation symbol as a syntactic entity subject only to a static
+  semantics. The type $A \opto B$ denotes the space of operations
+  whose payload has type $A$ and whose interpretation yields a value
+  of type $B$.
+\end{definition}
 %
-From a programming perspective effect handlers are an operational
-extension of \citet{BentonK01} style exception handlers.
+As with the free monad, the meaning of an algebraic effect operation
+is conferred by some separate interpreter. In the algebraic theory of
+computational effects such interpreters are known as handlers for
+algebraic effects, or simply \emph{effect handlers}. They were
+introduced by \citet{PlotkinP09,PlotkinP13} by the end of the decade.
+%
+A crucial difference between effect handlers and interpreters of free
+monads is that effect handlers use delimited control to realise the
+behaviour of computational effects.
+% The meaning of an algebraic effect is conferred by a suitable effect
+% handler, or in analogy with the free monad a suitable interpreter. Effect handlers were By
+% the end of the decade \citet{PlotkinP09,PlotkinP13} introduced
+% \emph{handlers for algebraic effects}, which interpret computation
+% trees induced by effectful operations in a similar way to runners of
+% free monad interpret computation trees. A crucial difference between
+% handlers and runners is that the handlers are based on first-class
+% delimited control.
+%
+Practical programming with effect handlers was popularised by
+\citet{KammarLO13}, who advocated algebraic effects and their handlers
+as a modular basis for effectful programming.
+
+Effect handlers introduce two dual control constructs.
 %
 \[
   \ba{@{~}l@{~}r}
-    \Do\;\ell^{A \opto B}~M^C : B & \Handle\;M^A\;\With\;H^{A \Harrow B} : B \smallskip\\
-    \multicolumn{2}{c}{H^{C \Harrow D} ::= \{\Return\;x^C \mapsto M^D\} \mid \{\OpCase{\ell^{A \opto B}}{p^A}{k^{B \to D}} \mapsto M^D\} \uplus H}
+    \Do\;\ell^{A \opto B}~V^A : B & \Handle\;M^C\;\With\;H^{C \Harrow D} : D \smallskip\\
+    \multicolumn{2}{c}{H ::= \{\Return\;x^C \mapsto N^D\} \mid \{\OpCase{\ell^{A \opto B}}{p^A}{k^{B \to D}} \mapsto N^D\} \uplus H^{C \Harrow D}}
   \ea
 \]
-The operation symbols are declared in a signature
-$\ell : A \opto B \in \Sigma$.
+%
+The $\Do$ construct reifies the control state up to a suitable handler
+and packages it up with the operation symbol $\ell$ and its payload
+$V$ before transferring control to the suitable handler. As control is
+transferred a hole is left in the evaluation context that must be
+filled before evaluation can continue. The $\Handle$ construct
+delimits $\Do$ invocations within the computation $M$ according to the
+handler definition $H$. Handler definitions consist of the union of a
+single $\Return$-clause and the disjoint union of zero or more
+operation clauses. The $\Return$-clause specifies what to do with the
+return value of a computation. An operation clause
+$\OpCase{\ell}{p}{k}$ matches on an operation symbol and binds its
+payload to $p$ and its continuation $k$. Note that the domain type of
+the continuation agrees with the codomain type of the operation
+symbol, and the codomain type of the continuation agrees with the
+codomain type of the handler definition. Continuation application
+fills the hole left by the $\Do$ construct, thus providing a value
+interpretation of the invocation. The continuation returns inside the
+handler once the $\Return$-clause computation has finished.
+%
+Operationally, effect handlers may be regarded as an extension of
+\citet{BentonK01} style exception handlers.
+
+We can implement mutable state with effect handlers as follows.
 %
 \[
   \ba{@{~}l@{\qquad\quad}@{~}r}
@@ -1509,12 +1567,16 @@ interpreter is that here the continuation $k$ implicitly reinstalls
 the handler, whereas in the free state monad interpreter we explicitly
 reinstalled the handler via a recursive application.
 %
-By fixing $S = \Int$ we can use the above effect handler to run the
-delimited control variant of $\incrEven$.
+By fixing $S = \Int$ and $A = \Bool$ we can use the above effect
+handler to run the delimited control variant of $\incrEven$.
 %
 \[
   \runState~\incrEven~4 \reducesto^+ \Record{\True;5} : \Bool \times \Int
 \]
+%
+Effect handlers come into their own when multiple effects are
+combined. Throughout the dissertation we will see multiple examples of
+handlers in action (e.g. Chapter~\ref{ch:unary-handlers}).
 
 \subsubsection{Effect tracking}
 \dhil{Cite \citet{GiffordL86}, \citet{LucassenG88}, \citet{TalpinJ92},
@@ -1554,10 +1616,70 @@ function under a handler that interprets at least $\Get$ and $\Put$.
 
 \dhil{Mention the importance of polymorphism in effect tracking}
 
+\section{Scope}
+Since the inception of effect handlers numerous variations and
+extensions of them have been proposed.  In this dissertation I am
+concerned only with \citeauthor{PlotkinP09}'s deep handlers, their
+shallow variation, and parameterised handlers which are a slight
+variation of deep handlers.
 
+\subsection{Some pointers to elsewhere}
+The literature on effect handlers is rich, and my dissertation is but
+one of many on topics related to effect handlers. In this section I
+provide a few pointers to related work involving effect handlers that
+I will not otherwise discuss in this dissertation.
+
+Readers interested in the mathematical theory and original development
+of effect handlers should consult \citeauthor{Pretnar10}'s PhD
+dissertation~\cite{Pretnar10}.
+
+Lexical effect handlers are a variation on \citeauthor{PlotkinP09}'s
+deep handlers, which provide a form of lexical scoping for effect
+operations, thus statically binding them to their handlers.
+%
+\citeauthor{Geron19}'s PhD dissertation develops the mathematical
+theory of scoped effect operations, whilst \citet{WuSH14} and
+\citet{BiernackiPPS20} studies them from a programming perspective.
+
+To get a grasp of the reasoning principles for effect handlers,
+interested readers should consult \citeauthor{McLaughlin20}'s PhD
+dissertation, which contains a development of relational reasoning
+techniques for shallow
+multi-handlers~\cite{McLaughlin20}. \citeauthor{McLaughlin20}'s
+techniques draw inspiration from the logical relation reasoning
+techniques for deep handlers due to \citet{BiernackiPPS18}.
+
+\citeauthor{Ahman17}'s PhD dissertation is relevant for readers
+interested in the integration of computational effects into dependent
+type theories~\cite{Ahman17}. \citeauthor{Ahman17} develops an
+intensional \citet{MartinLof84} style effectful dependent type theory
+equipped with a novel computational dependent type.
+
+Effect handlers were conceived in the realm of category theory to give
+an algebraic treatment of exception handling~\cite{PlotkinP09}. They
+were adopted early by functional programmers, who either added
+language-level support for effect handlers~
+\cite{Hillerstrom15,DolanWSYM15,BiernackiPPS18,Leijen17,BauerP15,BrachthauserSO20a,LindleyMM17,Chiusano20}
+or embedded them in
+libraries~\cite{KiselyovSS13,KiselyovI15,KiselyovS16,KammarLO13,BrachthauserS17,Brady13,XieL20}. Thus
+functional perspectives on effect handlers are plentiful in the
+literature. Only a few has studied effect handlers outside the realm
+of functional programming: \citet{Brachthauser20} offers an
+object-oriented perspective on effect handlers; \citet{Saleh19}
+provides a logic programming perspective via an effect handlers
+extension to Prolog; and \citet{Leijen17b} has an imperative take on
+effect handlers in C.
 
 \section{Contributions}
-The key contributions of this dissertation are the following:
+The key contributions of this dissertation are scattered across the
+four main parts. The following listing summarises the contributions of
+each part.
+\paragraph{Background}
+\begin{itemize}
+  \item A comprehensive operational characterisation of various
+    notions of continuations and first-class control phenomena.
+\end{itemize}
+\paragraph{Programming}
 \begin{itemize}
   \item A practical design for a programming language equipped with a
     structural effect system and deep, shallow, and parameterised effect
@@ -1566,6 +1688,10 @@ The key contributions of this dissertation are the following:
     demonstrating how to compose the essence of an \UNIX{}-style
     operating system with user session management, task parallelism,
     and file I/O using standard effects and handlers.
+\end{itemize}
+
+\paragraph{Implementation}
+\begin{itemize}
   \item A novel generalisation of the notion of continuation known as
     \emph{generalised continuation}, which provides a succinct
     foundation for implementing deep, shallow, and parameterised
@@ -1576,16 +1702,22 @@ The key contributions of this dissertation are the following:
   \item An abstract machine semantics based on generalised
     continuations, which characterises the low-level stack
     manipulations admitted by effect handlers at runtime.
+\end{itemize}
+\paragraph{Expressiveness}
+\begin{itemize}
   \item A formal proof that deep, shallow, and parameterised handlers
     are equi-expressible in the sense of typed macro-expressiveness.
   \item A robust mathematical characterisation of the computational
     efficiency of effect handlers, which shows that effect handlers
     can improve the asymptotic runtime of certain classes of programs.
-  \item A comprehensive operational characterisation of various
-    notions of continuations and first-class control phenomena.
 \end{itemize}
 
 \section{Structure of this dissertation}
+
+The following is a summary of the chapters belonging to each part of
+this dissertation.
+
+\paragraph{Background}
 Chapter~\ref{ch:maths-prep} defines some basic mathematical
 notation and constructions that are they pervasively throughout this
 dissertation.
@@ -1597,6 +1729,7 @@ the various first-class sequential control operators that appear in
 the literature. The application spectrum of continuations is discussed
 as well as implementation strategies for first-class control.
 
+\paragraph{Programming}
 Chapter~\ref{ch:base-language} introduces a polymorphic fine-grain
 call-by-value core calculus, $\BCalc$, which makes key use of
 \citeauthor{Remy93}-style row polymorphism to implement polymorphic
@@ -1612,6 +1745,7 @@ oriented programming in practice by implementing a small operating
 system dubbed \OSname{} based on \citeauthor{RitchieT74}'s original
 \UNIX{}.
 
+\paragraph{Implementation}
 Chapter~\ref{ch:cps} develops a higher-order continuation passing
 style translation for effect handlers through a series of step-wise
 refinements of an initial standard continuation passing style
@@ -1627,6 +1761,7 @@ continuations into \citeauthor{FelleisenF86}'s CEK machine to obtain
 an adequate abstract runtime with simultaneous support for deep,
 shallow, and parameterised handlers.
 
+\paragraph{Expressiveness}
 Chapter~\ref{ch:deep-vs-shallow} shows that deep, shallow, and
 parameterised notions of handlers can simulate one another up to
 specific notions of administrative reduction.
@@ -1642,6 +1777,7 @@ We show that $\HPCF$ admits an asymptotically more efficient
 implementation of generic count than any $\BPCF$ implementation.
 %
 
+\paragraph{Conclusions}
 Chapter~\ref{ch:conclusions} concludes and discusses future work.