Created
August 31, 2019 22:50
-
-
Save atacratic/15f37109cb536655d8bc536ddd25477e to your computer and use it in GitHub Desktop.
Prototype IO proxy handler for record/replay in Unison
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment