[Haskell-cafe] Semantic Domain, Function, and denotational model.....

Daryoush Mehrtash dmehrtash at gmail.com
Tue Sep 16 15:39:43 EDT 2008


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/


More information about the Haskell-Cafe mailing list