[Caml-list] [ANN] PEC ver. 1.1

[Caml-list] [ANN] PEC ver. 1.1

[Satoshi Ogasawara]

Hello lists,

I'm please to announce release PEC version 1.1, a push-based event combinator library
which is helpful to write event driven systems with purely functional style.

 https://github.com/osiire/Pec

PEC is similar to React library but there are some different points.

- PEC's update cycle is separated from sending events.
  You can send a value to event during update cycle.

- PEC doesn't hold any pointer(including weak one) to event until the
  event will be subscribed.

- All PEC's signal are switchable. 'switch' means you can replace dependency
  of a signal keeping signals depends on the signal unchanged.

You can see sample codes to use PEC.

https://github.com/osiire/Pec/blob/master/test/

Regards,
 ogasawara

Re: [Caml-list] [ANN] PEC ver. 1.1

[Adrien]

Hi,

I haven't been able to take more than a close look at PEC but I'm
interested in it (in particular for the ability to send values to
events during the update cycle).

I've noticed EventSig.scan: val scan : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a t
Is this function like a fold? Is there a particular reason for naming
it "scan" (rather than "fold")?

Thanks.

-- 
Adrien Nader

Re: [Caml-list] [ANN] PEC ver. 1.1

[Satoshi Ogasawara]

(2012/04/18 2:52), Adrien wrote:
> I haven't been able to take more than a close look at PEC but I'm
> interested in it (in particular for the ability to send values to
> events during the update cycle).

Thank you for your interest in my library.

> I've noticed EventSig.scan: val scan : ('a ->  'b ->  'a) ->  'a ->  'b t ->  'a t
> Is this function like a fold? Is there a particular reason for naming
> it "scan" (rather than "fold")?

Because I thought Haskell's scanl is more similar to EventSig.scan than foldl.

scanl : (a -> b -> a) -> a -> [b] -> [a]
foldl : (a -> b -> a) -> a -> [b] -> a

BTW, I have just noticed Event.scan has a bug. The result of scan function should
  contain initial value specified second argument, but Event.scan doesn't.
That has been fixed.


Regards,
   Ogasawara

Re: [Caml-list] [ANN] PEC ver. 1.1

[Daniel Bünzli]

Hello, 

> PEC is similar to React library but there are some different points.
> 
> - PEC's update cycle is separated from sending events.
> You can send a value to event during update cycle.


What's the semantics if you send two different values to an event during an update cycle ? 
 
> - PEC doesn't hold any pointer(including weak one) to event until the
> event will be subscribed.


I'm not sure how that's different from react. If an event has no dependents (by which I understand your "subscribed"), react doesn't hold any pointer either. 
 
> - All PEC's signal are switchable. 'switch' means you can replace dependency
> of a signal keeping signals depends on the signal unchanged.


How is that different from react's E.switch/S.switch ? 

Best,

Daniel

Re: [Caml-list] [ANN] PEC ver. 1.1

[Satoshi Ogasawara]

Hello,

(2012/04/18 4:23), Daniel Bünzli wrote:
>> - PEC's update cycle is separated from sending events.
>> You can send a value to event during update cycle.
> What's the semantics if you send two different values to an event during an update cycle ?

They fires two different event if you send two different value to an event
even if same update cycle. Events send are stored in an event queue,
and they will be poped by 'run' function just like GUI event loop.

>> - PEC doesn't hold any pointer(including weak one) to event until the
>> event will be subscribed.
> I'm not sure how that's different from react. If an event has no dependents (by which I understand your "subscribed"), react doesn't hold any pointer either.

React constructs 'heap' to hold dependency graph inside the library.
let e' = map (fun x -> x + 1) e, the e' and e are weakly pointed by the heap.
PEC doesn't have heap structure in the library. This is a difference.

This difference is important if you want to translate the OCaml event
combinator to javascript because javascript doesn't have weak pointer.

>> - All PEC's signal are switchable. 'switch' means you can replace dependency
>> of a signal keeping signals depends on the signal unchanged.
> How is that different from react's E.switch/S.switch ?

