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