Jason (jcreed) wrote,

That Martin Hoffmann paper I mentioned earlier is here:

In the back of my head I keep thinking about what it would mean to have these diamonds refer to permission-to-make-a-database-query or something like that. This would be a pretty big departure from the paper, since it has these tokens being consumed *and* generated (because they represent memory that can be reclaimed), and if you're keeping track of number of executions of some expensive piece of code, they'd just be consumed.

Something that came up during the conversation with gwillen was whether you could capture things that sounded like big-O statements about number of diamonds that had to be consumed. Barring real dependent types that let you say how big your data structures are, I don't really see how you'd do this. But if you allow them (and allow a suggestive notation for an n-ary tensor of diamonds) then the operation that takes the type A to the type


is pretty interesting. It's saying simply that there is some time-cost (or number-of-queries cost) you have to pay before you get an A. This sounds like a really weak claim, but there's a difference between the type

∃n.◇n ⊸ A list → B

and the type

A list → ∃n.◇n ⊸ B

The former knows how costly it is to get from an A list to a B, before you give it the A list. The latter only knows afterwards. So the former might be a type you could assign only to a sufficiently efficient function, e.g. one that knows how to batch up all the queries arising from the A list into one DB call.


In fact, weirdly, as modal logic, ∃n.◇n ⊸ --- seems to behave like (Pfenning-style, not Awodey-Bauer-style) proof irrelevance! It's not transitive, because knowing that there's some cost to find out what the cost to complete a project is is not the same as knowing the cost to complete a project. This feels like some Fred Brooks shit right here.
Tags: logic, math, types

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded