Prototype IO proxy handler for record/replay in Unison

IO-record-replay.u

-- This gist demonstrates a prototype IO proxy handler for record/replay.  
-- The hope is to get some version of this into unisonbase someday.  
--
-- More motivation and explanation is at https://github.com/unisonweb/unison/issues/258.
--
-- It currently only handles a few IO primitives - there's a bunch of boilerplate code 
-- needed to handle the rest.  And see 'Limitations' below for issues coming out of this
-- prototyping.  
-- 
-- The aim is to provide the following:
--
--   recordIO : Request IO t ->{IO} (t, IORecord)
--   replayIO : IORecord -> Request IO t ->{Exception (IOReplayException t)} IOResult t
--
-- So, record all the input/output done by your IO computation, then feed it back into your
-- code later, running as a pure computation, to play about with either in some kind of debugger, or
-- as you tweak the code by adding logging.  
--
-- *** USAGE ***
--
-- Given a program : '{IO} Nat
-- 
--   case (handle recordIO in !program) of
--    (nat, recording) -> ...
--
-- Given a recording, record : IORecord
--
--   case (handle exceptionToEither in (handle replayIO record in !program)) of
--      Either.Right (IOResult.Completed nat) -> ...
--
-- One way to get a window into the program being replayed is to instrument it.  You could write:
--
--   ability Log where
--     log : Text -> ()
--
--   program : '{IO, Log} Nat
--
--   replay : IORecord -> ('{IO, Log} a) ->{Log} a
--
-- *** LIMITATIONS ***
-- 
-- This is not very useful yet because Unison doesn't yet have:
-- - convenient typed data persistence, so you can't store your recordings to examine later
-- - Universal.toText (or similar), so you can't view a print-out of the recordings
--
-- It's also not complete:
-- - it needs all the boilerplate code writing for the various IO primitives: it currently only
--   covers getLine_, putText_, and a handful of others
-- - although fork is exposed in .base.io.IO, other concurrency primitives are not, so there's
--   no way to get a hold of any recordings made in forked child threads
-- - there are some issues around recording calls to bracket, which need a bit of experiment/
--   prototyping (see IOReplayException.BracketUnsupported below), and which anyway might 
--   point to deeper snags around recording computations that hit exceptions (especially
--   asynchronous exceptions as described at http://hackage.haskell.org/package/base-4.12.0.0/docs/Control-Exception.html#g:10).

use .base
use .base.io

-- the following bit of preamble to go in .base

ability Exception e where
  raise : e -> a

exceptionToEither : Request (Exception e) a -> Either e a
exceptionToEither r = case r of
  { Exception.raise e -> k } -> Either.Left e
  { a } -> Either.Right a

-- the following to go in .base.io.record

-- A recording of the IO performed during execution of an IO computation.
-- We store the list of calls made to IO primitives.  (There is actually some tree-like structure
-- here, or will be in future, see IORecord'.fork_).
type IORecord = IORecord [IORecord']
  
-- To replay computations we only need to store the return values from each IO primitive, i.e.
-- the inputs to the program.  But we store the arguments to the IO primitives as well (which are 
-- outputs from the program) to check the program is making the same IO calls on replay as it did
-- during recording.  
type IORecord' = 
    getLine_ .base.io.Handle (.base.Either .base.io.Error .base.Text)
  | putText_ .base.io.Handle .base.Text (.base.Either .base.io.Error ())
  -- TODO insert lots more formulaic stuff here      
  -- ...
  -- and finally these are the special cases:
  | throw .base.io.Error
  -- When IO supports enough stuff to build a simple future on, there will be an extra 
  -- (Future IORecord) giving the IORecord from the forked child thread.
  | fork_ ('{.base.io.IO} ()) (.base.Either .base.io.Error .base.io.ThreadId) -- Future IORecord
  -- (Need to use existentials to capture the args and return value of bracket.)
  | bracket_ (.base.Either .base.io.Error ())

-- Just the arguments to each IO primitive - used by IOReplayException.RequestMismatch.
type IORequest = 
    getLine_ .base.io.Handle
  | putText_ .base.io.Handle .base.Text
  -- insert lots more formulaic stuff here      
  -- ...
  -- and finally these are the special cases:
  | throw .base.io.Error
  | fork_ ('{.base.io.IO} ())
  | bracket_ 

-- A wrapper around the result of an '{IO} t computation, capturing cases where it calls to 
-- .base.io.throw_.  
-- TODO more general issues around exceptions need more thought.  Ideally we want our recording 
-- to still be produced in cases of exceptions, especially since those cases are ones where
-- examining and replaying a recording might be particularly useful.  
type IOResult t = 
    Completed t
  -- The computation did a .base.io.throw    
  | Throw .base.io.Error

-- We want to allow new code to be run against a recording produced by old code, as long as the IO 
-- that is happening is the same.  IOReplayException describes mismatches between the IO done by the 
-- old code, and the IO requested by the new code.  
-- Ideally the IORecord elements would be replaced by indices (or zippers) into the overall IORecord, showing which 
-- thread you're in, rather than just records of the remaining computation at the point there was a mismatch.
type IOReplayException a = 
    -- The computation completed without performing all the requests in the record.
    -- args: the expected remaining record; result of actual computation
    EarlyCompletion IORecord (IOResult a)
    -- The computation made a request that doesn't match the recording (either in the type of the
    -- request or the value of an argument passed to it).
    -- This includes the case where the computation makes more requests than are in the recording, in
    -- which case the recording returned here will be empty.  
    -- Note that the matching-argument-values check skips function values.
    -- args: expected remaining requests according to recording; actual next request from current computation
  | RequestMismatch IORecord IORequest
    -- TODO recordIO cannot currently record IO performed in child threads created by .base.io.fork_, so
    -- computation in those threads cannot be replayed.  We flag this by raising an exception from the 
    -- parent thread when it tries to replay a fork_ call.
  | ForkUnsupported
    -- TODO recordIO cannot currently record computations which use bracket_, due to difficulties coming from 
    -- (a) its return value not being of a fixed type, (b) inability to retrieve the recording from the 
    -- 'release' step.
  | BracketUnsupported

recordIO : Request IO t ->{IO} (t, IORecord)
recordIO req = case recordIO_ (IORecord []) req of
  (IOResult.Completed t, record) -> (t, record)
  (IOResult.Throw e, record) -> IO.throw e

recordIO_ : IORecord -> Request IO t ->{IO} (IOResult t, IORecord)
recordIO_ record request = case request of
  { IO.getLine_ a -> k } -> 
    r = IO.getLine_ a
    case record of 
      IORecord.IORecord record' -> 
        handle recordIO_ (IORecord.IORecord (record' :+ IORecord'.getLine_ a r)) in k r
  { IO.putText_ a b -> k } -> 
    r = IO.putText_ a b
    case record of 
      IORecord.IORecord record' -> 
        handle recordIO_ (IORecord.IORecord (record' :+ IORecord'.putText_ a b r)) in k r
  -- insert lots more formulaic stuff here      
  -- ...
  -- and finally deal with the special cases:
  { IO.throw a -> k } -> 
    case record of 
      IORecord.IORecord record' -> (IOResult.Throw a, (IORecord.IORecord (record' :+ IORecord'.throw a)))
  { IO.fork_ a -> k } -> 
    -- When IO supports enough stuff to build a simple future on, wrapChild will:
    -- - wrap the computation in a "handle recordIO_"
    -- - get the child record fed back into a future in the parent record.
    -- See IOReplayException.ForkUnsupported.
    wrapChild : '{.base.io.IO} q -> '{.base.io.IO} q
    wrapChild = id
    r = IO.fork_ (wrapChild a)
    case record of 
      IORecord.IORecord record' -> 
        handle recordIO_ (IORecord.IORecord (record' :+ IORecord'.fork_ a r)) in k r
  { IO.bracket_ a b c -> k } -> 
    -- This is incomplete - see IOReplayException.BracketUnsupported
    r = IO.bracket_ a b c
    case record of 
      IORecord.IORecord record' -> 
        handle recordIO_ (IORecord.IORecord (record' :+ IORecord'.bracket_ r)) in k r
  { t } -> (IOResult.Completed t, record)

replayIO : IORecord -> Request IO t ->{Exception (IOReplayException t)} IOResult t
replayIO record request = 
  and' a b = and a b
  case request of
    { IO.getLine_ a -> k } ->
      case record of 
        IORecord.IORecord ((IORecord'.getLine_ a' r) +: rest) | a == a' -> handle replayIO (IORecord.IORecord rest) in k r
        _ -> Exception.raise (IOReplayException.RequestMismatch record (IORequest.getLine_ a))
    { IO.putText_ a b -> k } ->
      case record of 
        IORecord.IORecord ((IORecord'.putText_ a' b' r) +: rest) | and' (a == a') (b == b') -> handle replayIO (IORecord.IORecord rest) in k r
        _ -> Exception.raise (IOReplayException.RequestMismatch record (IORequest.putText_ a b))
  -- insert lots more formulaic stuff here      
  -- ...
  -- and finally deal with the special cases:
    { IO.throw a -> k } ->
      case record of 
        IORecord.IORecord ((IORecord'.throw a') +: rest) | a == a' -> 
          if size rest == 0
          then IOResult.Throw a
          else Exception.raise (IOReplayException.EarlyCompletion (IORecord.IORecord rest) (IOResult.Throw a))
        _ -> Exception.raise (IOReplayException.RequestMismatch record (IORequest.throw a))
    { IO.fork_ a -> k } -> Exception.raise IOReplayException.ForkUnsupported
    { IO.bracket_ a b c -> k } -> Exception.raise IOReplayException.BracketUnsupported
    { t } -> 
      case record of 
        IORecord.IORecord l | size l == 0 -> IOResult.Completed t
        _ -> Exception.raise (IOReplayException.EarlyCompletion record (IOResult.Completed t))

-- the following just to show it working, not for inclusion in unisonbase

eg : '{IO} Text
eg = 'let
       l = getLine stdin
       l

egRecorded : '{IO} ()
egRecorded = 'let
  case (handle recordIO in !eg) of
    (line, IORecord.IORecord l) -> 
      case l of 
        (IORecord'.getLine_ _ (Either.Right line')) +: rest -> 
          printLine ("You said " ++ line ++ " and I recorded " ++ line')

egRecordedReplayed : '{IO} ()
egRecordedReplayed = 'let
  case (handle recordIO in !eg) of
    (line, record) -> 
      case (handle exceptionToEither in (handle replayIO record in !eg)) of
        Either.Right (IOResult.Completed line') -> printLine ("First I got " ++ line ++ " then on the replay I got " ++ line')

thrower : '{IO} Text
thrower = '(IO.throw (Error.Error ErrorType.IllegalOperation "bad!"))

throwerRecorded : '{IO} (IOResult Text, IORecord)
throwerRecorded = '(handle recordIO_ (IORecord []) in !thrower)

throwerRecordedReplayed : '{IO} ()
throwerRecordedReplayed = 'let
  case !throwerRecorded of
    (IOResult.Throw e, record) ->
      case (handle exceptionToEither in (handle replayIO record in !thrower)) of
        Either.Right (IOResult.Throw (Error.Error _ text)) -> printLine text