Re: [Haskell-cafe] Instances for continuation-based FRP
Conal Elliott co...@conal.net wrote: I first tried an imperative push-based FRP in 1998, and I had exactly the same experience as Heinrich mentions. The toughest two aspects of imperative implementation were sharing and event merge/union/mappend. This is exactly why I chose not to follow the imperative path from the very beginning and followed Yampa's example instead. Currently the denotational semantics of Netwire are only in my head, but the following is planned for the future: * Take inspiration from 'pipes' and find a way to add push/pull without giving up ArrowLoop. This has the highest priority, but it's also the hardest part. * Write down the denotational semantics as a specification. Optionally try to prove them in a theorem prover. * Engage more with you guys. We all have brilliant ideas and more communication could help us bringing FRP to the masses. I also plan to expose an opaque subset of Netwire which strictly enforces the traditional notion of FRP, e.g. continuous time. Netwire itself is really a stream processing abstraction and doesn't force you program in a reactive style. This is both a strength and a weakness. There is too much potential for abuse in this general setting. Greets, Ertugrul -- Not to be or to be and (not to be or to be and (not to be or to be and (not to be or to be and ... that is the list monad. signature.asc Description: PGP signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Instances for continuation-based FRP
Hi Conal, Thank you for replying. My aim is to find the simplest possible implementation of the semantics you describe in Push-pull FRP, so the denotational semantics are already in place. I guess what I am looking for is a simple translation of a denotational program into an imperative one. My intuition tells me that such a translation is possible, maybe even trivial, but I am not sure how to reason about correctness. While I like the idea of TCMs very much, they do not seem to be applicable for things that lack a denotation, such as IO. Maybe it is a question of how to relate denotational semantics to operational ones? Hans On 24 apr 2013, at 02:18, Conal Elliott wrote: Hi Hans, Do you have a denotation for your representation (a specification for your implementation)? If so, it will likely guide you to exactly the right type class instances, via the principle of type class morphisms (TCMs). If you don't have a denotation, I wonder how you could decide what correctness means for any aspect of your implementation. Good luck, and let me know if you want some help exploring the TCM process, -- Conal On Tue, Apr 23, 2013 at 6:22 AM, Hans Höglund h...@hanshoglund.se wrote: Hi everyone, I am experimenting with various implementation styles for classical FRP. My current thoughts are on a continuation-style push implementation, which can be summarized as follows. newtype EventT m r a= E { runE :: (a - m r) - m r - m r } newtype ReactiveT m r a = R { runR :: (m a - m r) - m r } type Event= EventT IO () type Reactive = ReactiveT IO () The idea is that events allow subscription of handlers, which are automatically unsubscribed after the continuation has finished, while reactives allow observation of a shared state until the continuation has finished. I managed to write the following Applicative instance instance Applicative (ReactiveT m r) where pure a = R $ \k - k (pure a) R f * R a = R $ \k - f (\f' - a (\a' - k $ f' * a')) But I am stuck on finding a suitable Monad instance. I notice the similarity between my types and the ContT monad and have a feeling this similarity could be used to clean up my instance code, but am not sure how to proceed. Does anyone have an idea, or a pointer to suitable literature. Best regards, Hans ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Instances for continuation-based FRP
Hi Hans. I'm delighted to hear that you have a precise denotation to define correctness of your implementation. So much of what gets called FRP these days abandons any denotational foundation, as well as continuous time, which have always been the two key properties of FRPhttp://stackoverflow.com/a/5878525/127335for me. I like your goal of finding a provably correct (perhaps correct by construction/derivation) implementation of the simple denotational semantics. I'm happy to give feedback and pointers if you continue with this goal. While I like the idea of TCMs very much, they do not seem to be applicable for things that lack a denotation, such as IO I suppose so, although I'd say it the other way around: things that lack denotation are not applicable for fulfilling denotational principles. Which suggests to me that IO will not get you to your goal. Instead, I recommend instead looking for a subset of imperative computation that suffices to implement the denotation you want, but is well-defined denotationally and tractable for reasoning. IO (general imperative computation) is neither, which is why we have denotative/functional programming in the first place. Regards, - Conal On Wed, Apr 24, 2013 at 8:31 AM, Hans Höglund h...@hanshoglund.se wrote: Hi Conal, Thank you for replying. My aim is to find the simplest possible implementation of the semantics you describe in Push-pull FRP http://conal.net/papers/push-pull-frp/, so the denotational semantics are already in place. I guess what I am looking for is a simple translation of a denotational program into an imperative one. My intuition tells me that such a translation is possible, maybe even trivial, but I am not sure how to reason about correctness. While I like the idea of TCMs very much, they do not seem to be applicable for things that lack a denotation, such as IO. Maybe it is a question of how to relate denotational semantics to operational ones? Hans On 24 apr 2013, at 02:18, Conal Elliott wrote: Hi Hans, Do you have a denotation for your representation (a specification for your implementation)? If so, it will likely guide you to exactly the right type class instances, via the principle of type class morphismshttp://conal.net/papers/type-class-morphisms/(TCMs). If you don't have a denotation, I wonder how you could decide what correctness means for any aspect of your implementation. Good luck, and let me know if you want some help exploring the TCM process, -- Conal On Tue, Apr 23, 2013 at 6:22 AM, Hans Höglund h...@hanshoglund.se wrote: Hi everyone, I am experimenting with various implementation styles for classical FRP. My current thoughts are on a continuation-style push implementation, which can be summarized as follows. newtype EventT m r a= E { runE :: (a - m r) - m r - m r } newtype ReactiveT m r a = R { runR :: (m a - m r) - m r } type Event= EventT IO () type Reactive = ReactiveT IO () The idea is that events allow subscription of handlers, which are automatically unsubscribed after the continuation has finished, while reactives allow observation of a shared state until the continuation has finished. I managed to write the following Applicative instance instance Applicative (ReactiveT m r) where pure a = R $ \k - k (pure a) R f * R a = R $ \k - f (\f' - a (\a' - k $ f' * a')) But I am stuck on finding a suitable Monad instance. I notice the similarity between my types and the ContT monad and have a feeling this similarity could be used to clean up my instance code, but am not sure how to proceed. Does anyone have an idea, or a pointer to suitable literature. Best regards, Hans ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Instances for continuation-based FRP
If you are not looking for the full reactive formalism but to treat event driven applications in a procedural ,sequential, imperative way (whatever you may call it) by means o continuations, then this is a good paper in the context of web applications: inverting back the inversion of control http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.3112 2013/4/24 Conal Elliott co...@conal.net Hi Hans. I'm delighted to hear that you have a precise denotation to define correctness of your implementation. So much of what gets called FRP these days abandons any denotational foundation, as well as continuous time, which have always been the two key properties of FRPhttp://stackoverflow.com/a/5878525/127335for me. I like your goal of finding a provably correct (perhaps correct by construction/derivation) implementation of the simple denotational semantics. I'm happy to give feedback and pointers if you continue with this goal. While I like the idea of TCMs very much, they do not seem to be applicable for things that lack a denotation, such as IO I suppose so, although I'd say it the other way around: things that lack denotation are not applicable for fulfilling denotational principles. Which suggests to me that IO will not get you to your goal. Instead, I recommend instead looking for a subset of imperative computation that suffices to implement the denotation you want, but is well-defined denotationally and tractable for reasoning. IO (general imperative computation) is neither, which is why we have denotative/functional programming in the first place. Regards, - Conal On Wed, Apr 24, 2013 at 8:31 AM, Hans Höglund h...@hanshoglund.se wrote: Hi Conal, Thank you for replying. My aim is to find the simplest possible implementation of the semantics you describe in Push-pull FRP http://conal.net/papers/push-pull-frp/, so the denotational semantics are already in place. I guess what I am looking for is a simple translation of a denotational program into an imperative one. My intuition tells me that such a translation is possible, maybe even trivial, but I am not sure how to reason about correctness. While I like the idea of TCMs very much, they do not seem to be applicable for things that lack a denotation, such as IO. Maybe it is a question of how to relate denotational semantics to operational ones? Hans On 24 apr 2013, at 02:18, Conal Elliott wrote: Hi Hans, Do you have a denotation for your representation (a specification for your implementation)? If so, it will likely guide you to exactly the right type class instances, via the principle of type class morphismshttp://conal.net/papers/type-class-morphisms/(TCMs). If you don't have a denotation, I wonder how you could decide what correctness means for any aspect of your implementation. Good luck, and let me know if you want some help exploring the TCM process, -- Conal On Tue, Apr 23, 2013 at 6:22 AM, Hans Höglund h...@hanshoglund.sewrote: Hi everyone, I am experimenting with various implementation styles for classical FRP. My current thoughts are on a continuation-style push implementation, which can be summarized as follows. newtype EventT m r a= E { runE :: (a - m r) - m r - m r } newtype ReactiveT m r a = R { runR :: (m a - m r) - m r } type Event= EventT IO () type Reactive = ReactiveT IO () The idea is that events allow subscription of handlers, which are automatically unsubscribed after the continuation has finished, while reactives allow observation of a shared state until the continuation has finished. I managed to write the following Applicative instance instance Applicative (ReactiveT m r) where pure a = R $ \k - k (pure a) R f * R a = R $ \k - f (\f' - a (\a' - k $ f' * a')) But I am stuck on finding a suitable Monad instance. I notice the similarity between my types and the ContT monad and have a feeling this similarity could be used to clean up my instance code, but am not sure how to proceed. Does anyone have an idea, or a pointer to suitable literature. Best regards, Hans ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Alberto. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Instances for continuation-based FRP
Hi Jared, Oh -- does Elm have a denotational semantics? I haven't heard of one. I just now skimmed the informal description of the Signal typehttp://elm-lang.org/docs/Signal/Signal.elm, and from the reference to updates in the description of merge, it sound like whatever semantics it might have, it couldn't be function-of-time. I'm intrigued with your interpretation. I wonder what it could mean for an event to be a derivative, especially partial one, and for arbitrary types. -- Conal On Wed, Apr 24, 2013 at 1:48 PM, earl obscure theanswertoprobl...@gmail.com wrote: Hi Conal, Caveat pre-emptor I'm new to haskell, frp, etc .. anyway how I was interpreting Elm's Eventbased strict FRP, was that each event was the partial derivative of the continuous time variable, and then since it was being strict, it would evaluate the tangent line or state of the system at that point, only update when necessary. Now related to Continuations, this is something I've been thinking about as well,but haven't gotten very far; apparently cont monad, and comonad are closely related. I was hoping to use the comonad rules, extend/duplicate to encode different continuations paths, and then extract when, a continuation path is chosen. Was hoping maybe the analog would be PDE's, or something more general than my interpretation of Elm's FRP. These are just random thoughts that I wanted to get out. Thanks. Jared Nicholson. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Instances for continuation-based FRP
The intuition intrigues me. If, upon inspection, it survives morphs into something else, I'd like to hear about it. Good luck! -- Conal The object of mathematical rigor is to sanction and legitimize the conquests of intuition, and there was never any other object for it. - Jacques Hadamard I call intuition cosmic fishing. You feel a nibble, then you've got to hook the fish. -- Buckminster Fullero On Wed, Apr 24, 2013 at 7:26 PM, earl obscure theanswertoprobl...@gmail.com wrote: His description of the different frp approaches starts at section 2.1 of the thesis. http://www.testblogpleaseignore.com/wp-content/uploads/2012/04/thesis.pdfThen in 3.1 describes implementation of discrete signals. I don't think he gives a denotational semantics. I was thinking, the event, is the derivative of the specific continuous signal it corresponds to, all other continuous signals of the system held equal. Applying the partial derivative, is like sampling, or discrete time stepping. But it is samplying the entire state, or multivariate structure not just the specific symbol. This made more sense unarticulated. I'll need to think a bit. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Instances for continuation-based FRP
Hi everyone, I am experimenting with various implementation styles for classical FRP. My current thoughts are on a continuation-style push implementation, which can be summarized as follows. newtype EventT m r a= E { runE :: (a - m r) - m r - m r } newtype ReactiveT m r a = R { runR :: (m a - m r) - m r } type Event= EventT IO () type Reactive = ReactiveT IO () The idea is that events allow subscription of handlers, which are automatically unsubscribed after the continuation has finished, while reactives allow observation of a shared state until the continuation has finished. I managed to write the following Applicative instance instance Applicative (ReactiveT m r) where pure a = R $ \k - k (pure a) R f * R a = R $ \k - f (\f' - a (\a' - k $ f' * a')) But I am stuck on finding a suitable Monad instance. I notice the similarity between my types and the ContT monad and have a feeling this similarity could be used to clean up my instance code, but am not sure how to proceed. Does anyone have an idea, or a pointer to suitable literature. Best regards, Hans___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Instances for continuation-based FRP
Hi Hans, Do you have a denotation for your representation (a specification for your implementation)? If so, it will likely guide you to exactly the right type class instances, via the principle of type class morphismshttp://conal.net/papers/type-class-morphisms/(TCMs). If you don't have a denotation, I wonder how you could decide what correctness means for any aspect of your implementation. Good luck, and let me know if you want some help exploring the TCM process, -- Conal On Tue, Apr 23, 2013 at 6:22 AM, Hans Höglund h...@hanshoglund.se wrote: Hi everyone, I am experimenting with various implementation styles for classical FRP. My current thoughts are on a continuation-style push implementation, which can be summarized as follows. newtype EventT m r a= E { runE :: (a - m r) - m r - m r } newtype ReactiveT m r a = R { runR :: (m a - m r) - m r } type Event= EventT IO () type Reactive = ReactiveT IO () The idea is that events allow subscription of handlers, which are automatically unsubscribed after the continuation has finished, while reactives allow observation of a shared state until the continuation has finished. I managed to write the following Applicative instance instance Applicative (ReactiveT m r) where pure a = R $ \k - k (pure a) R f * R a = R $ \k - f (\f' - a (\a' - k $ f' * a')) But I am stuck on finding a suitable Monad instance. I notice the similarity between my types and the ContT monad and have a feeling this similarity could be used to clean up my instance code, but am not sure how to proceed. Does anyone have an idea, or a pointer to suitable literature. Best regards, Hans ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe