msgodf · September 28, 2018 19:36 · Sep 28, 2018 · Sep 28, 2018 · Sep 28, 2018 · Sep 28, 2018
diff --git a/sl2018.md b/sl2018.md
@@ -325,4 +325,8 @@ Partial<T> is built in
    
 Like a list comprehension, but more like an object type comprehension
 
+## Roto
+
+Hammond organ simulator
+
 
diff --git a/sl2018.md b/sl2018.md
@@ -322,3 +322,7 @@ type Pair<T,U> = [T, U];
 Type transformations
 
 Partial<T> is built in
+   
+Like a list comprehension, but more like an object type comprehension
+
+
diff --git a/sl2018.md b/sl2018.md
@@ -287,3 +287,38 @@ type Shape =
 ```
 
 Pattern matching
+
+& operator to intersect types
+
+type NamedPoint = Point & Named
+
+
+Type Narrowing
+
+```typescript
+const x: number | string
+```
+
+Discriminated Union
+
+add a kind field
+
+Complex derivations
+
+communicate to the type system that there's a relationship between the first argument and the second argument
+
+a little function that pulls apart the first type and reconstructs it into the second type where the arguments are optional
+
+normally referred to as type-level programming
+
+Generics are functions
+
+const ident  = x => x; // value level
+type Ident<T> = T; // type-level
+   
+const pair = (x,y) => [x,Y]
+type Pair<T,U> = [T, U];
+
+Type transformations
+
+Partial<T> is built in
diff --git a/sl2018.md b/sl2018.md
@@ -260,4 +260,30 @@ var join : ('k, 'v Incr.t, 'cmp) Map.t Incr.t -> ('k, 'v, 'cmp)  Map.t Incr.t
 * SAC is a powerful optimization tool
 * Diff and patch are incremental functional glue
 
-https://github.com/janestreet/incr_dom
+https://github.com/janestreet/incr_dom
+
+## Understanding Typescript's Structural Typing System
+
+Works at Atomic Object
+
+When I hear people say "but most logic bugs aren't type errors" I just want to show them how to make bugs into type errors @mattoflambda
+
+Typescript has structure not nominal types
+
+Nominal type is like a secret club whereas a structural type is a minimal set of requirements that you need to be able get in
+
+Structural typing feels light
+
+But it's not enough
+
+Modelling invariants with type sets
+
+Sum Types (F#)
+
+```f#
+type Shape =
+  | Square of size : int
+  | Rectangle of width : int * height: int
+```
+
+Pattern matching
diff --git a/sl2018.md b/sl2018.md
@@ -225,3 +225,39 @@ val diff_map : 'a Incr.t -> (('a * 'b) option -> 'a -> 'b) -> 'b Incr.t
 ```
 
 ### Implementing `incr_map`
