L8

Question 1

Explain Landin’s knot

Answer 1

203

Question 2

What is the problem associated with introducing state for the theory?

Answer 2

203-205

Every type is inhabited

Interaction between state + functions = recursive definitions

STLC is consistent but lost this when we added state

Question 3

Explain how to overcome the theoretical problem associated with state

Answer 3

206

Question 4

Describe the types, pure terms, impure terms, values, stores, contexts, store typings for the monadic language

Answer 4

207

Refs and T.
Get three new constructs for references.

Locations and wrapped impure code are both values.

Stores: loc -> value
Context: var -> type
Store Typing: loc -> type

Question 5

Give rules for pure term typing in monadic language

Answer 5

208

A location that stores a value of type X has type ref X.

Question 6

Give rules for effectful term typing in monadic language

Answer 6

209

let x=e;t – the e needs to be of type T X (i.e. wrapped)

return e implies that e is of (pure) type X — it isn’t effectful (conservative approximation)

Question 7

Give rules for pure op sem of monadic language

Answer 7

210

Question 8

What is the store typing relation? What is a configuration and configuration typing? Store and config typing for monadic language

Answer 8

213

• well typed store = given the asserted store typing, Sigma, is every location containing a well typed value consistent with what the store typing says for that location? (need two sigmas because one acts as an accumulator that is checked before everything has been added).
• ConfigOK=is store well typed and term well-typed (wrt impure typing relation, in empty var->type context?
• StoreCons also ensures that all expressions in store are closed.
• ConfigOK uses the effectful typing to check the term rather than the pure typing. A config’s term is essentially an impure rather than pure expression (for generality – as pure computations can’t depend on impure ones).

Question 9

• Pure Term Weakening:

Answer 9

214

New var can go anywhere in the context list

Question 10

• Pure Term Exchange:

Answer 10

214

Question 11

• Pure Term Substitution:

Answer 11

214

Question 12

• Effectful Term Weakening:

Answer 12

215

Remember to always use the effectful term type judgement for effectful terms

Effectful weakening is about the effectful type relation not the store typing

Question 13

• Effectful Term Exchange:

Answer 13

215

Question 14

• Effectful Term Substitution:

Answer 14

215

A pure term gets substituted into an effectful term

Question 15

Proof ordering for monadic language

Answer 15

216

Two mutually recursive judgements – need to prove each meta theory using mutual induction

Question 16

Store extension definition, store monotonicity lemma STATEMENT and proof principle

Answer 16

217

Question 17

Progress for MonL

Answer 17

218

A well typed config contains a term that is a wrapped return of a value or (imp) reduces

Question 18

Preservation for MonL

Answer 18

218

Question 19

Point of MonL

Answer 19

219

Question 20

Monads for iO language – types, pure terms, impure terms, values, contexts

Answer 20

220

Any {t} is a value

T_IO is parametrised by another type X

The impure terms have print/let/return constructs

Question 21

MonIOLan pure term typing

Answer 21

221 no store typing

Question 22

MonIOLan effectful term typing

Answer 22

222

return e also has the type of e but just under the imperative typing relation.

when a pure value is evaluated (unwrapped) by an impure let, it must have a monadic wrapper type

Question 23

MonIOLan op sem pure part

Answer 23

223

Question 24

MonIOLan op sem impure part

Answer 24

224

Remember

• impure term can’t reduce to a pure term (use return in cases where you’d want that e.g. print returning unit)
• let x = {t}; t1 … is an impure reduction context for t
• return itself needs to reduce its argument using the pure relation

Question 25

limits of MonIOLan wrt encapsulating effects + comparison with checked java exceptions

Answer 25

225-229

See Types.pages

Question 26

Effects in Koka

Answer 26

230

Question 27

Define the termination property

Answer 27

204

Question 28

Give impure operational semantics of MonLan

Answer 28

211-212

• when otherwise pure values as the result of impure reduction – use return e.g. for locations, unit
• pure expressions only reduce by pure reduction relation
• don’t treat stores as anything other than lists
• let x={t};t2 reduces t with the stateful reduction until it arrives at let x={return v};t

Question 29

Actual proof of store monotonicity for MonLan

Answer 29

Not given in notes, mentioned on 217