{-# 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
EInt i) = DInt i
denote (EAdd e1 e2) =
denote (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
= DInt
int DInt i1) (DInt i2) = DInt (i1 + i2) add (
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
DInt i1) (DInt i2) = DInt (i1 * i2) mul (
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
= \ s -> (DInt s,s)
getG = \ s -> case e s of
putG e 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
Done x) k = k x
bind (Req r k1) k2 = Req r (\ x -> bind (k1 x) k2) bind (
We can finally write our denotations:
instance EArith Comp where
= Done . DCInt
int = bind e1 $ \ x1 -> case x1 of
add e1 e2 DCInt a -> bind e2 $ \ x2 -> case x2 of
DCInt b -> Done (DCInt (a + b))
instance EMul Comp where
= bind e1 $ \ x1 -> case x1 of
mul e1 e2 DCInt a -> bind e2 $ \ x2 -> case x2 of
DCInt b -> Done (DCInt (a * b))
instance GlobalIntState Comp where
= Req (ReqState Get) Done
getG = bind e $ \ x -> case x of
putG e 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