+
+* big implementation *
+
+### Mapping an incremental function over an incremental map
+
+```ocaml
+val incr_map' : ('k, 'v1, 'cmp) Map.t Incr.t -> ('v1 Incr.t -> 'v2 Incr.t) -> ('k, 'v2, 'cmp) Map.t Incr.t
+```
+
+Not going to implement this with diff_map, this is much more complicated.
+
+Split by key, process, and merge.
+
+### Split and Join
+
+```ocaml
+var split : 
+('k, 'v, 'cmp) Map.t Incr.t -> ('k, 'v Incr.t, 'cmp) Map.t Incr.t
+
+var join : ('k, 'v Incr.t, 'cmp) Map.t Incr.t -> ('k, 'v, 'cmp)  Map.t Incr.t
+```
+
+### Extending Incremental
+
+* `diff_map` works on any diffable data structure
+* Split and Join on top of Incremental 
+    * `incr_map` provides map speicific primatives
+    * `incr_select` for range and focus operations
+
+### Things to remember
+
+* UI design is an optimization problem - building efficient algorithms that make it possible
+* SAC is a powerful optimization tool
+* Diff and patch are incremental functional glue
+
+https://github.com/janestreet/incr_dom
diff --git a/sl2018.md b/sl2018.md
@@ -206,4 +206,22 @@ where
 let%map
 ``` 
 
-is sugar
+is sugar from https://github.com/janestreet/ppx_let
+
+### Diffing maps
+
+Symmetric diff function on two maps, produces a sequence of `Left`, `Right`, or `Unequal` (both, but with different values)
+
+Fast.
+
+Take this idea and embed it in an incremental computation
+
+### Hooking in Diffs with `diff_map`
+
+Previous value 
+
+```ocaml
+val diff_map : 'a Incr.t -> (('a * 'b) option -> 'a -> 'b) -> 'b Incr.t
+```
+
+### Implementing `incr_map`
diff --git a/sl2018.md b/sl2018.md
@@ -179,3 +179,31 @@ Dynamic graphs. But somewhat limited.
 
 * Map works for static structures
 * Bind adds (limited) dynamism - whole new computations on the right, compromising incrementality.
+
+How about incrementality sorting 10,000 things? It's not clear how you would do that.
+
+How can we be dynamic _and_ incremental?
+
+### Mapping over an incremental map
+
+```ocaml
+val incr_map : ('k, 'v1, 'cmp) Map.t Incr.t -> ('v1 -> 'v2) -> ('k, 'v2, cmp) Map.t Incr.t
+```
+
+Overloading here:
+
+Map the structure
+map the operation
+
+
+```ocaml
+let incr_map m f = let%map m = m in Map.map m f
+```
+
+where
+
+```ocaml
+let%map
+``` 
+
+is sugar
diff --git a/sl2018.md b/sl2018.md
@@ -163,6 +163,8 @@ Map can fan out, but not fan in. Hence we use Map2, which takes two incrementals
 val map2 : 'a Incr.t -> 'b Incr.t -> ('a -> 'b -> 'c) -> 'c Incr.t
 ```
 
+Static graphs/structure.
+
 ### Bind
 
 A page that shows one _or_ the other.
@@ -171,3 +173,9 @@ A page that shows one _or_ the other.
 val bind : 'a Incr.t -> ('a -> 'b Incr.t) -> 'b Incr.t
 ```
 
+Dynamic graphs. But somewhat limited.
+
+### Incremental thus far
+
+* Map works for static structures
+* Bind adds (limited) dynamism - whole new computations on the right, compromising incrementality.
diff --git a/sl2018.md b/sl2018.md
@@ -160,6 +160,14 @@ Apply map once to build the incrementals for each sub part. Apply it again to co
 Map can fan out, but not fan in. Hence we use Map2, which takes two incrementals. Merge the two virtual DOMs.
 
 ```ocaml
-map2 : 'a Incr.t -> 'b Incr.t -> ('a -> 'b -> 'c) -> 'c Incr.t
+val map2 : 'a Incr.t -> 'b Incr.t -> ('a -> 'b -> 'c) -> 'c Incr.t
+```
+
+### Bind
+
+A page that shows one _or_ the other.
+
+```ocaml
+val bind : 'a Incr.t -> ('a -> 'b Incr.t) -> 'b Incr.t
 ```
 
diff --git a/sl2018.md b/sl2018.md
@@ -155,5 +155,11 @@ Based on Acar's Self Adjusting Computations
 val map : 'a Incr.t -> ('a -> 'b) -> 'b Incr.t
 ```
 
+Apply map once to build the incrementals for each sub part. Apply it again to convert it to the virtual DOM.
 
+Map can fan out, but not fan in. Hence we use Map2, which takes two incrementals. Merge the two virtual DOMs.
+
+```ocaml
+map2 : 'a Incr.t -> 'b Incr.t -> ('a -> 'b -> 'c) -> 'c Incr.t
+```
 
diff --git a/sl2018.md b/sl2018.md
@@ -149,3 +149,11 @@ If the virtual DOM or model is big then it doesn't work so well.
 Your computation as a dependency graph
 Based on Acar's Self Adjusting Computations
 
+### Map and Map2
+
+```ocaml
+val map : 'a Incr.t -> ('a -> 'b) -> 'b Incr.t
+```
+
+
+
diff --git a/sl2018.md b/sl2018.md
@@ -134,5 +134,18 @@ Not that different to that used in React or Elm.
 
 ... -> Action -> Model -> Virtual DOM -> ...
 
+### Your UI as an Incremental Computation
 
+Lots of data in the initial render, but when things change they change in small ways. These small changes should be cheap to apply.
+
+Model -> Virtual DOM -> DOM
+
+Compute a diff between previous virtual DOM and the new one. Map that to changes to the DOM.
+
+If the virtual DOM or model is big then it doesn't work so well.
+
+### Incrementality with Incremental
+
+Your computation as a dependency graph
+Based on Acar's Self Adjusting Computations
 
diff --git a/sl2018.md b/sl2018.md
@@ -114,10 +114,25 @@ Rust doesn't have dependent types, we're wedging them in to through the type sys
 
 Should use Coq, Agda, or Isabelle. So they wrote Agda <=> Rust.
 
+
+Map the semantics of our Rust program into Agda, and use that to verify
+
+
 ## Data Driven UIs, Incrementally - Yaron Minsky
 
 Why do we care about this? Because we need UIs for _ourselves_. Data driven company. UIs that can dynamically transform and allow us to interact with the data.
 
+Table, lots of data (~100k rows). Data is changing.
+
+Jane Street use OCaml for everything! Including UIs.
+
+### Your UI as two functions
+
+A nice way of expressing UIs.
+
+Not that different to that used in React or Elm.
+
+... -> Action -> Model -> Virtual DOM -> ...
+
 
 
-Map the semantics of our Rust program into Agda, and use that to verify
diff --git a/sl2018.md b/sl2018.md
@@ -112,7 +112,7 @@ example of the vector of size N in Rust
 
 Rust doesn't have dependent types, we're wedging them in to through the type system. We don't trust the Rust compiler to enforce this.
 
-Should use Coq, Agda, or Isabelle
+Should use Coq, Agda, or Isabelle. So they wrote Agda <=> Rust.
 
 ## Data Driven UIs, Incrementally - Yaron Minsky
 

diff --git a/sl2018.md b/sl2018.md
@@ -99,3 +99,25 @@ CH correspondence
 "Dependently typed programs are by their nature, proof carrying code"
 
 Agda, or Idris
+
+Lazily evaluated, non-deterministic memory management
+
+=> Rust
+
+defining nats inductively in Rust types
+
+traits allow types to be treated like terms
+
+example of the vector of size N in Rust
+
+Rust doesn't have dependent types, we're wedging them in to through the type system. We don't trust the Rust compiler to enforce this.
+
+Should use Coq, Agda, or Isabelle
+
+## Data Driven UIs, Incrementally - Yaron Minsky
+
+Why do we care about this? Because we need UIs for _ourselves_. Data driven company. UIs that can dynamically transform and allow us to interact with the data.
+
+
+
+Map the semantics of our Rust program into Agda, and use that to verify
diff --git a/sl2018.md b/sl2018.md
@@ -65,17 +65,37 @@ ASIL - automotive safety integrity level (lowest A, highest D)
 
 Sensor input -> AI -> actuation
 
+ASIL D requires that mathematical modelling or proof is done.
+
 Program |___extraction___| Proof
 
 Proof assistant
 Coq
 Agda
 Haskell
 
-Not an option - Extraction target is C/C++
+None of these are an option - Extraction target is C/C++
+
+Could we extract the C program from a proof? There is some work on that. Generated code is terrifying, but "not to be inspected". Supposed to trust the extracting/generating code.
+
+Programs, syntax (formalized, its structure and contents) vs semantics (modeled, what it means to run the program)
+
+Denotational semantics - glue syntax to some meaning
+
+u8 -> {x|x E N ^ x <= 255}
+
+tableau - turnstile
+
+A simple type theory isn't rich enough for reasoning about our programs
+
+=> Dependent types
+
+"realize a continuum of precision up to a complete specification of a programs behaviour" - Why Dependent Types Matter
 
-Could we extract the C program from a proof? There is some work on that.
+http://www.cs.nott.ac.uk/~psztxa/publ/ydtm.pdf
 
+CH correspondence
 
+"Dependently typed programs are by their nature, proof carrying code"
 
-None of these
+Agda, or Idris
diff --git a/sl2018.md b/sl2018.md
@@ -53,3 +53,29 @@ Good questions are hard to write if you are an expert.
 Project quantum
 
 A corpus of high quality computing questions would be fantastically useful - to every teacher, year, and country.
+
+
+## Proof theory impressionism: Blurring the Curry-Howard line - Dan Pittman
+
+A problem that has caused him a great amount of anxiety
+
+Program |_____?_____| Proof
+
+ASIL - automotive safety integrity level (lowest A, highest D)
+
+Sensor input -> AI -> actuation
+
+Program |___extraction___| Proof
+
+Proof assistant
+Coq
+Agda
+Haskell
+
+Not an option - Extraction target is C/C++
+
+Could we extract the C program from a proof? There is some work on that.
+
+
+
+None of these
diff --git a/sl2018.md b/sl2018.md
@@ -1,32 +1,55 @@
-# SPJ keynote
+# Strange Loop 2018 notes
+
+## SPJ keynote
 
 http://csunplugged.org/sorting-networks
 
 communication
 
-Myth 1. it's all about computers
+### Myth 1. it's all about computers
 
 "Computer science is no more about computers than astronomy is about telescopes" - Dijkstra
 
 Ideas, not technology
 
-Myth 3. it's all about jobs
+### Myth 3. it's all about jobs
 
 It's about tomorrow's jobs, not today's
 
 Understanding the world, not just about jobs
 
-## Summary
+### Summary
 
 Ideas, not technology
 Every child, not just geeks
 Educational not instrumental
 Discipline, not skill
 
-## The UK journey
+### The UK journey
 
 2008 Computing at school 
 2010 CAS curriculum
 2011 Shut down or restart report by Royal Society
 2012 BCS invited to create a working group to draft the new Computing curriculu
-2014 New curriculum launches
+2014 New curriculum launches
+
+"You can say what you like, but it has to fit on two sides of A4"
+
+### Lesson 2. Get high-stakes examination rights
+### Lesson 3. Loving our teachers
+### Lesson 4. spend a tiny fraction of research
+
+Other subjects have centuries of experience; we have 5 years.
+Current practice is "gut feel". This is stupid. We should study what works and then do that.
+
+### Lesson 5. Leverage formative assessment
+
+Every teacher must come to an opinion about their students' understanding. They may do this informally, through project or programming work, or through _asking them questions_.
+
+Where do they get these questions from? Often they just make them up.
+
+Good questions are hard to write if you are an expert.
+
+Project quantum
+
+A corpus of high quality computing questions would be fantastically useful - to every teacher, year, and country.
diff --git a/sl2018.md b/sl2018.md
@@ -0,0 +1,32 @@
+# SPJ keynote
+
+http://csunplugged.org/sorting-networks
+
+communication
+
+Myth 1. it's all about computers
+
+"Computer science is no more about computers than astronomy is about telescopes" - Dijkstra
+
+Ideas, not technology
+
+Myth 3. it's all about jobs
+
+It's about tomorrow's jobs, not today's
+
+Understanding the world, not just about jobs
+
+## Summary
+
+Ideas, not technology
+Every child, not just geeks
+Educational not instrumental
+Discipline, not skill
+
+## The UK journey
+
+2008 Computing at school 
+2010 CAS curriculum
+2011 Shut down or restart report by Royal Society
+2012 BCS invited to create a working group to draft the new Computing curriculu
+2014 New curriculum launches
No results found