Almost same except all signals are created though react's S.switch at initializing.

It's convenient to design library for dynamic event driven systems. For example,
let me assume a signal of window size property.

type window = {
    size : (int * int) signal;
}

If you want to change the dependency of window.size after initialize the window
keeping signals depends on the size unchanged, there is no way except making switch
event at initializing.

type window = {
    size : (int * int) signal;
    size_switch_event : (int * int) event event;
}

I feel it's not convenient. So I decided to embedded the swith_event to inside of signals.

Regards,
   Ogasawara

Re: [Caml-list] [ANN] PEC ver. 1.1

[Daniel Bünzli]

Le mercredi, 18 avril 2012 à 03:59, Satoshi Ogasawara a écrit :
> > What's the semantics if you send two different values to an event during an update cycle ?
>  
> They fires two different event if you send two different value to an event
> even if same update cycle. Events send are stored in an event queue,
> and they will be poped by 'run' function just like GUI event loop.


Ok. I would just like to point out that you can do exactly the same with React. However React doesn't integrate that functionality, the client has to implement it. Mainly for two reasons.  

1) Thread-safety and compositionality. React has no global data structure.

2) Semantic issues. As soon as primitive events are triggered by other primitive events you run into the problem of multiple occurences of the same event during an update cycle. Now given the synchrony hypothesis of update cycles (an update cycle is instantaneous), this is a violation of the semantics of events (an event has at most one occurence at any given time t). And then people ask you if you can somehow manage the order of updates in an update cycle and then you are not doing FRP anymore, you are doing RP. By loosing the F you also loose compositionality and the equational reasoning tools provided by the denotational semantics of events.   

> > I'm not sure how that's different from react. If an event has no dependents (by which I understand your "subscribed"), react doesn't hold any pointer either.
>  
> React constructs 'heap' to hold dependency graph inside the library.
> let e' = map (fun x -> x + 1) e, the e' and e are weakly pointed by the heap.
> PEC doesn't have heap structure in the library. This is a difference.
>  
> This difference is important if you want to translate the OCaml event
> combinator to javascript because javascript doesn't have weak pointer.


To be precise React constructs a heap only during an update cycle. Now I guess you must have some kind of similar data structure encoded since if you don't update your events in topological order of the dependency graph, you'll have glitches and again violate the semantics of events.

Regarding the absence of Weak usage I'm curious in how you manage the garbage collections of events that depend on others.  
  
> > How is that different from react's E.switch/S.switch ?
>  
> Almost same except all signals are created though react's S.switch at initializing.
>  
> It's convenient to design library for dynamic event driven systems. For example,
> let me assume a signal of window size property.
>  
> type window = {
> size : (int * int) signal;
> }
>  
> If you want to change the dependency of window.size after initialize the window
> keeping signals depends on the size unchanged, there is no way except making switch
> event at initializing.
>  
> type window = {
> size : (int * int) signal;
> size_switch_event : (int * int) event event;
> }
>  
> I feel it's not convenient. So I decided to embedded the swith_event to inside of signals.

Best,

Daniel

Re: [Caml-list] [ANN] PEC ver. 1.1

[Satoshi Ogasawara]

Hello,

Thank you very much for your prompt reply.

(2012/04/18 16:36), Daniel Bünzli wrote:
> 1) Thread-safety and compositionality. React has no global data structure.

I'm sorry about my misunderstanding that React has a global structure.

> 2) Semantic issues. As soon as primitive events are triggered by other primitive events you run into the problem of multiple occurences of the same event during an update cycle. Now given the synchrony hypothesis of update cycles (an update cycle is instantaneous), this is a violation of the semantics of events (an event has at most one occurence at any given time t). And then people ask you if you can somehow manage the order of updates in an update cycle and then you are not doing FRP anymore, you are doing RP. By loosing the F you also loose compositionality and the equational reasoning tools provided by the denotational semantics of events.

