<div dir="ltr"><div><div><div>Hi Hans.<br><br></div>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 <a href="http://stackoverflow.com/a/5878525/127335">the two key properties of FRP</a> for me.<br>
<br></div>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.<br>
<br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">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<br>
</blockquote><br></div>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.<br>
<div><div><br></div><div>Regards, - Conal<br></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Apr 24, 2013 at 8:31 AM, Hans Höglund <span dir="ltr"><<a href="mailto:hans@hanshoglund.se" target="_blank">hans@hanshoglund.se</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div>Hi Conal,</div><div><br></div><div>Thank you for replying.</div><div><br></div>
<div>
My aim is to find the simplest possible implementation of the semantics you describe in <a href="http://conal.net/papers/push-pull-frp/" target="_blank">Push-pull FRP</a>, 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. </div>
<div><br></div><div>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?</div>
<span class="HOEnZb"><font color="#888888"><div><br></div><div>Hans</div></font></span><div><div class="h5"><div><br></div><br><div><div>On 24 apr 2013, at 02:18, Conal Elliott wrote:</div><br><blockquote type="cite"><div dir="ltr">
<div><div>Hi Hans,<br><br></div>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 <a href="http://conal.net/papers/type-class-morphisms/" target="_blank">type class morphisms</a> (TCMs). If you don't have a denotation, I wonder how you could decide what correctness means for any aspect of your implementation.<br>
<br></div><div>Good luck, and let me know if you want some help exploring the TCM process,<br><br></div>-- Conal<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Apr 23, 2013 at 6:22 AM, Hans Höglund <span dir="ltr"><<a href="mailto:hans@hanshoglund.se" target="_blank">hans@hanshoglund.se</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">Hi everyone,<div><br></div><div>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.</div>
<div><br></div><div><div><font face="Courier">> newtype EventT m r a = E { runE :: (a -> m r) -> m r -> m r }</font></div><div><font face="Courier">> newtype ReactiveT m r a = R { runR :: (m a -> m r) -> m r }</font></div>
</div><div><div><font face="Courier">> type Event = EventT IO ()</font></div><div><font face="Courier">> type Reactive = ReactiveT IO ()</font></div></div><div><br></div><div>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.</div>
<div><br></div><div>I managed to write the following Applicative instance</div><div><br></div><div><font face="Courier">> instance Applicative (ReactiveT m r) where</font></div><div><div><font face="Courier">> pure a = R $ \k -> k (pure a)</font></div>
<div><font face="Courier">> R f <*> R a = R $ \k -> f (\f' -> a (\a' -> k $ f' <*> a'))</font></div></div><div><br></div><div>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.</div>
<div><br></div><div>Best regards,</div><div>Hans</div></div><br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div></div></div></blockquote></div><br></div>