Update lecture 2

parent dc254b64
...@@ -211,7 +211,7 @@ evaluator would have to deal with type errors dynamically:: ...@@ -211,7 +211,7 @@ evaluator would have to deal with type errors dynamically::
... | _ | _ | _ = nothing ... | _ | _ | _ = nothing
**Exercise (difficulty: 1)** The above implementation is needlessly **Exercise (difficulty: 1)** The above implementation is needlessly
verbose, use the Maybe monad to hide the treatment of errors. verbose, use the Maybe monad to abstract away error handling.
The moral of this implementation is that we failed to encode our The moral of this implementation is that we failed to encode our
invariant in the datatype ``exp'`` and paid the price in the invariant in the datatype ``exp'`` and paid the price in the
...@@ -346,7 +346,9 @@ structuring compilers and proving them correct`_, (1980). This ...@@ -346,7 +346,9 @@ structuring compilers and proving them correct`_, (1980). This
reflects the influence it had on a generation of computer scientists reflects the influence it had on a generation of computer scientists
interested in language design on one hand (they gave us algebraic interested in language design on one hand (they gave us algebraic
datatypes) and verified compilation on the other hand (they gave us datatypes) and verified compilation on the other hand (they gave us
denotational models). denotational models). I learned these ideas from `Conor
McBride <http://strictlypositive.org/>`_, who had learned them from
`James McKinna <http://homepages.inf.ed.ac.uk/jmckinna/>`_.
************************************************ ************************************************
Computing normal forms of λ-terms Computing normal forms of λ-terms
...@@ -819,24 +821,24 @@ This might not deter the brave monadic programmer: we can emulate ...@@ -819,24 +821,24 @@ This might not deter the brave monadic programmer: we can emulate
We then simply translate the previous code to a monadic style, a We then simply translate the previous code to a monadic style, a
computer could do it automatically:: computer could do it automatically::
mutual reify : ∀{T} → ⟦ T ⟧Type → Fresh term
reify : ∀{T} → ⟦ T ⟧Type → Fresh term reflect : (T : type) → term → Fresh ⟦ T ⟧Type
reify {unit} nf = return nf
reify {A * B} (a , b) = reify a >>= λ a → reify {unit} nf = return nf
reify b >>= λ b reify {A * B} (a , b) = reify a >>= λ a
return (pair a b) reify b >>= λ b →
reify {S ⇒ T} f = gensym tt >>= λ s → return (pair a b)
reflect S (var s) >>= λ t reify {S ⇒ T} f = gensym tt >>= λ s
reify (f t) >>= λ b reflect S (var s) >>= λ t
return (lam s b) reify (f t) >>= λ b →
return (lam s b)
reflect : (T : type) → term → Fresh ⟦ T ⟧Type
reflect unit nf = return nf reflect unit nf = return nf
reflect (A * B) nf = reflect A (fst nf) >>= λ a → reflect (A * B) nf = reflect A (fst nf) >>= λ a →
reflect B (snd nf) >>= λ b → reflect B (snd nf) >>= λ b →
return (a , b) return (a , b)
reflect (S ⇒ T) neu = return (λ s → {!!}) reflect (S ⇒ T) neu = return (λ s → {!!})
-- XXX: cannot conclude with `reflect T (neu ! reify s)` -- XXX: cannot conclude with `reflect T (neu ! reify s)`
Excepted that, try as we might, we cannot reflect a function. Excepted that, try as we might, we cannot reflect a function.
...@@ -1159,7 +1161,8 @@ can easily be equipped with a renaming: we therefore take it as the ...@@ -1159,7 +1161,8 @@ can easily be equipped with a renaming: we therefore take it as the
**Remark:** The above construction of the exponential is taken from **Remark:** The above construction of the exponential is taken from
MacLane & Moerdijk's `Sheaves in Geometry and Logic`_ (p.46). MacLane & Moerdijk's `Sheaves in Geometry and Logic`_ (p.46).
At this stage, we have enough structure to interpret types::
At this stage, we have enough structure to interpret the types::
⟦_⟧ : type → Sem ⟦_⟧ : type → Sem
⟦ unit ⟧ = ⊤̂ ⟦ unit ⟧ = ⊤̂
......
No preview for this file type
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment