fix typos, add diagram

Author: liesnikov

slides/Makefile

@@ -23,20 +23,23 @@ main.tex: main.md macros.tex Makefile bib.bib
          --slide-level=2 \
          -o main.tex
 
-figures: dependent-types-compiler.pdf dependent-types-typechecker.pdf dependent-types-general.pdf prior-work.pdf
+figures: dependent-types-compiler.pdf dependent-types-typechecker.pdf dependent-types-general.pdf prior-work.pdf architecture-diagram.pdf
 
-dependent-types-compiler.pdf:
+dependent-types-compiler.pdf: dependent-types-compiler.svg
 	inkscape ./dependent-types-compiler.svg --export-pdf=dependent-types-compiler.pdf
 
-dependent-types-typechecker.pdf:
+dependent-types-typechecker.pdf: dependent-types-typechecker.svg
 	inkscape ./dependent-types-typechecker.svg --export-pdf=dependent-types-typechecker.pdf
 
-dependent-types-general.pdf:
+dependent-types-general.pdf: dependent-types-general.svg
 	inkscape ./dependent-types-general.svg --export-pdf=dependent-types-general.pdf
 
-prior-work.pdf:
+prior-work.pdf: prior-work.svg
 	inkscape ./prior-work.svg --export-pdf=prior-work.pdf
 
+architecture-diagram.pdf: architecture-diagram.svg
+	inkscape ./architecture-diagram.svg --export-pdf=architecture-diagram.pdf
+
 open: main.pdf
 	xdg-open main.pdf &
 

slides/architecture-diagram.svg

@@ -115,7 +115,7 @@ f k _¹ (C _² _³) (succ zero)
 
 * replace `_¹` with `?¹`
 * we know that `?¹ : F k`
-* looking up `t` yields type `T ?² ?³`
+* elaborating `(C _² _³)` yields type `T ?² ?³`
 * produce a constraint `?¹ ~ T ?² ?³`
 
 ## How do constraints work
@@ -215,6 +215,10 @@ Bottom line: this is a design study
 * each constraint raised gets an opportunity to be solved/simplified immediately by the user-supplied solver
 * if it doesn't - we can freeze the problem and return a meta in place of the typechecked solution
 
+## Design overview
+
+![](./architecture-diagram.pdf)
+
 ## Open questions
 
 ::: incremental
@@ -236,17 +240,22 @@ Current idea:
 
 * there is machinery in Haskell to declare interfaces [@pangPluggingHaskell2004]
 * what should the interface look like?
-* ```
+```
   data SolverTag = ...
   
-  type Solver = ConstraintF c -> (Set (ConstraintF c), Map MetaId Term)
+  type Solver = ConstraintF c -> ( Set (ConstraintF c)
+                                 , Map MetaId Term )
   
   data PluginInterface = Plugin {
     solvers :: Map SolverTag Solver,
     solverTags :: [SolverTag],
     priorities :: [(SolverTag, SolverTag)]
   }
-  
+```
+
+## how does dynamic linking interfere with what we can do
+
+```
   instance ConstraintMap constraintTag ConstraintType where
   ...
   
@@ -269,7 +278,7 @@ Current idea:
 * Lean
   * uses macros to redefine symbols
   * uses reflection and typechecking monads to define custom elaboration procedures
-* TypeOS
+* TypOS
   * you have to buy into a whole new discipline
   * we hope to keep things a bit more conventional engineering-wise