[Haskell-cafe] Semantic Domain, Function,
and denotational model.....
Ryan Ingram
ryani.spam at gmail.com
Tue Sep 16 17:55:06 EDT 2008
"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/
>
More information about the Haskell-Cafe
mailing list