Strange Loop 2018

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