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