I see that React is implemented with intend to keep good semantics and able to
realize same functions as PEC.
But PEC dose not violate good semantics either. PEC treats only one event at any
given time t. Please see blow code.

module E = Pec.Event.Make (Pec.EventQueue.DefaultQueueM) (Pec.EventQueue.DefaultQueueI)
open Printf

let _ =
   let e, sender = E.make () in
   let e' = E.map (fun x -> sender 2; x + 1) e in   (* during update cycle, send 2. *)
   let _ = E.subscribe (printf "e=%d\n") e in
   let _ = E.subscribe (printf "e'=%d\n") e' in
   sender 1;
   ignore (E.run ());   (* run one event *)
   printf "---\n";
   ignore (E.run ());   (* run one event *)
   printf "end\n"

This program outputs:

e=1
e'=2
---
e=2
e'=3
end

The function (fun x -> sender 2; x + 1) is not purely functional. I see that violates
a part of good semantics and composability. But there is no problem of multiple
occurrences of the same event in one update cycle.

To write event driven systems such like GUI sometimes needs a event-event chain
without real-user actions. Sending events during update cycle is something unavoidable.

> Regarding the absence of Weak usage I'm curious in how you manage the garbage collections of events that depend on others.

Yes, weak-pointer-less implementation is one of my purpose. The key point is
that dependency of events are represented by nested variants.

Best Regards,
   Ogasawara

Re: [Caml-list] [ANN] PEC ver. 1.1

[Daniel Bünzli]

Le mercredi, 18 avril 2012 à 13:44, Satoshi Ogasawara a écrit :
> But PEC dose not violate good semantics either. PEC treats only one event at any
> given time t. Please see blow code.


I don't think your code shows the problem I'm talking about.
  
> module E = Pec.Event.Make (Pec.EventQueue.DefaultQueueM) (Pec.EventQueue.DefaultQueueI)
> open Printf
>  
> let _ =
> let e, sender = E.make () in
> let e' = E.map (fun x -> sender 2; x + 1) e in (* during update cycle, send 2. *)


Here add :

let e'' = E.map (fun x -> sender 3; x + 1) e in  
  
and now what should the value of e be in the next update cycle ? All the options you have (keep only the first call to sender, keep only the last call to sender, keep both and execute one after the other) break the functional and compositional nature of FRP because it violates the semantics of events.

> To write event driven systems such like GUI sometimes needs a event-event chain
> without real-user actions. Sending events during update cycle is something unavoidable.


I don't have enough experience to assert that's really the case. However if that's needed I suspect that the way to resolve conflicts that break the semantics, should they arise, is actually very specific to the problem domain and shouldn't rely on anything related to the order of updates during the update cycle.  

The only thing I'm saying here is that your first message made it sound like PEC solved a problem of React ("You can send a value to event during update cycle."). It's not a problem of React it's a problem of interfacing FRP with your application domain. And React can perfectly be adapted to use the same unsound solution that PEC seems to use by adding the sender calls in a thunk queue and dequeing after the end of the update cycle.  
  
> Yes, weak-pointer-less implementation is one of my purpose. The key point is
> that dependency of events are represented by nested variants.


That doesn't really answer my question (or at least I don't understand what it means).

Best,

Daniel

Re: [Caml-list] [ANN] PEC ver. 1.1

[Satoshi Ogasawara]

First of all, I apologize about my first message. Now I understand React can be
easily adapted to send a value during update cycle by using thunk. To forbid
sending events during update cycle in React is not restriction but design choice.

(2012/04/18 22:27), Daniel Bünzli wrote:
 > and now what should the value of e be in the next update cycle ? All the options you 
have (keep only the first call to sender, keep only the last call to sender, keep both and 
execute one after the other) break the functional and compositional nature of FRP because 
it violates the semantics of events.

PEC takes the third option. I understand that the evaluation order of update
are problematic.

module E = Pec.Event.Make (Pec.EventQueue.DefaultQueueM) (Pec.EventQueue.DefaultQueueI)
open Printf

