brains splattered all over the walls
It’s nearly the new year, my lectures are all done, and the activities of War, Famine, Pestilence and Death in my daily life have settled down at least a bit. I wonder if I might find some of the discarded slops of my brain and scoop them back into my cranium, to see if they might restart. What was it that the person who used to be me used to think about? I hastily scribbled a list of things I think I think are worth thinking about, and as it got longer and longer, I got that thinking feeling. It occurred to me that maybe I should try to write just a little bit about where I’m at with some of them, as a way of examining the dependency relationships between them and planning some sort of strategy to address the mess.
Working through some of this stuff might also make it a bit clearer why I’m not in the mood for significant programming language design and implementation just now. I’m not promising that I’ll never be. I don’t want to make a bunch of short term decisions for the sake of ‘going live’ that I’m sure I’ll regret.
So, here’s the list that I scribbled, in the order in which I scribbled it (which is not a sensible order). I’ll try to give a one-line (of source, which seems to spill when rendered) summary of each.
variables live in worlds; terms are built in worlds; worlds are preordered, controlling information flow
breaks subject reduction in Coq; has only non-dependent case in Agda; needs a better equality to repair
an inductive datatype just gives the closed terms of a syntax with no binding; syntax should be primitive
- irish induction-recursion
my coding of IR functors is at least as rich as Dybjer and Setzer’s; they compose; too good to be true?
- dependent types for data modelling
types for spreadsheets or databases unless they’re relative to a model of the underlying data, so make that
let’s just treat Set as a datatype (ahem, a syntax) and get on with it; get parametricity from worlds
- universe hierarchies
cumulativity matters; universe polymorphism is overrated; no fixed hierarchy but morphisms between them
using core types for the presentation of elaboration problems, not just the semantics of their solutions
the equational theories of open terms can be generated more interestingly than by lifting closed computation
what are they? what’s their proof-relevant counterpart? is that enough higher-dimensional structure?
- OTT motivation delivery
before we abandon Observational Type Theory, we should at least try to remember what it was and did
would really enjoy an internal notion of computation, a closed universe of HITs, the fun I’m used to
- user interfaces in a darkened room
a functional model of the structure of applications, abstracting away from appearance/hardware
- traffic-dependent session types
the protocol for future communication depends not on the prior processes, just on their traffic
- linear dependent types
with a dependent lollipop, rather than the current both-present-but-never-the-twain state of the art
- theories of testing
testing can reveal the absence of bugs if you can bound the weirdness of the programs being tested
- differential structure and deep patterns
building search (what strategy?) into pattern matching by allowing plugging-into-contexts on the left
if we have sole ownership of data, we can mutate it, and maintain multiple access paths…consistently?
- local time for recursion and corecursion
use a temporal modality to demonstrate totality, but your client doesn’t care, so make sure it isn’t there
- internal parametricity
whatever I know about what I don’t know, I want a goddamn proof term which tells me that I know it
- re-engineering failed definitions
it’s all very well refining holes until you find out they’re the wrong holes; assisted head-scratching?
how do we work with ornaments in practice, both from the developer’s viewpoint and the compiler’s?
how to put reference implementations in a signature and choose better implementations in the structure
pure function application is just the least nontrivial way for one computation to contextualize another
There are probably more that I’ve forgotten. I wonder where to begin. I’d be rash to promise a ‘24 days of unfinished half-ideas’, but I might get further than nowhere.
EDIT: I omitted ν-rules from the original version, quite by accident.