L8 Flashcards
Explain Landin’s knot
203
What is the problem associated with introducing state for the theory?
203-205
Every type is inhabited
Interaction between state + functions = recursive definitions
STLC is consistent but lost this when we added state
Explain how to overcome the theoretical problem associated with state
206
Describe the types, pure terms, impure terms, values, stores, contexts, store typings for the monadic language
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
Give rules for pure term typing in monadic language
208
A location that stores a value of type X has type ref X.
Give rules for effectful term typing in monadic language
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)
Give rules for pure op sem of monadic language
210
What is the store typing relation? What is a configuration and configuration typing? Store and config typing for monadic language
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).
• Pure Term Weakening:
214
New var can go anywhere in the context list
• Pure Term Exchange:
214
• Pure Term Substitution:
214
• Effectful Term Weakening:
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
• Effectful Term Exchange:
215
• Effectful Term Substitution:
215
A pure term gets substituted into an effectful term
Proof ordering for monadic language
216
Two mutually recursive judgements – need to prove each meta theory using mutual induction
Store extension definition, store monotonicity lemma STATEMENT and proof principle
217
Progress for MonL
218
A well typed config contains a term that is a wrapped return of a value or (imp) reduces
Preservation for MonL
218
Point of MonL
219
Monads for iO language – types, pure terms, impure terms, values, contexts
220
Any {t} is a value
T_IO is parametrised by another type X
The impure terms have print/let/return constructs
MonIOLan pure term typing
221 no store typing
MonIOLan effectful term typing
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
MonIOLan op sem pure part
223
MonIOLan op sem impure part
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
