From 117d0f3b6bb07c4a1d4ee39b9db04a51eda2c546 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-=C3=89variste=20Dagand?=
Date: Thu, 15 Feb 2018 16:24:12 +0100
Subject: [PATCH] Add takeaways
---
agda/01-effectful/Monad.lagda.rst | 9 +++++++-
agda/02-dependent/Indexed.lagda.rst | 32 ++++++++++++++++++++---------
agda/03-total/Recursion.lagda.rst | 9 ++++++++
3 files changed, 39 insertions(+), 11 deletions(-)
diff --git a/agda/01-effectful/Monad.lagda.rst b/agda/01-effectful/Monad.lagda.rst
index f57e621..0322071 100644
--- a/agda/01-effectful/Monad.lagda.rst
+++ b/agda/01-effectful/Monad.lagda.rst
@@ -23,12 +23,19 @@ Today, we shall:
- present a general framework for modelling *algebraic* effects
- meet a few monads (reader, writer, non-determinism, random, CPS, etc.)
-`Notions of computations determine monads`_:
+Vision: `Notions of computations determine monads`_
1. syntax of effectful operations
2. equational theory of effectful operations
3. denotational semantics = quotiented syntax
4. interpreter / monad!
+Takeaways:
+ - you will be *able* to define a monad (``return``, ``bind``) and its supporting operations
+ - you will be *able* to use the following monads: exceptions, reader, writer, state, non-determinism
+ - you will be *able* to relate an equational theory with a monadic presentation (normalization-by-evaluation)
+ - you will be *familiar* with algebraic effects
+ - you will be *familiar* with the most commonly used monads
+
************************************************
Historical background
diff --git a/agda/02-dependent/Indexed.lagda.rst b/agda/02-dependent/Indexed.lagda.rst
index f9f81d6..6e128dc 100644
--- a/agda/02-dependent/Indexed.lagda.rst
+++ b/agda/02-dependent/Indexed.lagda.rst
@@ -34,6 +34,13 @@ Today, we shall:
The vision: `The Proof Assistant as an Integrated Development Environment`_
+Takeaways:
+ - you will be *able* to use inductive families to encode structural invariants
+ - you will be *able* to write dependently-typed programs over inductive families
+ - you will be *able* to construct denotational models in type theory
+ - you will be *familiar* with the Yoneda lemma
+ - you will be *familiar* with the notion of functor and presheaf
+ - you will be *familiar* with normalization-by-evaluation for the simply-typed calculus
..
::
@@ -45,6 +52,7 @@ The vision: `The Proof Assistant as an Integrated Development Environment`_
Typing ``sprintf``
************************************************
+
..
::
@@ -1258,15 +1266,18 @@ implementation::
-By defining a richly-structured model, we have seen how we could
-implement a typed model of the λ-calculus and manipulate binders in
-the model.
+************************************************
+Conclusion
+************************************************
+
+In the first and second part, we have seen how inductive types and
+families can be used to build initial models, supporting the
+definition of various interpretations in Agda itself.
+
+In the third part, we have seen how, by defining a richly-structured
+model, we could implement a typed model of the λ-calculus and
+manipulate binders in the model.
-Takeaways:
- * You are *familiar* with the construction of denotational models in type theory
- * You are *able* to define an inductive family that captures exactly some structural invariant
- * You are *able* to write a dependently-typed program
- * You are *familiar* with normalization-by-evaluation proofs for the simply-typed calculus
**Exercises (difficulty: open ended):**
@@ -1284,9 +1295,10 @@ Takeaways:
categorical semantics (described in the next section) provides
the blueprint of the necessary proofs.
--------------------------------------
+
+************************************************
Optional: Categorical spotting
--------------------------------------
+************************************************
..
::
diff --git a/agda/03-total/Recursion.lagda.rst b/agda/03-total/Recursion.lagda.rst
index 0b2b098..4bee09a 100644
--- a/agda/03-total/Recursion.lagda.rst
+++ b/agda/03-total/Recursion.lagda.rst
@@ -62,6 +62,14 @@ The vision: `Total Functional Programming`_
- zealously pursued with dependent types by `Conor McBride `_
- at the origin of *all* of today's examples
+Takeaways:
+ - you will be *able* to reify a measure by indexing an inductive type
+ - you will be *able* to define your own induction principles
+ - you will be *able* to give a "step-indexed" interpretation of a general recursive function
+ - you will be *familiar* with the Bove-Capretta technique
+ - you will be *familiar* with the notion of monad morphism
+
+
************************************************
First-order Unification
************************************************
@@ -483,6 +491,7 @@ underlying composition of substitutions::
Structurally: most-general unifier
--------------------------------------
+
The implementation of the most-general unifier is exactly the same,
excepted that termination has become self-evident: when performing the
substitution (case ``amgu {suc k} _ _ (m , (σ ∷[ r / z ]))``), the
--
GitLab