let _ =
   let e, sender = E.make () in
   let e' = E.map (fun x -> sender 2; x + 1) e in
   let e'' = E.map (fun x -> sender 3; x + 1) e in
   let _ = E.subscribe (printf "e=%d\n") e in
   let _ = E.subscribe (printf "e'=%d\n") e' in
   let _ = E.subscribe (printf "e''=%d\n") e'' in
   sender 1;
   ignore (E.run ());
   printf "---\n";
   ignore (E.run ());
   printf "---\n";
   ignore (E.run ());
   printf "end\n"

This program outputs:

e=1
e'=2
e''=2
---
e=2
e'=3
e''=3
---
e=3
e'=4
e''=4
end

This result rely on order of applying subscribe function. I think any program
depending on the evaluation order of updates are not good one.

But I'm not sure why only sending a value to event breaks functional and compos-
itional nature of FRP. I think all side-effects during update cycle are breaks
functional and compositional nature of FRP too, because the results of both programs
are depends on evaluation order of updates.

A:
let e' = E.map (fun x -> sender 1; x + 1) e in
let e'' = E.map (fun x -> sender 2; x + 1) e in

B:
let e' = E.map (fun x -> print_int 1; x + 1) e in
let e'' = E.map (fun x -> print_int 2; x + 1) e in

Are there any special problem in program A? In other word, program B keeps
functional and compositional nature of FRP?

>> Yes, weak-pointer-less implementation is one of my purpose. The key point is
>> that dependency of events are represented by nested variants.
>
> That doesn't really answer my question (or at least I don't understand what it means).

Inside PEC, "let e' = E.map f e" is just variant instance.

   let map f e = Wrap {
     event = e;
     wrap = f;
     w_latest = None;
   }

Another primitive combinator functions also just makes a variant instance.

   and 'a event =
     | Cell : 'a mcell -> 'a event
     | Wrap : ('a, 'b) mwrap -> 'b event
     | Choose : 'a choose -> 'a event
     | Never : 'a event
     | Switch : 'a mswitch -> 'a event

So an event value itself is a nested variant instance which can be GCed freely
when user-level references are disappear. (There are no library level reference.)

When an event is subscribed, the argument function are set in source events of
subscribed event. This means subscribed events are never GCed until source events
are GCed.(or until unsubscribe.)

If one of source events are fired, dependent events marked with subscribe functions
are updated. Weak pointer does not needs in that algorithm.


Best Regards,
  Ogasawara

Re: [Caml-list] [ANN] PEC ver. 1.1

[Daniel Bünzli]

Le mercredi, 18 avril 2012 à 19:39, Satoshi Ogasawara a écrit :
> Now I understand React can be
> easily adapted to send a value during update cycle by using thunk. To forbid
> sending events during update cycle in React is not restriction but design choice.


Just to be precise. It *is* forbidden to use the sending function of a primitive event during an update cycle. It is of course not forbidden to store this call in a queue as a thunk and execute it later, after the update cycle ended, like PEC does.  
  
> But I'm not sure why only sending a value to event breaks functional and compos-
> itional nature of FRP. I think all side-effects during update cycle are breaks
> functional and compositional nature of FRP too, because the results of both programs
> are depends on evaluation order of updates.
>  
> A:
> let e' = E.map (fun x -> sender 1; x + 1) e in
> let e'' = E.map (fun x -> sender 2; x + 1) e in
>  
> B:
> let e' = E.map (fun x -> print_int 1; x + 1) e in
> let e'' = E.map (fun x -> print_int 2; x + 1) e in
>  
> Are there any special problem in program A?  

Yes because the semantics of [e] is violated, it has three values at the same time, the current value during the update cycle, the value 1 and the value 2. Now suppose I reason about the semantics of [e] in this program, it has a well-defined outcome *for [e] itself* if I send it a value [v]. However if you now add a new module that uses [e] and does :  

