Denotational Semantics

The goal here is to define a meaning function from Behaviors to some semantic domain in such a way that type class instances pull back from the instances on the semantic domain, in the sense of type class morphisms.

The implementation of a Behavior is polymorphic in the choice of underlying Event. The meaning function is specified with respect to the Semantic event type provided in this module.

We consider behaviors which are valid sampling functions. Precisely, a Behavior (Semantic time) a, which is a function of type

b :: forall b. Semantic time (a -> b) -> Semantic time b

should preserve the set of input times in the output:

map fst (unwrap (b e)) = map fst (unwrap e) :: List time

The semantic domain for these behaviors is just the function type

time -> a

The meaning of the sampling function b is then the function

\t -> valueOf (sample b (once t identityentity))


valueOf (Semantic (Tuple _ a : Nil)) = a
once t a = Semantic (Tuple t a : Nil)

Note that the time-preservation property ensures that the result of applying b is an event consisting of a single time point at time t, so this is indeed a well-defined function.

In addition, we have this property, due to time-preservation:

sample b (once t f) = once t (valueOf (sample b (once t f)))



map of the meaning is the meaning of map:

map f (meaning b)
= f <<< meaning b
= \t -> f (valueOf (sample b (once t identity)))
  {- parametricity -}
= \t -> valueOf (sample b (map (_ <<< f) (once t identity)))
= meaning (map f b)


<*> of the meanings is the meaning of <*>:

meaning (a <*> b)
= \t -> valueOf (sample (a <*> b) (once t identity))
= \t -> valueOf (sample b (sample a (compose <$> once t identity)))
= \t -> valueOf (sample b (sample a (once t identity)))
= \t -> valueOf (sample b (sample a (once t identity)))
  {- sampling preserves times -}
= \t -> valueOf (sample b (once t (valueOf (sample a (once t identity))))
= \t -> valueOf (sample b (once t (meaning a t)))
  {- parametricity -}
= \t -> meaning a t (valueOf (sample b (once t identity)))
= \t -> meaning a t (meaning b t)
= meaning a <*> meaning b


The meaning of pure is pure:

meaning (pure a)
= \t -> valueOf (sample (pure a) (once t identity))
= \t -> a
= pure a

#Semantic Source

newtype Semantic time a

The semantic domain for events