[Haskell-cafe] Semantic Domain, Function,
and denotational model.....
Conal Elliott
conal at conal.net
Tue Sep 16 18:23:57 EDT 2008
exactly. it's a specification of the denotational semantics of "time". any
valid implementation must satisfy such properties.
2008/9/16 Ryan Ingram <ryani.spam at gmail.com>
> "at time = id" is not valid Haskell. It's expositional, describing a
> law that "at" and "time" fulfill.
>
> It's like saying "m >>= return = m" when describing the Monad laws.
> You can't write that directly, but it better be true!
>
> -- ryan
>
> 2008/9/16 Daryoush Mehrtash <dmehrtash at gmail.com>:
> > I can sort of see what is happening in "time = O (pure (Fun id))".
> > But I am not sure I understand this:
> >
> > time :: Behavior Time
> > at time = id
> >
> > as I understand it "at" is a function that take Behaviour and returns
> > a function that is Time -> a. How can you have a function on the
> > left side of the equation?
> >
> > thanks,
> >
> > Daryoush
> >
> >
> > 2008/9/16 Conal Elliott <conal at conal.net>:
> >> Hi Ryan,
> >>
> >> Thanks very much for these explanations. Clear and right on!
> >>
> >> Best regards, - Conal
> >>
> >> P.S. I'll be at ICFP and am looking forward to seeing folks there.
> >>
> >> 2008/9/16 Ryan Ingram <ryani.spam at gmail.com>
> >>>
> >>> The key insight is that Behavior a is not necessarily a time function;
> >>> it's abstract. But you can treat it as if it was one by observing it
> >>> with "at".
> >>>
> >>> In Conal's paper, the internal type of behavior is:
> >>>
> >>> > -- composition of types; like (.) at the type level
> >>> > newtype O h g a = O (h (g a))
> >>>
> >>> > -- function type that can directly observe some constant functions
> >>> > data Fun t a = K a | Fun (t -> a)
> >>>
> >>> > -- Behavior a ~~ Reactive (Fun Time a)
> >>> > type Behavior = Reactive `O` Fun Time
> >>>
> >>> > -- Reactive has a current value and an event stream of values to
> switch
> >>> > to at particular times
> >>> > -- Then an event is just a reactive that might not have a current
> value
> >>> > until some time in the future.
> >>> > data Reactive a = Stepper a (Event a)
> >>> > newtype Event a = Ev (Future (Reactive a))
> >>>
> >>> Now, at the internal level, you can write the primitive "time" as
> >>>
> >>> > time :: Behavior Time
> >>> > time = O (pure (Fun id))
> >>>
> >>> with "pure" from the Applicative instance for Reactive:
> >>>
> >>> > pure x = Stepper x never
> >>>
> >>> "never" is a future that never occurs, so the reactive value never
> >>> changes.
> >>>
> >>> From a users' point of view, all this is invisible--you only get a few
> >>> observation functions (including "at"). Internally, however, constant
> >>> behaviors, or behaviors that contain "steps" that are constant, can be
> >>> evaluated extremely quickly; once the behavior returns K x, you know
> >>> that the result can't change until the next event in the reactive
> >>> stream. You only need to continuously evaluate the behavior if you
> >>> get a "Fun" result. See sinkB on page 9 of the paper to understand
> >>> how this is used to improve performance.
> >>>
> >>> The semantic function "at" drives the model; it allows you to describe
> >>> the laws for the library to fulfill very succinctly:
> >>>
> >>> at (fmap f x) = fmap f (at x)
> >>> at (pure x) = pure x
> >>> at (f <*> x) = at f <*> at x
> >>> at (return x) = return x
> >>> at (m >>= f) = at m >>= at . f
> >>> etc.
> >>>
> >>> Similarily, for Futures, we have "force :: Future a -> (Time, a)"
> >>>
> >>> force (fmap f z) = (t, f x) where (t,x) = force z
> >>> force (pure x) = (minBound, x)
> >>> force (ff <*> fx) = (max tf tx, f x) where (tf, f) = force ff ; (tx,
> >>> x) = force fx
> >>> force (return x) = (minBound, x)
> >>> force (m >>= f) = (max tm tx, x) where (tm, v) = force m; (tx, x) =
> force
> >>> (f v)
> >>> etc.
> >>>
> >>> This gives the library user solid ground to stand on when reasoning
> >>> about their code; it should do what they expect. And it gives the
> >>> library author a very strong goal to shoot for: just fulfill these
> >>> laws, and the code is correct! This allows radical redesigns of the
> >>> internals of the system while maintaining a consistent and intuitive
> >>> interface that reuses several classes that the user is hopefully
> >>> already familiar with: monoids, functors, applicative functors, and
> >>> monads.
> >>>
> >>> -- ryan
> >>>
> >>> 2008/9/16 Daryoush Mehrtash <dmehrtash at gmail.com>:
> >>> > ّ I don't follow the "at" and "type B a". "Behavior a" itself is a
> >>> > time function. At least in the version of the code that was
> >>> > developed in Pual Hudak's Haskell School of Expression it was defined
> >>> > as:
> >>> >
> >>> >> newtype Behavior a
> >>> >> = Behavior (([Maybe UserAction],[Time]) -> [a])
> >>> >
> >>> > In a function like time you can see that the "at" function makes
> things
> >>> > simpler.
> >>> >
> >>> > In the original version time was defined as:
> >>> >
> >>> >> time :: Behavior Time
> >>> >> time = Behavior (\(_,ts) -> ts)
> >>> >
> >>> > In Conal's paper
> >>> >
> >>> > time :: Behavior Time
> >>> > at time = id
> >>> >
> >>> > Comparing the two implementation of the time, it seems to me that
> "at"
> >>> > and "type B a" has put the design on a more solid ground. But I
> don't
> >>> > quite understand the thought process, or the principal behind what is
> >>> > happening.
> >>> >
> >>> > daryoush
> >>> >
> >>> >
> >>> > On Mon, Sep 15, 2008 at 10:46 AM, Ryan Ingram <ryani.spam at gmail.com>
> >>> > wrote:
> >>> >> Here's a quick overview that might help you.
> >>> >>
> >>> >> For a reactive behavior, we have two types to think about:
> >>> >>
> >>> >> type B a = Time -> a
> >>> >> (the semantic domain)
> >>> >>
> >>> >> data Behavior a = ?
> >>> >> (the library's implementation).
> >>> >> at :: Behavior a -> B a
> >>> >> (observation function)
> >>> >>
> >>> >> This is really just classic "information hiding" as you would do
> with
> >>> >> any abstract data type. Consider a simple "stack" data structure
> that
> >>> >> supports push and pop.
> >>> >>
> >>> >>> data S a = S
> >>> >>> { popS :: Maybe (a, S a)
> >>> >>> , pushS :: a -> S a
> >>> >>> }
> >>> >>
> >>> >>> data Stack a = ?
> >>> >>> observeStack :: Stack a -> S a
> >>> >>
> >>> >> As a library user, you don't really care about the implementation of
> >>> >> Stack, just as a user of Conal's library doesn't really care about
> the
> >>> >> implementation of Behavior. What you *do* care about is that you
> can
> >>> >> think about it in the simpler terms of "Time -> a" which is the
> model
> >>> >> he has chosen.
> >>> >>
> >>> >> The rest of the library design comes from taking that model and
> >>> >> thinking about what typeclasses and operations "Time -> a" should
> >>> >> support, and creating typeclass morphisms between Behavior a and B a
> >>> >> where necessary. For example:
> >>> >>
> >>> >>> -- This makes (r -> a) into a functor over a; it is a
> generalization
> >>> >>> of Time -> a
> >>> >>> instance Functor ((->) r) where
> >>> >>> -- fmap :: (a -> b) -> (r -> a) -> (r -> b)
> >>> >>> fmap f x = \r -> f (x r)
> >>> >>> -- or, "fmap = (.)", if you're golfing :)
> >>> >>
> >>> >> In order for the morphism between B and Behavior to make sense, you
> >>> >> want this law to hold:
> >>> >> fmap f (at behavior) = at (fmap f behavior)
> >>> >> for all behavior :: Behavior a.
> >>> >>
> >>> >> The fmap on the left applies to B which is (Time ->); the fmap on
> the
> >>> >> right applies to Behavior.
> >>> >>
> >>> >> Conal writes this law more elegantly like this:
> >>> >>> instance(semantic) Functor Behavior where
> >>> >>> fmap f . at = at . fmap f
> >>> >>
> >>> >> As long as you as the user can think about behaviors generally as
> >>> >> functions of Time, you can ignore the implementation details, and
> >>> >> things that you expect to work should work. This drives the design
> of
> >>> >> the entire library, with similar morphisms over many typeclasses
> >>> >> between Event and E, Reactive and B, etc.
> >>> >>
> >>> >> -- ryan
> >>> >>
> >>> >> On Mon, Sep 15, 2008 at 10:13 AM, Daryoush Mehrtash
> >>> >> <dmehrtash at gmail.com> wrote:
> >>> >>> Interestingly, I was trying to read his paper when I realized that
> I
> >>> >>> needed to figure out the meaning of denotational model, semantic
> >>> >>> domain, semantic functions. Other Haskell books didn't talk about
> >>> >>> design in those terms, but obviously for him this is how he is
> driving
> >>> >>> his design. I am looking for a simpler tutorial, text book like
> >>> >>> reference on the topic.
> >>> >>>
> >>> >>> Daryoush
> >>> >>>
> >>> >>> On Mon, Sep 15, 2008 at 1:33 AM, Ryan Ingram <ryani.spam at gmail.com
> >
> >>> >>> wrote:
> >>> >>>> I recommend reading Conal Elliott's "Efficient Functional
> Reactivity"
> >>> >>>> paper for an in-depth real-world example.
> >>> >>>>
> >>> >>>> http://www.conal.net/papers/simply-reactive
> >>> >>>>
> >>> >>>> -- ryan
> >>> >>>>
> >>> >>>> On Sun, Sep 14, 2008 at 11:31 AM, Daryoush Mehrtash
> >>> >>>> <dmehrtash at gmail.com> wrote:
> >>> >>>>> I have been told that for a Haskell/Functional programmer the
> >>> >>>>> process
> >>> >>>>> of design starts with defining Semantic Domain, Function, and
> >>> >>>>> denotational model of the problem. I have done some googling on
> the
> >>> >>>>> topic but haven't found a good reference on it. I would
> >>> >>>>> appreciate
> >>> >>>>> any good references on the topic.
> >>> >>>>>
> >>> >>>>> thanks,
> >>> >>>>>
> >>> >>>>> daryoush
> >>> >>>>>
> >>> >>>>> ps. I have found referneces like
> >>> >>>>> http://en.wikibooks.org/wiki/Haskell/Denotational_semantics which
> >>> >>>>> talks about semantic domain for "the Haskell programs 10, 9+1,
> 2*5"
> >>> >>>>> which doesn't do any good for me. I need something with a more
> >>> >>>>> real
> >>> >>>>> examples.
> >>> >>>>> _______________________________________________
> >>> >>>>> 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
> >>>
> >>
> >>
> >
> >
> >
> > --
> > Daryoush
> >
> > Weblog: http://perlustration.blogspot.com/
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080917/c102bd43/attachment.htm
More information about the Haskell-Cafe
mailing list