let e''' = E.map (fun x -> sender 3; x + 1) e  

then the semantics of [e] changes, sending the same [v] to [e] results in a different outcome *for [e] itself* and hence for all its dependents. That's what I mean when I say that you lost the functional and compositional nature of FRP. You are back into imperative programming. Note that this is also valid if the [sender] function sends to another primitive event e'.  
  
> In other word, program B keeps
> functional and compositional nature of FRP?


Yes because since you didn't play dirty tricks with [e], if you add a new module that uses [e] and does :  

let e''' = E.map (fun x -> print_int 3; x + 1) e

the semantics of [e] is still the same, sending the same value to [e] has the same outcome *for [e] itself* whether e''' is present or not. Of course this is not the case for stdout and its final state will depend on the evaluation order of the FRP system. But we never pretended that stdout was an event or a signal, stdout lives outside the FRP system.  
  
> So an event value itself is a nested variant instance which can be GCed freely
> when user-level references are disappear. (There are no library level reference.)
>  
> When an event is subscribed, the argument function are set in source events of
> subscribed event. This means subscribed events are never GCed until source events
> are GCed.(or until unsubscribe.)

> If one of source events are fired, dependent events marked with subscribe functions
> are updated. Weak pointer does not needs in that algorithm.




So if I understand correctly you are doing manual memory management via (un)subscribe of the leaves of the dependency tree and instead of having weak "forward" pointers from events to their dependents you have regular "backward" pointers from events to the events they depend on. Once these leaves are subscribed we can follow them backwards to find out what their primitive event set is and understand what needs to be updated along the way. It may be an interesting approach to avoid weak pointers but I'd need more thinking to convince me it can correctly handles all the dark sides of leaks, fixed point definitions, signal initialization and dynamically changing dependency graph. By the way you still need to update the events in the correct order/and or only once to prevent glitches, how do you achieve that ?

Best,

Daniel

Re: [Caml-list] [ANN] PEC ver. 1.1

[Satoshi Ogasawara]

(2012/04/19 7:32), Daniel Bünzli wrote:
> Yes because the semantics of [e] is violated, it has three values at the same time, the current value during the update cycle, the value 1 and the value 2. Now suppose I reason about the semantics of [e] in this program, it has a well-defined outcome *for [e] itself* if I send it a value [v]. However if you now add a new module that uses [e] and does :

Thank you for helping me understand with your explanation.

If I understand correctly sending [v] to [e] immediately during update cycle
are violate the semantics because it cause more than one values on one event at
the same time.

Using React,

let e, sender = E.create () in
let e' = E.map (fun x -> Queue.add q (fun () -> sender 1); x + 1) e in
let e'' = E.map (fun x -> Queue.add q (fun () -> sender 2); x + 1) e in

does this code violate the semantics of events? If so, PEC is also unsound.
I'd like to know PEC is unsound or not.

 > So if I understand correctly you are doing manual memory management via (un)subscribe 
of the leaves of the dependency tree and instead of having weak "forward" pointers from 
events to their dependents you have regular "backward" pointers from events to the events 
they depend on. Once these leaves are subscribed we can follow them backwards to find out 
what their primitive event set is and understand what needs to be updated along the way.

Yes, exactly.

 >It may be an interesting approach to avoid weak pointers but I'd need more thinking to 
convince me it can correctly handles all the dark sides of leaks, fixed point definitions, 
signal initialization and dynamically changing dependency graph. By the way you still need 
to update the events in the correct order/and or only once to prevent glitches, how do you 
achieve that ?

To prevent glitches, PEC distinct one update cycle to another by time identity.
And calculated results are cached for same update cycle.
Update order is straight forward. Just follow from leaf to primitive source event.
It's not problem because only one primitive value changes at one update cycle.

Best Regards,
   Ogasawara

Re: [Caml-list] [ANN] PEC ver. 1.1

[Daniel Bünzli]

Le jeudi, 19 avril 2012 à 10:59, Satoshi Ogasawara a écrit :
> If I understand correctly sending [v] to [e] immediately during update cycle
> are violate the semantics because it cause more than one values on one event at
> the same time.


Yes.  

> Using React,
>  
> let e, sender = E.create () in
> let e' = E.map (fun x -> Queue.add q (fun () -> sender 1); x + 1) e in
> let e'' = E.map (fun x -> Queue.add q (fun () -> sender 2); x + 1) e in
>  
> does this code violate the semantics of events?  

Yes. It has the same problem. Let's start with :

> let e, sender = E.create () in
> let e' = E.map (fun x -> Queue.add q (fun () -> sender 1); x + 1) e in




Since the thunk is delayed to be executed after the update cycle we *could* say that an occurence of [e] at time [t] defines the occurence of [e] at time [t + dt]. Note however that this is a bad idea, the right way to solve these problems is to use fixed point operators, see [1].

Now this is all fine, during the update cycle, which is made under a synchrony hypothesis (i.e. it takes no time, see [2]), we are defining the occurence of [e] at time [t + dt] as being 1. So far so good.  

But now we change the program and add

> let e, sender = E.create () in
> let e' = E.map (fun x -> Queue.add q (fun () -> sender 1); x + 1) e in
> let e'' = E.map (fun x -> Queue.add q (fun () -> sender 2); x + 1) e in

  


This is not fine at all, during the update cycle, which again, takes no time, i.e. everything therein happens simultaneously at time [t], we are defining the occurence of [e] at time [t + dt] as being 1 and 2 at the same time. A schizophrenic event which obviously violates the semantics of events since an event must have at most one occurence at any given time [t].

So basically when you allow feedback from primitive events to primitive events you have to be very careful. Maybe that's needed in practice, again, I don't have enough experience to assert that, but if you do it you should make sure that the semantics of events is not violated.  

> If so, PEC is also unsound.
> I'd like to know PEC is unsound or not.


PEC may not be unsound as a whole. However the idea that you can just send to primitive events during update cycles and not bother is unsound with respect to the semantics of events as soon as you send two different values to the same primitive event.  

> To prevent glitches, PEC distinct one update cycle to another by time identity.
> And calculated results are cached for same update cycle.
> Update order is straight forward. Just follow from leaf to primitive source event.
> It's not problem because only one primitive value changes at one update cycle.


Right. But you still have to maintain some kind of mapping between the primitive event and the leaves they may influence to know which ones to update when the corresponding primitive event occurs. Do you store that in the primitive event itself or do you use a global data structure ?

While I'm not very fond of the sub/unscribe part I think it's an interesting implementation and may try, once I get some time, to adapt it to React to see what we can get from it (I also think that the resulting implementation could be much simpler). One can in fact argue that using React you also have to do the same manual management by having to keep reference on leaf events to avoid them being gc'd. The difference is that PEC trusts the client to perform unsubscribes correctly to avoid leaks while React allows not to bother about that at all (but Weak pointers have their cost). Besides it may be the case that in practice sub/unsuscribe calls are not that plentyfull; I would count one subscribe and no unsubscribe in the breakout.ml example of React's distribution.  

Best,

Daniel

[1] http://erratique.ch/software/react/doc/React.E.html#VALfix
[2] http://erratique.ch/software/react/doc/React#simultaneity  

Re: [Caml-list] [ANN] PEC ver. 1.1

[Daniel Bünzli]

Le jeudi, 19 avril 2012 à 12:31, Daniel Bünzli a écrit :

> While I'm not very fond of the sub/unscribe part I think it's an interesting implementation and may try, once I get some time, to adapt it to React to see what we can get from it (I also think that the resulting implementation could be much simpler).  
In fact, if I really understood what you are doing, I think there is a performance problem with your approach. Suppose we have the following configuration where L is a subscribed "leaf" event, that depends on N events that eventually lead to the primitive events P1 ... PN :  

L
| \  ... \
° °      °
|  \  ...  \
°  °       °
|   \  ...  \
... ...    ...
|    \        \  
P1 P2 ... PN

If P1 occurs then you start walking back from L, but you don't know where P1 is so you have to walk down every branch until you find P1 and then walk back from there up to L to make the update.

Contrast this with (weak) forward pointers: you just start from P1 and walk *once* up to L.

Is that correct ?  

Best,

Daniel

Re: [Caml-list] [ANN] PEC ver. 1.1

[Satoshi Ogasawara]

(2012/04/19 19:57), Daniel Bünzli wrote:
> Le jeudi, 19 avril 2012 à 12:31, Daniel Bünzli a écrit :
> If P1 occurs then you start walking back from L, but you don't know where P1 is so you have to walk down every branch until you find P1 and then walk back from there up to L to make the update.
> Contrast this with (weak) forward pointers: you just start from P1 and walk *once* up to L.
> Is that correct ?

It's correct. But the performance can be optimized in future I think.

When subscribing a event, we can collect and store information about tree structure.
Present implementation discards these information.

Best Regards,
   Ogasawara

Re: [Caml-list] [ANN] PEC ver. 1.1

[Satoshi Ogasawara]

Thank you for helping me understand with your explanation.

Your event semantics has two invariant.

  1. for all e, t : occurrence of [e] at time [t] is one or zero.
  2. if primitive [e] is occurred in time [t], update cycle runs in time [t].

Do you have any experience to proof a theorem against event combination term
by using above axiom and event combinators semantics? I'm interested in this
kind of reasoning.

(2012/04/19 19:31), Daniel Bünzli wrote:
> Right. But you still have to maintain some kind of mapping between the primitive event and the leaves they may influence to know which ones to update when the corresponding primitive event occurs. Do you store that in the primitive event itself or do you use a global data structure ?

Primitive events has list of leaves.


Best Regards,
  Ogasawara

Re: [Caml-list] [ANN] PEC ver. 1.1

[Daniel Bünzli]

Le jeudi, 19 avril 2012 à 15:02, Satoshi Ogasawara a écrit :
> Your event semantics has two invariant.
>  
> 1. for all e, t : occurrence of [e] at time [t] is one or zero.
> 2. if primitive [e] is occurred in time [t], update cycle runs in time [t].


Yes. You can read about the denotational semantics of React here:

http://erratique.ch/software/react/doc/React#sem

Besides all the combinators of React have a complete description of their denotational semantics. Note that in general for users of FRP I think it really doesn't help to think about update cycles, it seems to bring in more confusion. Users should care and think in terms of the semantics of events and signals. Update cycles are an implementation detail and should be understood only by programmers who need to interface the FRP system to a problem domain.  

> Do you have any experience to proof a theorem against event combination term
> by using above axiom and event combinators semantics? I'm interested in this
> kind of reasoning.


In this post I use the semantics and equational reasoning to understand why something doesn't happen.  

https://sympa-roc.inria.fr/wws/arc/caml-list/2009-12/msg00054.html

(you may have to read the whole thread to fully understand the example).  

> It's correct. But the performance can be optimized in future I think.
>  
> When subscribing a event, we can collect and store information about tree structure.
> Present implementation discards these information.




I didn't think hard about this but I suspect you'll hit problems with dynamic changes to the dependency graph (e.g. switching). And besides one should be careful not to make the creation of signals and events too expensive. I'm doubtful but I'm interested in hearing if you get any results in that direction.
  
Best,

Daniel

Re: [Caml-list] [ANN] PEC ver. 1.1

[Satoshi Ogasawara]

(2012/04/19 23:09), Daniel Bünzli wrote:
>> Do you have any experience to proof a theorem against event combination term
>> by using above axiom and event combinators semantics? I'm interested in this
>> kind of reasoning.
>
> In this post I use the semantics and equational reasoning to understand why something doesn't happen.
>
> https://sympa-roc.inria.fr/wws/arc/caml-list/2009-12/msg00054.html
>
> (you may have to read the whole thread to fully understand the example).

Thank you for your information. I like this kind of strict reasoning.
I'd like to add some semantics to PEC, too.

Any way, thank you for your educational discussion!

Best Regards,
  Ogasawara