[Haskell-cafe] Instances for continuation-based FRP

[Conal Elliott]

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<http://stackoverflow.com/a/5878525/127335>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 <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 morphisms<http://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 <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
>>
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130424/91b3c3b1/attachment.htm>