Skip to content

brains splattered all over the walls

December 30, 2014

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.

  • worlds
    variables live in worlds; terms are built in worlds; worlds are preordered, controlling information flow
  • coinduction
    breaks subject reduction in Coq; has only non-dependent case in Agda; needs a better equality to repair
  • syntax-not-just-data
    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
  • reflection
    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
  • problems-as-types
    using core types for the presentation of elaboration problems, not just the semantics of their solutions
  • ν-rules
    the equational theories of open terms can be generated more interestingly than by lifting closed computation
  • quotients
    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
  • HoTT
    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
  • mutation
    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?
  • ornaments
    how do we work with ornaments in practice, both from the developer’s viewpoint and the compiler’s?
  • modularity
    how to put reference implementations in a signature and choose better implementations in the structure
  • effects-and-handlers
    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.

6 Comments leave one →
  1. January 3, 2015 9:04 am

    So, do you mean OTT is a dead idea? Why is it so, and do you have an alternative way in mind for getting observational equality?

    Also, is Epigram 2 completely dead now? Is it dead because the developers scattered or because it has crucial flaws? Is the source theoretically available for the public (more specifically, for me)?

  2. January 3, 2015 11:17 am

    OTT isn’t dead. Thorsten has rejected his own creation, but I haven’t. It isn’t HoTT, which means nobody wants it, even though we don’t know how to do HoTT properly yet. OTT is full of clues for how to make HoTT work, so whether it survives or not, it has been a useful lesson.

    Epigram 2 is completely dead. The developers scattered, and I got a job which makes it hard to maintain such a project. But it also suffered from my tendency to destroy anything I’ve had time to think about. Did it have flaws? Yes, lots. (Of course, I think the systems that other people have constructed would benefit from some rethinking, but still we benefit from the fact that they exist in their current state.) In many ways, this collection of topics is a bunch of stuff I’ve learned to worry about by working on Epigram 2. The thing that was Epigram 2 is a thing I’m sure I don’t want any more. I’m stumbling towards a new thing that I might want, but that’ll be a thing apart.

  3. molikto permalink
    January 3, 2015 1:29 pm

    we got computation rule for univalence and higher inductive types now. . although i think you must be aware of it

  4. molikto permalink
    January 3, 2015 1:31 pm

    “user interfaces in a darkened room” that’s something in my mind for a long time.

  5. January 5, 2015 10:17 pm

    molikto: More specific citation needed on that computation rule.

  6. mimblewabe permalink
    January 6, 2015 7:50 pm

    Robin Green:

    with the caveat that “While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky’s Univalence Axiom.”

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: