Lecture Notes onMonadic Input and Output15-312: Foundations of Programming LanguagesFrank PfenningLecture 17October 28, 2004After reviewing the basic idea behind the encapsulation of effects, weintroduce input and output as a specific kind of effect. After store effects inthe last lecture, this will be our second example. For simplicity, we don’tconsider store and input/output simultaneously.In review, in a pure functional language programs are evaluated onlyto obtain a value. A loose characterization of an effect is simply everythingelse that a function might perform. Allocating, mutating, and reading stor-age cells is one example of effects, input and output are two more. We saythat effects are encapsulated if they do not interfere with the meaning of thepure expressions in a language. Standard ML does not encapsulate effects,Haskell does.Encapsulation of effects is achieved by separating pure expressions (e)from potentially effectful expressions (written as m). All the usual constructsin MinML remain pure expressions.Types τ : : = τ1→ τ2| · · · | τ ref |τPure Expressions e : : = fn(x.e) | apply(e1, e2) | · · · | comp(m)Monadic Expressions m : : = e | letcomp(e, x.m)| ref(e) | assign(e1, e2) | deref(e)In the concrete syntax, we write τ comp forτ and let comp x = e in m endfor letcomp(e, x. m). As an example, consider the following signature andimplementation.signature C =sigLECTURE NOTES OCTOBER 28, 2004L17.2 Monadic Input and Outputtype cval new : c compval inc : c -> unit compval get : c -> int compend;structure C :> C =structtype c = int refval new = comp (ref 0)val inc = fn r => comp (let comp x = !r in r := x+1 end)val get = fn r => comp (!r)end;Now we can create a cell, increment and read it with the following(monadic) expression, using a slight shorthand by allowing multiple dec-larations as in Standard ML.letcomp x = C.newcomp _ = C.inc xcomp y = C.get xinyend;When started in the empty memory, the above monadic expression ex-ecutes and evaluates to h(l=1), 1i for some l. It is worth writing out thiscomputation step by step to see exactly how computation proceeds andeffects and effect-free computations may be interleaved.In order to model input and output, the state that monadic expres-sions may refer to contains two streams: an input stream and an outputstream. Streams are potentially infinite sequence of integers, k1· · · kn· · ·.The empty stream is denoted by . We denote streams by s and write(sI, sO) for the pair of input and output streams. We have the constructsread, eof and write(e) for reading from the input stream, testing if the inputstream is empty, and writing the value of e to the output stream, respec-tively. These constructs must be monadic expressions, since they have aneffect.LECTURE NOTES OCTOBER 28, 2004Monadic Input and Output L17.3Γ ` read ÷ intΓ ` eof ÷ boolΓ ` e : intΓ ` write(e) ÷ 1As in the case of mutable storage, the operational semantics distin-guishes states for monadic expressions (which must include the input andoutput streams) and pure expressions (which does not include the inputand output streams).h(k · sI, sO), readi 7→ h(sI, s0), int(k)iReadh(k · sI, sO), eofi 7→ h(k · sI, sO), falseiEofFalseh(, sO), eofi 7→ h(, sO), trueiEofTruee 7→ e0h(sI, sO), write(e)i 7→ h(sI, sO), write(e0)iWriteArgv valueh(sI, sO), write(int(k))i 7→ h(sI, k · sO), h iiWriteThis language extension seems simple, although it is not completelytrivial to write programs using the monadic syntax. Moreover, we haveto formulate the progress theorem carefully. In fact, with the stated rules itfails! The reason is that if we try to read from an empty input stream no ruleis applicable. It is quite instructive to see where the proof of progress failsunless we incorporate the possibility that m may be blocked. In a concur-rent language (or even in a realistic sequential language) such blocking oninput can certainly occur, so it seems reasonable to allow for it and modelit. Of course, our language has no explicit mechanism of unblocking, butthis will change later on. So we are aiming at the following version of theprogress theorem.LECTURE NOTES OCTOBER 28, 2004L17.4 Monadic Input and OutputTheorem 1 (Progress)(1) If · ` e : τ then either(i) e 7→ e0for some e0, or(ii) e value(2) If · ` m ÷ τ then either(i) h(sI, sO), mi 7→ h(s0I, s0O), m0i for some s0I, s0Oand m0, or(ii) m = v and v value, or(iii) sI=  and m blocked.The first thought on how to define the judgment m blocked would be tosimply writeread blockedBlockedReadHowever, this is not enough as, again, a failed proof of the progress theo-rem should tell you. We may also be in the situation where the read is notat the top level, but is the first monadic expression to be executed. In otherwords, the search rules may lead us to a read expression. The general wayto capture this is with the rulem1blockedletcomp(comp(m1), x.m2) blockedBlockedLetNote that we never need to look at m2, nor do we need to account for thecase of letcomp(e, x.m2) where e is not a value, because a pure expression ecannot have an effect unless it is situated as in the BlockedLet rule.With the right definition of blocked states, it is then easy to prove theprogress theorem, employing value inversion as in other progress proofswe have carried out up to this point. We just have to be sure to cover all thepossible cases.We close the lecture with two simple examples. The first is a (non-recursive) computation which reads one integer and then writes to the out-put.val copyOne : unit comp =comp (let comp x = read in write x end)The next one is a recursive function to copy the whole input stream tothe output stream. This function should loop forever, if the input stream isinfinite.LECTURE NOTES OCTOBER 28, 2004Monadic Input and Output L17.5val copy : unit comp =rec copy =>comp (letcomp b = eofcomp x = if b then comp (letcomp _ = copyOnecomp _ = copyin () end)else comp ()in () end)This last example has some subtleties. For example, the conditional isa pure expression (and not a monadic expression). In order to properlyinterleave pure and effectful computation, it must be essentially where itis: on the right-hand side of a comp declaration, where both branches areagain computations.LECTURE NOTES OCTOBER 28,