Re: [Haskell-cafe] Semantic Domain, Function, and denotational model.....
I noticed that Wikipedia has listed a few text books on the topic: http://en.wikipedia.org/wiki/Denotational_semantics#Textbooks Any recommendations on which one might be a better read? Thanks, Daryoush 2008/9/16 Greg Meredith [EMAIL PROTECTED]: Daryoush, Hopefully, the other replies about proving the monad laws already answered your previous question: yes! As for notions of semantic domain and denotational model, these ideas go back quite a ways; but, were given solid footing by Dana Scott. In a nutshell, we have essentially three views of a computation Operational -- computation is captured in a program and rules for executing it Logical -- computation is captured in a proof and rules for normalizing it Denotational -- computation is captured as a (completely unfolded) mathematical structure In the latter view we think of computations/programs as denoting some (usually infinitary) mathematical object. Our aim is to completely define the meaning of programs in terms of maps between their syntactic representation and the mathematical objects their syntax is intended to denote. (Notationally, one often writes such maps as [| - |] : Program - Denotation.) For example, we model terms in the lambda calculus as elements in a D-infinity domain or Bohm trees or ... . Or, in more modern parlance, we model terms in the lambda calculus as morphisms in some Cartesian closed category, and the types of those terms as objects in said category. The gold standard of quality of such a model is full abstraction -- when the denotational notion of equivalence exactly coincides with an intended operational notion of equivalence. In symbols, P ~ Q = [| P |] = [| Q |], where ~ and = are the operational and denotational notions of equivalence, respectively The techniques of denotational semantics have been very fruitful, but greatly improved by having to rub elbows with operational characterizations. The original proposals for denotational models of the lambda calculus were much too arms length from the intensional structure implicit in the notion of computation and thus failed to achieve full abstraction even for toy models of lambda enriched with naturals and booleans (cf the so-called full abstraction for PCF problem). On the flip side, providing a better syntactic exposure of the use of resources -- ala linear logic -- aided the denotational programme. More generally, operational models fit neatly into two ready-made notions of equivalence contextual equivalence -- behaves the same in all contexts bisimulation -- behaves the same under all observations Moreover, these can be seen to coincide with ready-made notions of equivalence under the logical view of programs. Except for syntactically derived initial/final denotational models -- the current theory usually finds a more home-grown denotational notion of equivalence. In fact, i submit that it is this very distance from the syntactic presentation that has weakened the more popular understanding of denotational models to just this -- whenever you have some compositionally defined map from one representation to another that respects some form of equivalence, the target is viewed as the denotation. Best wishes, --greg Date: Mon, 15 Sep 2008 10:13:53 -0700 From: Daryoush Mehrtash [EMAIL PROTECTED] Subject: Re: [Haskell-cafe] Semantic Domain, Function, and denotational model. To: Ryan Ingram [EMAIL PROTECTED] Cc: Haskell Cafe haskell-cafe@haskell.org Message-ID: [EMAIL PROTECTED] Content-Type: text/plain; charset=ISO-8859-1 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 [EMAIL PROTECTED] 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 [EMAIL PROTECTED] 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@haskell.org
Re: [Haskell-cafe] Semantic Domain, Function, and denotational model.....
, but greatly improved by having to rub elbows with operational characterizations. The original proposals for denotational models of the lambda calculus were much too arms length from the intensional structure implicit in the notion of computation and thus failed to achieve full abstraction even for toy models of lambda enriched with naturals and booleans (cf the so-called full abstraction for PCF problem). On the flip side, providing a better syntactic exposure of the use of resources -- ala linear logic -- aided the denotational programme. More generally, operational models fit neatly into two ready-made notions of equivalence contextual equivalence -- behaves the same in all contexts bisimulation -- behaves the same under all observations Moreover, these can be seen to coincide with ready-made notions of equivalence under the logical view of programs. Except for syntactically derived initial/final denotational models -- the current theory usually finds a more home-grown denotational notion of equivalence. In fact, i submit that it is this very distance from the syntactic presentation that has weakened the more popular understanding of denotational models to just this -- whenever you have some compositionally defined map from one representation to another that respects some form of equivalence, the target is viewed as the denotation. Best wishes, --greg Date: Mon, 15 Sep 2008 10:13:53 -0700 From: Daryoush Mehrtash [EMAIL PROTECTED] Subject: Re: [Haskell-cafe] Semantic Domain, Function, and denotational model. To: Ryan Ingram [EMAIL PROTECTED] Cc: Haskell Cafe haskell-cafe@haskell.org Message-ID: [EMAIL PROTECTED] Content-Type: text/plain; charset=ISO-8859-1 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 [EMAIL PROTECTED] 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 [EMAIL PROTECTED] 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- L.G. Meredith Managing Partner Biosimilarity LLC 806 55th St NE Seattle, WA 98105 +1 206.650.3740 http://biosimilarity.blogspot.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- L.G. Meredith Managing Partner Biosimilarity LLC 806 55th St NE Seattle, WA 98105 +1 206.650.3740 http://biosimilarity.blogspot.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Semantic Domain, Function, and denotational model.....
ّ 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 [EMAIL PROTECTED] 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 [EMAIL PROTECTED] 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 [EMAIL PROTECTED] 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 [EMAIL PROTECTED]
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@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] Semantic Domain, Function, and denotational model.....
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 [EMAIL PROTECTED]:
ّ 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 [EMAIL PROTECTED] 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 ::
Re: [Haskell-cafe] Semantic Domain, Function, and denotational model.....
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 [EMAIL PROTECTED]
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 [EMAIL PROTECTED]:
ّ 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 [EMAIL PROTECTED]
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
Re: [Haskell-cafe] Semantic Domain, Function, and denotational model.....
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 [EMAIL PROTECTED]:
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 [EMAIL PROTECTED]
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 [EMAIL PROTECTED]:
ّ 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 [EMAIL PROTECTED]
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
Re: [Haskell-cafe] Semantic Domain, Function, and denotational model.....
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 [EMAIL PROTECTED]:
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 [EMAIL PROTECTED]:
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 [EMAIL PROTECTED]
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 [EMAIL PROTECTED]:
ّ 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 [EMAIL PROTECTED]
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
}
Re: [Haskell-cafe] Semantic Domain, Function, and denotational model.....
exactly. it's a specification of the denotational semantics of time. any valid implementation must satisfy such properties. 2008/9/16 Ryan Ingram [EMAIL PROTECTED] 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 [EMAIL PROTECTED]: 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 [EMAIL PROTECTED]: 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 [EMAIL PROTECTED] 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 [EMAIL PROTECTED]: ّ 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 [EMAIL PROTECTED] 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
[Haskell-cafe] Semantic Domain, Function, and denotational model.....
Daryoush, Hopefully, the other replies about proving the monad laws already answered your previous question: yes! As for notions of semantic domain and denotational model, these ideas go back quite a ways; but, were given solid footing by Dana Scotthttp://en.wikipedia.org/wiki/Dana_Scott. In a nutshell, we have essentially three views of a computation - Operational http://en.wikipedia.org/wiki/Operational_semantics -- computation is captured in a program and rules for executing it - Logical http://en.wikipedia.org/wiki/Proof-theoretic_semantics -- computation is captured in a proof and rules for normalizing it - Denotational http://en.wikipedia.org/wiki/Denotational_semantics -- computation is captured as a (completely unfolded) mathematical structure In the latter view we think of computations/programs as denoting some (usually infinitary) mathematical object. Our aimhttp://en.wikipedia.org/wiki/Domain_theoryis to completely define the meaning of programs in terms of maps between their syntactic representation and the mathematical objects their syntax is intended to denote. (Notationally, one often writes such maps as [| - |] : Program - Denotation.) For example, we model terms in the lambda calculus as elements in a D-infinity domain or Bohm trees or ... . Or, in more modern parlance, we model terms in the lambda calculus as morphisms in some Cartesian closed category, and the types of those terms as objects in said category. The gold standard of quality of such a model is full abstractionhttp://en.wikipedia.org/wiki/Denotational_semantics#Full_abstraction-- when the denotational notion of equivalence exactly coincides with an intended operational notion of equivalence. In symbols, - P ~ Q = [| P |] = [| Q |], where ~ and = are the operational and denotational notions of equivalence, respectively The techniques of denotational semantics have been very fruitful, but greatly improved by having to rub elbows with operational characterizations. The original proposals for denotational models of the lambda calculus were much too arms length from the intensional structure implicit in the notion of computation and thus failed to achieve full abstraction even for toy models of lambda enriched with naturals and booleans (cf the so-called full abstraction for PCF problemhttp://en.wikipedia.org/wiki/Programming_language_for_Computable_Functions). On the flip side, providing a better syntactic exposure of the use of resources -- ala linear logic -- aided the denotational programme. More generally, operational models fit neatly into two ready-made notions of equivalence - contextual equivalencehttp://encyclopedia2.thefreedictionary.com/Contextual+equivalence-- behaves the same in all contexts - bisimulation http://en.wikipedia.org/wiki/Bisimulation -- behaves the same under all observations Moreover, these can be seen to coincide with ready-made notions of equivalence under the logical view of programs. Except for syntactically derived initial/final denotational models -- the current theory usually finds a more home-grown denotational notion of equivalence. In fact, i submit that it is this very distance from the syntactic presentation that has weakened the more popular understanding of denotational models to just this -- whenever you have some compositionally defined map from one representation to another that respects some form of equivalence, the target is viewed as the denotation. Best wishes, --greg Date: Mon, 15 Sep 2008 10:13:53 -0700 From: Daryoush Mehrtash [EMAIL PROTECTED] Subject: Re: [Haskell-cafe] Semantic Domain, Function, and denotational model. To: Ryan Ingram [EMAIL PROTECTED] Cc: Haskell Cafe haskell-cafe@haskell.org Message-ID: [EMAIL PROTECTED] Content-Type: text/plain; charset=ISO-8859-1 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 [EMAIL PROTECTED] 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 [EMAIL PROTECTED] 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
Re: [Haskell-cafe] Semantic Domain, Function, and denotational model.....
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 [EMAIL PROTECTED] 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@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] Semantic Domain, Function, and denotational model.....
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 [EMAIL PROTECTED] 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 [EMAIL PROTECTED] 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@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] Semantic Domain, Function, and denotational model.....
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 [EMAIL PROTECTED] 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 [EMAIL PROTECTED] 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 [EMAIL PROTECTED]
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@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
[Haskell-cafe] Semantic Domain, Function, and denotational model.....
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
