From c9307065b9e519890583bae865ed76fd27e7a8e9 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Thu, 14 Jan 2021 15:43:04 -0800
Subject: [PATCH] A short talk on the new parameterized moduels design

---
 docs/ParameterizedModules/Makefile |   7 +
 docs/ParameterizedModules/talk.md  | 210 +++++++++++++++++++++++++++++
 2 files changed, 217 insertions(+)
 create mode 100644 docs/ParameterizedModules/Makefile
 create mode 100644 docs/ParameterizedModules/talk.md

diff --git a/docs/ParameterizedModules/Makefile b/docs/ParameterizedModules/Makefile
new file mode 100644
index 00000000..0d92f952
--- /dev/null
+++ b/docs/ParameterizedModules/Makefile
@@ -0,0 +1,7 @@
+.PHONY: all
+
+all: talk.pdf
+
+talk.pdf: talk.md Makefile
+	pandoc --to beamer --output talk.pdf talk.md
+
diff --git a/docs/ParameterizedModules/talk.md b/docs/ParameterizedModules/talk.md
new file mode 100644
index 00000000..98d4edaf
--- /dev/null
+++ b/docs/ParameterizedModules/talk.md
@@ -0,0 +1,210 @@
+ML-Sytle Modules for Cryptol
+============================
+
+Modules
+--------
+
+* Cryptol uses a Haskell-style module system
+
+* A *module* is for managing names, and may:
+
+  - bring *entities* into scope via *imports*
+  - define new entities via *declarations*
+  - *export* entities that are in scope
+
+Example
+-------
+
+```cryptol
+module M where
+
+  import A(b)     // Brings `b` in scope
+
+  x = 2 * b       // Defines `x` (public)
+
+  private
+    y = x + x     // Defines `y` (private)
+```
+
+
+Parameterize Modules: Current Version
+-----------------------------
+
+:::::::::::::: {.columns}
+::: {.column}
+### Parameterized module:
+
+```cryptol
+module F where
+
+  parameter
+    type n : #
+    type constraint
+          (n >= 128)
+    key : [n]
+
+
+  f : [n] -> [n]
+  f x = key ^ x
+```
+:::
+::: {.column}
+### Instantiation:
+
+```cryptol
+module I = F where
+  type n = 256
+  key    = 17
+```
+:::
+::::::::::::::
+
+
+Issues
+------
+
+Common complaints:
+
+* Clunky
+  - Many small files for instantiation modules
+
+* Inflexible
+  - Cannot split a large parameterized module
+    into multiple files
+
+* Repetition
+  - Cannot name groups of parameters for reuse
+
+
+
+The New Design
+--------------
+
+* Nested modules
+* Signatures
+* Functors
+* Instantiation
+* Syntactic sugar
+
+
+Nested Modules
+--------------
+
+* New concept: module entities
+* Introduced via new declarations
+* Used through `open` (similar to `import`)
+* Module names are managed like any other name
+
+Example
+-------
+```cryptol
+module A where
+  x = 0x2            // defines `x`, a value
+
+  module B where     // defines `B`, a module
+    y = x + 1        // defines `y`, a value
+
+  open B(y)          // uses `B`, brings `y` in scope
+  z = 2 * y          // defines `z`, uses `y`
+```
+
+Signatures
+----------
+
+A named collection of module parameters:
+
+```cryptol
+signature S where
+  type n : #
+  type constraint (n >= 128)
+  key : [n]
+```
+
+Signature names are controlled by the
+module system like other declarations.
+
+Functors
+--------
+
+Modules may be parameterized with a parameter declaration:
+```cyrptol
+module F where
+
+  signature S     // Defines `S`, a signature
+    type n : #
+
+  parameter P : S // Uses `S`, brings `n` in scope
+
+  f : [n] -> [n]
+  f x = x
+```
+
+Note: `P` is *not* a normal name.
+
+
+Instantiation
+-------------
+
+Another way to introduce a module entitiy:
+```cryptol
+module I where
+
+  module Arg where
+    type n = 256
+
+  module A = F with { P = Arg }
+```
+
+Syntactic Sugar
+---------------
+
+* Omit parameter name (single parameter functors)
+* Instantiate single parameter functors
+* Anonymous modules (generative)
+* Combined `parameter` and `signature`
+* Combined declare and open
+
+
+Example
+-------
+A use case we'd like to support
+
+```cryptol
+module F where
+  parameter
+    type n : #
+    key : [n]
+
+  f : [n] -> [n]
+  f x = x ^ key
+
+module G where
+  import F where
+    type n = 8
+    key    = 0x23
+```
+
+Desugared
+---------
+```cryptol
+module F where
+
+  signature A1
+    type n : #
+    key : [n]
+
+  parameter Default : A1
+
+  f : [n] -> [n]
+  f x = x ^ key
+
+module G where
+
+  module A2 where
+    type n = 8
+    key    = 0x23
+
+  import F with { Default = A2 }
+```
+
+