Closed pyrtsa closed 9 years ago
I've defined the semantics in the denotational semantics document at https://github.com/SodiumFRP/sodium/tree/master/denotational so it is actually documented, but I didn't realize that the implementation doesn't actually comply with that definition. The output of your example with the current semantics would be [a, b, c] because both defers will put the value into the same transaction. This is actually problematic. You really want the new transactions to be unique so things don't get dumped into the same transaction - which is not useful if defer()
/split()
are used more than once in the program. One possibility is to use a Supply to construct a hierarchy of child transaction rankings that determine their relative order.
The next thing I'm going to do when I finish the book is a comprehensive test case generator that will compare every implementation against the denotational semantics.
First use case: Let's say you have an incoming data packet with a number of frames in it, and you want to parse it into frames and process each frame in its own transaction. split() allows you to do that without going outside the FRP paradigm.
Second use case: It can be useful to model I/O as (in Haskell syntax) Stream a -> IO (Stream b)
. The assumption is usually that the output value is in new transaction. To implement a null IO operation - equivalent to \a -> pure b
where b
is some constant, you can use defer().
I'd like to keep defer()
and split()
if possible because they're useful. The Supply-like method looks to me to be the only technically correct solution.
So here's how it would look:
-- This is the rank of the current transaction
rank0 :: Rank
-- Give two child transaction ranks, the returned order corresponding to the
-- temporal order and all before any successor of the input.
splitRank2 :: Rank -> (Rank, Rank)
-- give an infinite list of children, and a second child, the returned order
-- corresponding to the temporal order and all before any successor of the input.
splitsRank :: Rank -> ([Rank], Rank)
defer :: Rank -> Stream a -> Stream a
split :: [Rank] -> Stream [a] -> Stream a
Thoughts?
I've decided that the best solution is this:
Whoever disagrees please comment.
I've implemented everything I described above. Will close.
What's the purpose
defer
ring andsplit
ting aStream
?What are the semantics of those operations?
It all reeks to me as a broken abstraction since every
defer
redStream
creates its own transaction in some (undocumented) order:That code prints
[A, a, B, b, C, c]
, which implies that deferred transactions see inconsistent intermediate states when deferred snapshotting and updating ofCell
s is involved.Why not
[Aa, Bb, Cc]
, i.e. make every singly deferredStream
firing happen in the same deferred transaction? Or indeed, why havedefer
in the first place? Does it have a use case?