msgodf/sl2018.md

## sl2018.md

      
                Raw

        
              sl2018.md
            
          
    Strange Loop 2018 notes
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
"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.
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
ASIL D requires that mathematical modelling or proof is done.
Program |extraction| Proof
Proof assistant
Coq
Agda
Haskell
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
http://www.cs.nott.ac.uk/~psztxa/publ/ydtm.pdf
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. 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 -> ...
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
Map and Map2
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.
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.
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.

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
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
let incr_map m f = let%map m = m in Map.map m f
where
let%map
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
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
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
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
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#)
type Shape =
  | Square of size : int
  | Rectangle of width : int * height: int
Pattern matching
& operator to intersect types
type NamedPoint = Point & Named
Type Narrowing
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; // type-level
const pair = (x,y) => [x,Y]
type Pair<T,U> = [T, U];
Type transformations
Partial is built in
Like a list comprehension, but more like an object type comprehension
Roto
Hammond organ simulator