Hans Höglund | 23 Apr 15:22 2013
Picon

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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Conal Elliott | 24 Apr 02:18 2013
Picon

Re: 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 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 <hans <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Hans Höglund | 24 Apr 17:31 2013
Picon

Re: 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 <hans <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Conal Elliott | 24 Apr 20:51 2013
Picon

Re: 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 FRP for 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 <hans <at> 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, 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 <hans <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe




_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Alberto G. Corona | 24 Apr 21:09 2013
Picon

Re: 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
 


2013/4/24 Conal Elliott <conal <at> 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 FRP for 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 <hans <at> 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, 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 <hans <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe





_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe




--
Alberto.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Heinrich Apfelmus | 25 Apr 14:16 2013
Picon

Re: Instances for continuation-based FRP

Hans Höglund wrote:
> 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.

In reactive-banana, the Reactive.Banana.Model module implements /
defines the denotational semantics.

   http://tinyurl.com/Reactive-Banana-Model

It's very similar to Conal's semantics from the Push-Pull article.

> 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.

In my experience, the main problem with imperative implementations is
that they have a hard time with the  union  combinator and with
preserving sharing. Reactive-banana is the best I could come up with.

Best regards,
Heinrich Apfelmus

--
http://apfelmus.nfshost.com

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Conal Elliott | 26 Apr 00:40 2013
Picon

Re: Instances for continuation-based FRP

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.

-- Conal


On Thu, Apr 25, 2013 at 5:16 AM, Heinrich Apfelmus <apfelmus <at> quantentunnel.de> wrote:
Hans Höglund wrote:
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.

In reactive-banana, the Reactive.Banana.Model module implements /
defines the denotational semantics.

  http://tinyurl.com/Reactive-Banana-Model

It's very similar to Conal's semantics from the Push-Pull article.


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.

In my experience, the main problem with imperative implementations is
that they have a hard time with the  union  combinator and with
preserving sharing. Reactive-banana is the best I could come up with.


Best regards,
Heinrich Apfelmus

--
http://apfelmus.nfshost.com




_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Ertugrul Söylemez | 26 Apr 02:11 2013
Picon

Re: Instances for continuation-based FRP

Conal Elliott <conal <at> 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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane