Conor McBride. At the whiteboard. An attempt to give a characterization of
the state monad, following exactly what get and put do.

  State : S -> * -> S -> *
    -- State s1 a s2 is the type of a computation that
    -- takes us from state s1 to state s2 and produces
    -- a result of type a
    -- Phil notes: this is like a Hoare triple whose pre-
    -- and post-conditions are very narrowly defined: they
    -- are full characterizations of the pre- and post-
    -- states. Conor: also connected to Atkey's parameterised
    -- monads.

  get: (s: S) -> State s ((s': S) * s' = s) s
   -- get doesn't change the state and returns it
   -- ((s': S) * s' = s) is the singleton type `{s}'

  put: (s': S) -> (s: S) -> State s 1 s'
   -- put changes the state and returns unit

Ridiculous, though: in order to invoke get, you need to know the state
already! Something is very wrong. The missing thing is the idea of a ghost
variable. Or auxiliary variable. (FP notes: the quantification over s in the
type of get should be an erasable universal quantifier.) What we mean is:
whatever the state is known to be statically, the operation will dynamically
produce a value which is equal to this state. I'm saying that to you, but I
haven't written on the board: we are missing this static/dynamic distinction.

Another Conor quote: `it seems to me, John, that you are suffering from Milner
hypnosis'.

Dan Licata notes: when you do binary search in an array, with a precondition
that the element *is* (somewhere) in the array, if you interpret this
precondition in a strong constructive sense, then you already know where the
element is in the array, and you don't need to search.

(Flips the whiteboard.) Displays a set of typing rules: Martin-Lof type
theory. A type of types, a dependent function type, lambda, application, a
conversion rule up to some equational theory, a variable lookup rule.  Type :
Type. One could refine it in various ways to obtain, e.g., a PTS. Here, want
to consider this idea that `stuff belongs somewhere' (static, dynamic). The
typing judgement becomes indexed with a world. The `world where we make types'
is called star, e.g., the rule Type : Type is indexed with *. The function
type becomes (x :w S) -> T, and the environment contains assumptions of the
form (x :w S). At application, the function and its result should live in the
same world (FP: why?), but the argument can live in a different world. At
variable lookup, we allow `sub-worlding' (a pre-order on worlds). Analogy with
information flow analysis: types must not leak into runtime. (FP: yes, in both
cases, it's a matter of ensuring the absence of certain dependencies.) Of
course, we want `sub-worlding' to be admissible as a rule (not just hard-wired
in the variable rule). Clearly this works only if the world * is maximal,
because we can only make types in *.

(FP: this reminds me of Frédéric Prost's paper in LICS 2000.)

Oleg argues that cross-stage persistence seems to go the other way: if a value
exists at static time, then we make reference to it at runtime.

An erasure property would state that we can erase anything that lives in some
fixed, upper-closed set of worlds. (FP: essentially a statement of
noninterference.) E.g. in the earth/heaven distinction, dynamic/static,
we can erase the static things.

In Haskell, at the moment, we arrange to make copies at the type level of
things that exist at the term level. Conor suggests having Pi below earth
and heaven, which live side by side. This represents things that can live
in both places.

Phil: question about the connection with Bernardy's type theory in color.
A: Would like to transport things from one world to another.