ehop2022.links

# DISCLAIMER: THIS MODULE REQUIRES A SPECIAL BRANCH OF LINKS TO
# COMPILE: https://github.com/dhil/links/tree/multi-line-comments
# commit ddcc02d3 as the effect patterns are not yet available in
# master (you'll find that everything is implemented twice in this
# file, once with the "new" syntax, which is shadowed by an
# implementation using the "old" syntax).

## Prelude
typename Option(a) = [|None|Some:a|];

sig todo : (String) ~> a
fun todo(s) { error("TODO: " ^^ s) }

sig fail : () {Fail:Zero |_}-> a
fun fail() { switch (do Fail) { } }

sig lookup : (a, [(a, b)]) {Fail:Zero |_}~> b
fun lookup(k, kvs) {
  switch (kvs) {
    case [] -> fail()
    case (k', v) :: kvs' ->
      if (k == k') v
      else lookup(k, kvs')
  }
}

sig modify : (a, b, [(a, b)]) ~> [(a, b)]
fun modify(k, v, kvs) {
  switch (kvs) {
    case [] -> []
    case (k', v') :: kvs' ->
      if (k == k') (k, v) :: kvs'
      else (k', v') :: modify(k, v, kvs')
  }
}

sig remove : (a, [(a, b)]) ~> [(a, b)]
fun remove(k, kvs) {
  switch (kvs) {
    case [] -> []
    case (k', v') :: kvs' ->
      if (k == k') kvs'
      else (k', v') :: remove(k, kvs')
  }
}

sig has : (a, [(a, b)]) ~> Bool
fun has(k, kvs) {
  switch (kvs) {
    case [] -> false
    case (k', _) :: kvs' ->
      k == k' || has(k, kvs')
  }
}

#!
#
#            Effect Handler Oriented Programming
#                Lets build an operating system
#                    Daniel Hillerström
#       Laboratory for Foundations of Computer Science
#         The University of Edinburgh, Scotland, UK
#
#             Elements of Programming Languages
#                     November 17, 2022
#
#                https://dhil.net/research/
#
#?

#!
#
# Non-local control is pervasive in programming languages
#
#  * Async/await
#  * Coroutines
#  * Lightweight threads
#  * Generators and iterators
#  * First-class continuations
#
#
#
#?

#!
#
# Non-local control is pervasive in programming languages
#
#  * Async/await (e.g. C++, Dart, JavaScript, Rust, Swift)
#  * Coroutines (e.g. C++, Kotlin, Python, Swift)
#  * Lightweight threads (e.g. Erlang, Go, Haskell, Java, Swift)
#  * Generators and iterators (e.g. C#, Dart, Haskell, JavaScript, Kotlin, Python)
#  * First-class continuations (e.g. Haskell, Java, OCaml, Scheme)
#
#
#
#?

#!
#
# Non-local control is pervasive in programming languages
#
#  * Async/await (e.g. C++, Dart, JavaScript, Rust, Swift)
#  * Coroutines (e.g. C++, Kotlin, Python, Swift)
#  * Lightweight threads (e.g. Erlang, Go, Haskell, Java, Swift)
#  * Generators and iterators (e.g. C#, Dart, Haskell, JavaScript, Kotlin, Python)
#  * First-class continuations (e.g. Haskell, Java, OCaml, Scheme)
#
# Question: How should we implement such control abstractions?
#
#?

#{
#!
#
# Effect handlers: a modular abstraction for programmable control
#
# Plotkin and Pretnar (2009) invented effect handlers.

# Separates the syntax...
sig syn : (Int) {Op:(Int) -> Int |e}~> Int
fun syn(x) { do Op(x) }







#?
#}

#{
#!
#
# Effect handlers: a modular abstraction for programmable control
#
# Plotkin and Pretnar (2009) invented effect handlers.

# Separates the syntax...
sig syn : (Int) {Op:(Int) -> Int |e}~> b
fun syn(x) { do Op(x) }

# ... from the semantics of effectful operations
sig sem : (() {Op:(Int) -> Int |e}~> a) ~e~> a
fun sem(m) {
  handle(m()) {
    case ans               -> ans
    case <Op(p) => resume> -> resume(p+1)
  }
}
#?
#}

#!
#
# Characteristics of effect handlers
#
# * A structured form of delimited control
# * Offer a high-degree of modularity through seamless composition
# * Increase the expressiveness of user-written code
#
#
#?

#!
#
# Some ways to think about effect handlers
#
# Operational interpretation
#   Resumeable exceptions
#   Programmable and composable operating systems
#
# Software engineering interpretation
#   Composable monad builders (monads as a design pattern)
#
# Functional programming interpretation
#   Folds over computation trees
#   Free interpreters
#
# Mathematical interpretation
#   Homomorphisms between free algebraic models
#
#?

#!
#
# Some ways to think about effect handlers
#
# Operational interpretation                      <--- THIS LECTURE
#   Resumeable exceptions
#   Programmable and composable operating systems
#
# Software engineering interpretation
#   Composable monad builders (monads as a design pattern)
#
# Functional programming interpretation
#   Folds over computation trees
#   Free interpreters
#
# Mathematical interpretation
#   Homomorphisms between free algebraic models
#
#?

#!
#
# Effect handler oriented programming (EHOP)
#
# Key characteristics
#  - Extensive use of effect handlers
#  - High-degree of modularity
#  - Extremely compositional
#
# Some languages that support EHOP:
#   C/C++, Eff, Haskell, Koka, Links, Pyro, OCaml, Unison, Wasm
#
#?

#!
#
# Objectives of this lecture
#
# - Demonstrate the versatility of effect handler oriented programming
# - Explain Ritchie & Thompson's (1974) UNIX as the combination of
#   textbook effects
#    + Exceptions: Process termination
#    + Dynamic binding: User environments
#    + Nondeterminism: Time-sharing
#    + State: File system
#    + ...
#
#?

#!
#
# This lecture at glance
#
# A model of UNIX with
#   * support for multiple users,
#   * time-sharing amongst processes,
#   * and a file system.
#
# Self-imposed constraints
#   * Interface cannot be changed
#   * Everything has to be definable in the calculus
#
# Disclaimer: We'll make some gross simplifications. A richer model of
# UNIX can be found in my PhD dissertation
#
# (the idea of using delimited control to model operating systems is
#  not new, see e.g. Kiselyov and Shan (2007), Wand (1980))
#
#?

#!
#
# The key idea
#
# *System calls*         are an interface, implemented by an *operating system*
#
# *Effectful operations* are an interface, implemented by an *effect handler*
#
#?

#!
#
# The key idea
#
# *System calls*         are an interface, implemented by an *operating system*
#          =                                                        =
# *Effectful operations* are an interface, implemented by an *effect handler*
#
#?

#
#
# What is an operating system? (very abstractly)
#
# An operating system responds to a collection of system calls
#
# Example tasks:
#  - Signalling errors
#  - Scheduling processes
#  - Reading/writing I/O
#

#
#
# What is an effect handler? (very abstractly)
#
# An effect handler responds a collection of abstract operation calls
#
# Example tasks:
#  - Signalling errors
#  - Scheduling processes
#  - Reading/writing I/O
#
#
#
#
#
#

#
#
# What is an effect handler? (very abstractly)
#
# An effect handler responds a collection of abstract operation calls
#
# Example tasks:
#  - Signalling errors
#  - Scheduling processes
#  - Reading/writing I/O
#
# Thus an effect handler is an operating system (credit James McKinna)
# (Kiselyov and Shan (2007) used delimited continuations to model
#  operating systems)
#
#


#
#
# Objectives of this talk
#
# - Demonstrate the versatility of handlers
# - Explain operating systems as the combination of
#   + Exceptions
#   + Dynamic binding
#   + Nondeterminism
#   + State
#
#

#
#
# What is UNIX?
#
# UNIX is an operating system designed by Ritchie and Thompson (1974)
#
# Components
#  - Commands (system calls)
#    + I/O interaction, user session login, inter-process
#      communication, etc
#  - Kernel   (interpreter)
#    + Handling of I/O, managing user sessions, scheduling of
#      processes
#  - Development environment
#    + Compiler tool-chains (e.g. `cc`)
#  - Documentation
#    + manual pages (e.g. `man`)
#
#

#
#
# Key characteristics of UNIX (Ritchie & Thompson, 1974)
#
# - Support for multiple user sessions
# - Time-sharing between processes
# - "Everything is a file"
#
#

#{
#!
#
# Basic I/O: Performing writes
#
typename File = String;
typename FileDescr = Int;

sig stdout : FileDescr
var stdout = 1;

sig echo : (String) {Write:(FileDescr, String) -> ()}-> ()
fun echo(cs) { do Write(stdout, cs) }
#?
#}

typename File = String;
typename FileDescr = Int;

sig stdout : FileDescr
var stdout = 1;

sig echo : (String) {Write:(FileDescr, String) -> () |%}-> ()
fun echo(cs) { do Write(stdout, cs) }


#{
#!
#
# Basic I/O: Handling writes
#
sig basicIO : ( () {Write:(FileDescr, String) -> ()}-> a ) -> (a, File)
fun basicIO(m) {
  handle(m()) {
    case ans -> (ans, "")
    case <Write(fd, cs) => (resume : (()) -> (a, File))> ->
      var (ans, file) = resume(());
      (ans, cs ++ file)
  }
}
#?
#}

sig basicIO : ( () {Write:(FileDescr, String) -> () |%}-> a ) { |%}-> (a, File)
fun basicIO(m) {
   handle(m()) {
     case Return(ans) -> (ans, "")
     case Write(_, cs, resume) ->
       var (ans, file) = resume(());
       (ans, cs ^^ file)
   }
}

#{
#!
#
# Basic I/O: Example
#
sig example0 : () -> ((), File)
fun example0() {
  basicIO(fun() {
        echo("Hello"); echo("World")
  })
}
#?
#}

sig example0 : () { |%}-> ((), File)
fun example0() {
  basicIO(fun() {
        echo("Hello"); echo("World")
  })
}


#!
#
# Dynamic semantics of handlers
#
#  (ret) handle(V) { case x -> N case ... }
#        ~> N[V/x]
#
#  (op)  handle(E[do Op(V)]) { case <Op(p) => r> -> N case ... }
#        ~> N[V/p
#            ,fun(x){ handle(E[x]) { case <Op(p) => r> -> N case ... }}/r]
#        (if Op \notin E)
#
#?

#{
#!
#
# Exceptions: Premature exits
#
sig exit : (Int) {Exit:(Int) -> Zero}-> a
fun exit(n) { switch (do Exit(n)) { } }
#?
#}

sig exit : (Int) {Exit:(Int) -> Zero |%}-> a
fun exit(n) { switch (do Exit(n)) { } }


#{
#!
#
# Handling exits
#
sig status : (() {Exit:(Int) -> Zero}-> a) -> Int
fun status(m) {
  handle(m()) {
    case ans -> 0
    case <Exit(n)> -> n
  }
}
#?
#}

sig status : (() {Exit:(Int) -> Zero |%}-> a) { |%}-> Int
fun status(m) {
  handle(m()) {
    case Return(_) -> 0
    case Exit(n, _) -> n
  }
}

#{
#!
#
# Handling exits: Example
#
sig example1 : () -> (Int, File)
fun example1() {
  basicIO(fun() {
        status(fun() {
          echo("Hello"); exit(1); echo("World")
        })
  })
}
#?
#}

sig example1 : () { |%}-> (Int, File)
fun example1() {
  basicIO(fun() {
        status(fun() {
          echo("Hello"); exit(1); echo("World")
        })
  })
}

#{
#!
#
# Does the ordering of handlers matter?
#
sig example1' : () -> Int
fun example1'() {
  status(fun() {
    basicIO(fun() {
      echo("Hello"); exit(1); echo("World")
    })
  })
}
#?
#}

sig example1' : () { |%}-> Int
fun example1'() {
  status(fun() {
    basicIO(fun() {
      echo("dead"); exit(1); echo("code")
    })
  })
}

#{
#!
#
# Dynamic binding: User-specific environments (1)
#
typename User = [|Alice|Bob|Root|];

sig whoami : () {Ask:String}-> String
fun whoami() { do Ask }
#?
#}

typename User = [|Alice|Bob|Root|];

sig whoami : () {Ask:String |%}-> String
fun whoami() { do Ask }

#{
#!
#
# Dynamic binding: User-specific environments (2)
#
sig env : (User, () {Ask:String}-> a) -> a
fun env(user, m) {
  handle(m()) {
    case ans -> ans
    case <Ask => resume> ->
      switch (user) {
        case Alice -> resume("alice")
        case Bob   -> resume("bob")
        case Root  -> resume("root")
      }
  }
}


sig example2 : () -> String
fun example2() {
  env(Root, whoami)
}
#?
#}

sig env : (User, () {Ask:String |%}-> a) { |%}-> a
fun env(user, m) {
  handle(m()) {
    case Return(x) -> x
    case Ask(resume) ->
      switch (user) {
        case Alice -> resume("alice")
        case Bob   -> resume("bob")
        case Root  -> resume("root")
      }
  }
}


sig example2 : () { |%}-> String
fun example2() {
  env(Root, whoami)
}

#!
#
# Aside: Dynamic binding with delimited continuations
#
# The idea of dynamic binding dates back to at least McCarthy (1960)
#
# Kiselyov, Shan, and Sabry (2006) demonstrated dynamic binding can be
# simulated with delimited continuations
#
#?

#{
#!
#
# User session management
#
sig su : (User) {Su:(User) -> ()}-> ()
fun su(user) { do Su(user) }

sig sessionmgr : (User, () {Ask:String, Su:(User) -> ()}-> a) -> a
fun sessionmgr(user, m) {
   env(user, fun() {
     handle(m()) {
       case ans -> ans
       case <Su(user') => resume> ->
         env(user', fun() { resume(()) })
     }
   })
}
#?
#}

sig su : (User) {Su:(User) -> () |%}-> ()
fun su(user) { do Su(user) }

sig sessionmgr : (User, () {Ask:String, Su:(User) -> () |%}-> a) { |%}-> a
fun sessionmgr(user, m) {
  env(user, fun() {
     handle(m()) {
       case Return(ans) -> ans
       case Su(user', resume) ->
         env(user', fun() { resume(()) })
     }
  })
}

#{
#!
#
# Multiple user sessions example
#
sig example3 : () -> (Int, File)
fun example3() {
  basicIO(fun() {
        sessionmgr(Root, fun() {
          status(fun() {
            su(Alice); echo(whoami()); echo(" ");
            su(Bob);   echo(whoami()); echo(" ");
            su(Root);  echo(whoami())
          })
        })
  })
}
#?
#}

sig example3 : () { |%}-> (Int, File)
fun example3() {
  basicIO(fun() {
        sessionmgr(Root, fun() {
          status(fun() {
            su(Alice); echo(whoami()); echo(" ");
            su(Bob);   echo(whoami()); echo(" ");
            su(Root);  echo(whoami())
          })
        })
  })
}

#!
#
# Nondeterminism: Multi-tasking (1)
#
# From the man pages.
#
# Description
#   fork() creates a new process by duplicating the calling process.  The
#   new process is referred to as the child process.  The calling process
#   is referred to as the parent process.
#
# Return value
#   On success, the PID of the child process is returned in the parent,
#   and 0 is returned in the child.
#
#?

#!
#
# Nondeterminism: Multi-tasking (2)
#
# Fork idiom
#
#    if (fork() > 0) parent's code
#    else child's code
#
# Let's simplify fork such that it returns a boolean: true for parent,
# false for child.
#
#?

#{
#!
#
# Nondeterminism: Multi-tasking (3)
#
sig fork : () {Fork:Bool}-> Bool
fun fork() { do Fork }

sig nondet : (() {Fork:Bool}-> a) -> [a]
fun nondet(m) {
  handle(m()) {
    case ans -> [ans]
    case <Fork => resume> ->
      resume(true) ++ resume(false)
  }
}
#?
#}

sig fork : () {Fork:Bool |_}-> Bool
fun fork() { do Fork }

sig nondet : (() {Fork:Bool |%}-> a) { |%}-> [a]
fun nondet(m) {
  handle(m()) {
    case Return(ans)  -> [ans]
    case Fork(resume) -> resume(true) ++ resume(false)
  }
}

#{
#!
#
# Nondeterminism: Example (1)
#
sig ritchie : () {Write:(FileDescr, String) -> ()}-> ()
fun ritchie() {
  echo("UNIX is basically ");
  echo("a simple operating system, ");
  echo("but ");
  echo("you have to be a genius to understand the simplicity.\n")
}

sig hamlet : () {Write:(FileDescr, String) -> ()}-> ()
fun hamlet() {
  echo("To be, or not to be,\n");
  echo("that is the question:\n");
  echo("Whether 'tis nobler in the mind to suffer\n")
}
#?
#}
sig ritchie : () {Write:(FileDescr, String) -> () |%}-> ()
fun ritchie() {
  echo("UNIX is basically ");
  echo("a simple operating system, ");
  echo("but ");
  echo("you have to be a genius to understand the simplicity.\n")
}

sig hamlet : () {Write:(FileDescr, String) -> () |%}-> ()
fun hamlet() {
  echo("To be, or not to be,\n");
  echo("that is the question:\n");
  echo("Whether 'tis nobler in the mind to suffer\n")
}

#{
#!
#
# Nondeterminism: Example (2)
#
sig example4 : () -> ([Int], File)
fun example4() {
  basicIO(fun() {
    nondet(fun() {
      sessionmgr(Root, fun() {
        status(fun() {
          if (fork()) {
            su(Alice);
            ritchie()
          } else {
            su(Bob);
            hamlet()
          }
        })
      })
    })
  })
}
#?
#}

sig example4 : () { |%}-> ([Int], File)
fun example4() {
  basicIO(fun() {
    nondet(fun() {
      sessionmgr(Root, fun() {
        status(fun() {
          if (fork()) {
            su(Alice);
            ritchie()
          } else {
            su(Bob);
            hamlet()
          }
        })
      })
    })
  })
}

#
#
# Mathematically well-founded nondeterminism
#
# The handler `nondet` is _exactly_ the handler Plotkin and Pretnar (2013)
# give for nondeterminism
# It satisfies the usual (semi-lattice) equations for nondeterministic choice, i.e.
#
#   if (fork()) M else M                        = M
#   if (fork()) M else N                        = if (fork()) N else M
#   if (fork()) L else { if (fork()) M else N } = if (fork()) { if (fork()) L else M } else N
#
#

#{
#!
#
# Interrupting processes
#
sig interrupt : () {Interrupt:()}-> ()
fun interrupt() { do Interrupt }

# Process reification
typename Pstate(a::Type, e::Eff)
         = [|Done:a
            |Paused:() -e-> Pstate(a, e)|];


sig reifyProcess : (() {Interrupt:() |e}-> a) -e-> Pstate(a, e)
fun reifyProcess(m) {
  handle(m()) {
    case ans -> Done(ans)
    case <Interrupt => resume> ->
      Paused(fun() { resume(()) })
  }
}
#?
#}

sig interrupt : () {Interrupt:() |%}-> ()
fun interrupt() { do Interrupt }

typename Pstate(a,e::Eff)
         = forall q::Presence.
           [|Done:a
            |Paused:() {Interrupt{q} |e}-> Pstate(a, { |e})|];


sig reifyProcess : (() {Interrupt:() |%}-> a) { |%}-> Pstate(a, { |%})
fun reifyProcess(m) {
  handle(m()) {
    case Return(ans) -> Done(ans)
    case Interrupt(resume) -> Paused(fun() { resume(()) })
  }
}

#{
#!
#
# Time-sharing via interrupts
#
sig schedule : ([Pstate(a, {Fork:Bool})]) -> [a]
fun schedule(ps) {
  fun schedule(ps, done) {
    switch (ps) {
      case [] -> done
      case Done(res) :: ps' ->
        schedule(ps', res :: done)
      case Paused(resume) :: ps' ->
        schedule(ps' ++ nondet(resume), done)
    }
  }
  schedule(ps, [])
}

sig timeshare : (() {Fork:Bool,Interrupt:()}-> a) -> [a]
fun timeshare(m) {
  var p = Paused(fun() { reifyProcess(m) });
  schedule([p])
}
#?
#}

sig schedule : ([Pstate(a, { Fork:Bool |%})]) { |%}~> [a]
fun schedule(ps) {
  fun schedule(ps, done) {
    switch (ps) {
      case [] -> done
      case Done(res) :: ps' ->
        schedule(ps', res :: done)
      case Paused(resume) :: ps' ->
        schedule(ps' ++ nondet(resume), done)
    }
  }
  schedule(ps, [])
}

sig timeshare : (() {Fork:Bool,Interrupt:() |%}-> a) { |%}-> [a]
fun timeshare(m) {
  var p = Paused(fun() { reifyProcess(m) });
  schedule([p])
}

#{
#!
#
# Injecting interrupts
#
# First idea: external source injects interrupts (Ahman and Pretnar (2021))
#
# Second idea: bundle interrupts with other operations
sig echo' : (FileDescr,String) {Interrupt:(), Write:(FileDescr,String) -> ()}-> ()
fun echo'(fd, cs) { interrupt(); do Write(fd, cs) }
#
# Third idea: overload interpretations of operations
sig interruptWrite : (() {Write:(FileDescr,String) -> ()}-> a)
                              {Interrupt:(),Write:(FileDescr,String) -> ()}-> a
fun interruptWrite(m) {
  handle(m()) {
    case ans -> ans
    case <Write(fd, cs) => resume> ->
      interrupt(); resume(do Write(fd, cs))
  }
}
#?
#}

sig interruptWrite : (() {Write:(FileDescr,String) -> () |%}-> a)
                              {Write:(FileDescr,String) -> () |%}-> a
fun interruptWrite(m) {
  handle(m()) {
    case Return(res) -> res
    case Write(fd, cs, resume) ->
      interrupt(); resume(do Write(fd, cs))
  }
}

#{
#!
#
# Time-sharing example
#
sig example5 : () -> ([Int], File)
fun example5() {
  basicIO(fun() {
    timeshare(fun() {
      interruptWrite(fun() {
        sessionmgr(Root, fun() {
          status(fun() {
            if (fork()) {
              su(Alice);
              ritchie()
            } else {
              su(Bob);
              hamlet()
            }
          })
        })
      })
    })
  })
}
#?
#}
sig example5 : () { |%}-> ([Int], File)
fun example5() {
  basicIO(fun() {
    timeshare(fun() {
      interruptWrite(fun() {
        sessionmgr(Root, fun() {
          status(fun() {
            if (fork()) {
              su(Alice);
              ritchie()
            } else {
              su(Bob);
              hamlet()
            }
          })
        })
      })
    })
  })
}

#{
#!
#
# State: File I/O
#
# Generic state handling
sig get : () {Get:s}-> s
fun get() { do Get }

sig put : (s) {Put:(s) -> ()}-> ()
fun put(st) { do Put(st) }

sig runState : (s, () {Get:() -> s,Put:(s) -> ()}-> a) -> (a, s)
fun runState(st0, m) {
  var f = handle(m()) {
    case ans                  -> fun(st) { (ans, st) }
    case <Get      => resume> -> fun(st) { resume(st)(st) }
    case <Put(st') => resume> -> fun(_)  { resume(())(st') }
  };
  f(st0)
}
#?
#}

sig get : () {Get:s |_}-> s
fun get() { do Get }

sig put : (s) {Put:(s) -> () |_}-> ()
fun put(st) { do Put(st) }

sig runState : (s, () {Get:() -> s,Put:(s) -> () |%}-> a) { |%}-> (a, s)
fun runState(st0, m) {
  var f = handle(m()) {
    case Return(x)       -> fun(st) { (x, st) }
    case Get(resume)     -> fun(st) { resume(st)(st) }
    case Put(st',resume) -> fun(_)  { resume(())(st') }
  };
  f(st0)
}

#{
#!
#
# State: Example
#
sig incr : () {Get:Int,Put:(Int) -> ()}-> ()
fun incr() { put(get() + 1) }

sig example6 : () -> ((), Int)
fun example6() {
  runState(41, incr)
}
#?
#}

sig incr : () {Get:Int,Put:(Int) -> () |%}-> ()
fun incr() { put(get() + 1) }

sig example6 : () { |%}-> ((), Int)
fun example6() {
  runState(41, incr)
}

#!
#
# Basic Serial File System (BSFS)
#
#     Directory              I-List              Data region
# +----------------+        +-------+     +--------------------------+
# | "hamlet"       |------> |   2   |---> | "To be, or not to be..." |
# +----------------+     /  +-------+     +--------------------------+
# | "richtie.txt"  |------> |   1   |---> | "UNIX is basically..."   |
# +----------------+    /   +-------+     +--------------------------+
# | ...            |    |   |  ...  |     | ...                      |
# +----------------+    |   +-------+     +--------------------------+
# | "stdout"       |------> |   1   |---> | ""                       |
# +----------------+    |   +-------+     +--------------------------+
# | ...            |    /
# +----------------+   /
# | "act3"         |---
# +----------------+
#
# Simplifications:
#   - Operating directly on inode pointers
#   - Reads and writes will be serial
#
#?

#{
#!
#
# BSFS structures
#
typename INode      = (loc:Int,lno:Int);
typename IList      = [(Int, INode)];  # INode index -> INode
typename Directory  = [(String, Int)]; # Filename -> INode index
typename DataRegion = [(Int, File)];   # Loc -> File

typename FileSystem = (dir:Directory,dregion:DataRegion,inodes:IList
                                    ,lnext:Int         ,inext:Int    );

sig fsys0 : FileSystem
var fsys0 = ( dir     = [("stdout", 0)]
            , inodes  = [(0, (loc=0, lno=1))]
            , dregion = [(0, "")]
            , lnext = 1, inext = 1 );


# Utility functions
sig lookup : (a, [(a, b)]) {Fail:Zero}-> b
var lookup = lookup;

sig withDefault : (a, () {Fail:Zero}-> a) -> a
fun withDefault(d, m) {
  handle(m()) {
    case ans    -> ans
    case <Fail> -> d
  }
}
#?
#}

typename INode      = (loc:Int,lno:Int);
typename IList      = [(Int, INode)];  # INode index -> INode
typename Directory  = [(String, Int)]; # Filename -> INode index
typename DataRegion = [(Int, File)];   # Loc -> File

typename FileSystem = (dir:Directory,dregion:DataRegion,inodes:IList
                                    ,lnext:Int         ,inext:Int    );

sig fsys0 : FileSystem
var fsys0 = ( dir     = [("stdout", 0)]
            , inodes  = [(0, (loc=0, lno=1))]
            , dregion = [(0, "")]
            , lnext = 1, inext = 1 );


# Utility functions
sig lookup : (a, [(a, b)]) {Fail:Zero |%}-> b
var lookup = lookup;

sig withDefault : (a, () {Fail:Zero |%}-> a) { |%}-> a
fun withDefault(x', m) {
  handle(m()) {
    case Return(x) -> x
    case Fail(_)   -> x'
  }
}

sig fwrite : (Int, String, FileSystem) {Fail:Zero |%}-> FileSystem
fun fwrite(ino, cs, fsys) {
  var inode = lookup(ino, fsys.inodes);
  var file  = lookup(inode.loc, fsys.dregion);
  var file' = file ^^ cs;
  (fsys with dregion = modify(inode.loc, file', fsys.dregion))
}

sig fread : (Int, FileSystem) {Fail:Zero |%}-> String
fun fread(ino, fsys) {
  var inode = lookup(ino, fsys.inodes);
  lookup(inode.loc, fsys.dregion)
}

#{
#!
#
# Handling BSFS operations: file reading and writing
#
sig fwrite : (FileDescr, String, FileSystem) {Fail:Zero}-> FileSystem
var fwrite = fwrite;
sig fread : (FileDescr, FileSystem) {Fail:Zero}-> String
var fread = fread;

sig fileRW : ( () { Read :(FileDescr) -> Option(String)
                  , Write:(FileDescr, String) -> ()    }-> a )
                          {Get:FileSystem,Put:(FileSystem) -> ()}-> a
fun fileRW(m) {
  handle(m()) {
    case ans -> ans
    case <Read(fd) => resume> ->
      var cs = withDefault(None, fun() {
                 Some(fread(fd, get()))
      }); resume(cs)
    case <Write(fd, cs) => resume> ->
      withDefault((), fun() {
        var fsys = fwrite(fd, cs, get());
        put(fsys)
      }); resume(())
  }
}
#?
#}

sig fileRW : ( () { Read :(FileDescr) -> Option(String)
                  , Write:(FileDescr, String) -> ()     |%}-> a )
                          {Get:FileSystem,Put:(FileSystem) -> () |%}-> a
fun fileRW(m) {
  handle(m()) {
    case Return(ans) -> ans
    case Read(fd, resume) ->
      var cs = withDefault(None, fun() {
                 Some(fread(fd, get()))
      }); resume(cs)
    case Write(fd, cs, resume) ->
      withDefault((), fun() {
        var fsys = fwrite(fd, cs, get());
        put(fsys)
      }); resume(())
  }
}

sig fopen : (String, FileSystem) {Fail:Zero |%}-> FileDescr
fun fopen(fname, fsys) { lookup(fname, fsys.dir) }

sig fcreate : (String, FileSystem) {Fail:Zero |%}-> (FileDescr, FileSystem)
fun fcreate(fname, fsys) {
  if (has(fname, fsys.dir)) {
    var ino = fopen(fname, fsys);
    # Truncate file
    var inode = lookup(ino, fsys.inodes);
    var dregion = modify(inode.loc, "", fsys.dregion);
    (ino, (fsys with =dregion))
  } else {
    var loc = fsys.lnext;
    var dregion = (loc, "") :: fsys.dregion;

    var ino   = fsys.inext;
    var inode = (loc=loc,lno=1);
    var inodes = (ino, inode) :: fsys.inodes;

    var dir = (fname, ino) :: fsys.dir;
    (ino, (=dir, =dregion, =inodes, lnext=loc+1, inext=ino+1))
  }
}

#{
#!
#
# BSFS operation: file opening and creation
#
sig fopen : (String, FileSystem) {Fail:Zero}-> FileDescr
var fopen = fopen;
sig fcreate : (String, FileSystem) {Fail:Zero}-> (FileDescr, FileSystem)
var fcreate = fcreate;

sig fileOC : ( () { Open  :(String) -> Option(FileDescr)
                  , Create:(String) -> Option(FileDescr) }-> a )
                          {Get:FileSystem,Put:(FileSystem) -> () }-> a
fun fileOC(m) {
  handle(m()) {
    case ans -> ans
    case <Open(fname) => resume> ->
      var fd = withDefault(None, fun() {
                 Some(fopen(fname, get()))
      }); resume(fd)
    case <Create(fname) => resume> ->
      var fd = withDefault(None, fun() {
                 var (fd, fsys) = fcreate(fname, get());
                 put(fsys); Some(fd)
      }); resume(fd)
  }
}
#?
#}

sig fileOC : ( () { Open  :(String) -> Option(FileDescr)
                  , Create:(String) -> Option(FileDescr) |%}-> a )
                          {Get:FileSystem,Put:(FileSystem) -> () |%}-> a
fun fileOC(m) {
  handle(m()) {
    case Return(ans) -> ans
    case Open(fname, resume) ->
      var fd = withDefault(None, fun() {
                 Some(fopen(fname, get()))
      }); resume(fd)
    case Create(fname, resume) ->
      var fd = withDefault(None, fun() {
                 var (fd, fsys) = fcreate(fname, get());
                 put(fsys); Some(fd)
      }); resume(fd)
  }
}

#{
#!
#
# BSFS version 0
#
sig bsfs0 : ( () {  Open  :(String) -> Option(FileDescr)
                  , Create:(String) -> Option(FileDescr)
                  , Read :(FileDescr) -> Option(String)
                  , Write:(FileDescr, String) -> ()      }-> a )
                          {Get:FileSystem,Put:(FileSystem) -> ()}-> a
fun bsfs0(m) {
  fileOC(fun() {
    fileRW(m)
  })
}
#?
#}

sig bsfs0 : ( () {  Open  :(String) -> Option(FileDescr)
                  , Create:(String) -> Option(FileDescr)
                  , Read :(FileDescr) -> Option(String)
                  , Write:(FileDescr, String) -> ()     |%}-> a )
                          {Get:FileSystem,Put:(FileSystem) -> () |%}-> a
fun bsfs0(m) {
  fileOC(fun() {
    fileRW(m)
  })
}

#{
#!
#
# Stream redirection
#
sig > : (() -> a, String)
             { Create:(String) -> Option(FileDescr)
             , Exit  : (Int) -> Zero
             , Write :(FileDescr,String) -> ()      }-> a
op f > fname {
  var fd = switch (do Create(fname)) {
             case None -> exit(-1)
             case Some(fd) -> fd
  }; handle(f()) {
      case ans -> ans
      case <Write(_, cs) => resume> ->
       resume(do Write(fd, cs))
    }
}
#?
#}

sig >- : (() { |%}-> a, String)
                { Create:(String) -> Option(FileDescr)
                , Exit  : (Int) -> Zero
                , Write :(FileDescr,String) -> ()      |%}-> a
op f >- fname {
  var fd = switch (do Create(fname)) {
             case None -> exit(-1)
             case Some(fd) -> fd
  }; handle(f()) {
      case Return(x) -> x
      case Write(_, cs, resume) ->
       resume(do Write(fd, cs))
    }
}

#{
#!
#
# Crude copy
#
sig ccp : (String, String) { Create:(String) -> Option(FileDescr)
                           , Exit  :(Int) -> Zero
                           , Read  :(FileDescr) -> Option(String)
                           , Open  :(String) -> Option(FileDescr)
                           , Write :(FileDescr,String) -> ()      }-> ()
fun ccp(src, dst) {
  var srcfd = switch (do Open(src)) {
    case None -> exit(-1)
    case Some(fd) -> fd
  };
  switch (do Read(srcfd)) {
    case None -> exit(-1)
    case Some(cs) -> fun() {echo(cs)} > dst
  }
}
#?
#}

sig ccp : (String, String) { Create:(String) -> Option(FileDescr)
                           , Exit  :(Int) -> Zero
                           , Read  :(FileDescr) -> Option(String)
                           , Open  :(String) -> Option(FileDescr)
                           , Write :(FileDescr,String) -> ()      |%}-> ()
fun ccp(src, dst) {
  var srcfd = switch (do Open(src)) {
    case None -> exit(-1)
    case Some(fd) -> fd
  };
  switch (do Read(srcfd)) {
    case None -> exit(-1)
    case Some(cs) -> fun() {echo(cs)} >- dst
  }
}

#{
#!
#
# Plugging everything together
#
sig example7 : () -> ([Int], FileSystem)
fun example7() {
  runState(fsys0, fun() {
    bsfs0(fun() {
      timeshare(fun() {
        interruptWrite(fun() {
          sessionmgr(Root, fun() {
            status(fun() {
              if (fork()) {
                su(Alice);
                ritchie > "ritchie.txt"
              } else {
                su(Bob);
                hamlet > "hamlet";
                ccp("hamlet", "act3")
              }
            })
          })
        })
      })
    })
  })
}
#?
#}

sig example7 : () { |%}-> ([Int], FileSystem)
fun example7() {
  runState(fsys0, fun() {
    bsfs0(fun() {
      timeshare(fun() {
        interruptWrite(fun() {
          sessionmgr(Root, fun() {
            status(fun() {
              if (fork()) {
                su(Alice);
                ritchie >- "ritchie.txt"
              } else {
                su(Bob);
                hamlet >- "hamlet";
                ccp("hamlet", "act3")
              }
            })
          })
        })
      })
    })
  })
}

#!
#
# Conclusion
#
# + Effect handlers are a versatile programming abstraction
# + Possible to retrofit legacy code with new functionality
# + Operating systems can be explained in terms of handlers
# + "Every problem can be solved by adding another handler"
#
# See my PhD dissertation[1] for an implementation of UNIX fork, usage of
# shallow handlers to implement a more UNIX-y shell environment.
#
# [1] "Foundations for Programming and Implementing Effect Handlers",
#     Daniel Hillerström, PhD dissertation, The University of
#     Edinburgh, Scotland, UK, 2021.
#
#?