{-# LANGUAGE FlexibleInstances #-}

Having An Effect

This blog post will be on denotational semantics, the sister of operational semantics, and how to make it more modular.

Denotational semantics is a compositional mapping from expressions in a language to something else. (Oleg Kiselyov, 2017)

What that something else is, the author of the denotational semantics may decide. It is frequently some collection of mathematical objects. We often call these something else ‘values’. The other part of the definition that needs explanation is the compositional mapping. This can be explained as the denotation of an expression composed of other expression only relies on the denotation of these subexpressions. We will see an example of this property shortly.

Now I will give a small example of a denotational semantics for a toy language. Its only use is explaining things. Here it is:

data Exp = EInt Int | EAdd Exp Exp deriving Show

In order to give these toy expressions a denotational semantics we will need a domain of values to map them to. In this case the domain will be a haskell value.

data Dom = DInt Int deriving Show

We want to create a mapping from Exp to Dom. A noisy functional programmer will immediately start yelling “function!”, but this is not always the case as we will see later on. This compositional mapping function often bears the name eval, but for clarity we will cal it denote. It can also called an interpreter. I will use the words denoter and interpreter interchangeably.

denote :: Exp -> Dom
denote (EInt i) = DInt i
denote (EAdd e1 e2) =
  case denote e1 of
    DInt i1 ->
      case denote e2 of
        DInt i2 ->
          DInt (i1 + i2)

The first definition is trivial: integer expressions map to integer values. What this tells us is that expressions that can not be reduced (these are also sometimes called values, confusingly), need a value in the domain of the denotational semantics. The second defintion shows us how the compositional property works in practice: we can define denote recursively. Our denotational semantics has no types, and that is fine for now, but if we would for example add boolean expressions to our language we would also have need for a DError data-type in our domain. This is because we do not allow boolean values to be added to each other (some languages do allow this, for example C).

There is another benefit of denotational semantics: we can prove that two expressions are denotationally equivalent. When two expressions are denotationally equivalent, we then have grounds for replacing one with the other. This can be used by compilers to optimize code. In our toy language we can interchange EInt 42, EAdd (EInt 13) (EInt 29), EAdd (EInt 29) (EInt 13), without loosing any ‘meaning’.

If we want to extend our language with more expressions, we will need to write a new expression data-type, or add these expressions to our existing data-type. In any case we will need to recompile our code. For now this is just and artifact of the Haskell embedding I proposed. If we wrote our semantics on paper, we could just refer to the page of our previous definition and put some ellipses somewhere. This holds for now, but there are semantics which even break the ellipses. We will solve this unstable denotation problem in Haskell by using typeclasses for now.

class EArith d where
  int :: Int -> d
  add :: d -> d -> d

We have defined an interface EArith that depends on the type variable d which represents the type of our domain. We can now give our compositional mapping by declaring an instance with our previous Dom data-type (NOT a function):

instance EArith Dom where
  int = DInt
  add (DInt i1) (DInt i2) = DInt (i1 + i2)

The compositionality of the denotational semantics now becomes even more apparent. Let’s prove our point by extending our expressions and semantics. We first define the typeclass:

class EMul d where
  mul  :: d -> d -> d

instance EMul Dom where
  mul (DInt i1) (DInt i2) = DInt (i1 * i2)

We can now write expressions which use int, add, and mul, they will all have type Dom.

If we were to add boolean values to our expressions, we would also have to extend our domain, but this is a trivial change and more importantly we don’t have to rewrite our denotations. There is a more fundamental change that arises when we add state to our expression language, which does require changing all of our denoters, which was the thing we were trying to avoid. Here is the culprit:

class GlobalIntState d where
  getG :: d
  putG :: d -> d

If we try to declare an instance for these expressions, we get stuck. We need some state variable to decide what integer to get for getG. Represented in a type:

type DomIntState = Int -> (Dom,Int)

Now we can declare our instance:

instance GlobalIntState DomIntState where
  getG   = \ s -> (DInt s,s)
  putG e = \ s -> case e s of
    (DInt s',_) -> (DInt s',s')

To solve our domain problems we will pick a new domain. To be more precise, we put a nice layer on top. Our new domain will consist of computations, which are made up of two parts: values and requests. Kiselyov uses a specific abstraction for this, that shows nicely the relation between our previous work and the improved version. The function with type DomC -> Comp is called a continuation.

data Comp = Done DomC | Req ReqT (DomC -> Comp)

data DomC = DCInt Int

data ReqT = ReqState StateReq

data StateReq = Get | Put Int

We then find that Comp is a monad:

bind :: Comp -> (DomC -> Comp) -> Comp
bind (Done x) k    = k x
bind (Req r k1) k2 = Req r (\ x -> bind (k1 x) k2)

We can finally write our denotations:

instance EArith Comp where
  int = Done . DCInt
  add e1 e2 = bind e1 $ \ x1 -> case x1 of
    DCInt a -> bind e2 $ \ x2 -> case x2 of
      DCInt b -> Done (DCInt (a + b))

instance EMul Comp where
  mul e1 e2 = bind e1 $ \ x1 -> case x1 of
    DCInt a -> bind e2 $ \ x2 -> case x2 of
      DCInt b -> Done (DCInt (a * b))

instance GlobalIntState Comp where
  getG   = Req (ReqState Get) Done
  putG e = bind e $ \ x -> case x of
    DCInt x -> Req (ReqState (Put x)) Done

We will have to write a handler for state. The drawback of this approach is that we can not use do-notation, because Comp is not parametarized over a type variable. It can only use DomC as instructions. There is a relation betweeen ReqT and the continuation supplied to Req. Currently we can use any ReqT with any function, which is not what we want to allow.

References

This blog post is mostly a transcription of the following lecture by Kiselyov. I highly recommend watching it. He also goes into the history of the subject and there are a lot of golden knowledge nuggets to be found.

[In English] Functional Thursday #Special – Having an Effect by Oleg Kiselyov, https://www.youtube.com/watch?v=GhERMBT7u4w

I also used some concepts from this web page. The whole blog post is just a freer monad view.

The Operational Monad Tutorial https://apfelmus.nfshost.com/articles/operational-monad.html