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)

    After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…

  • (no subject)

    Thai curry leftovers for dinner. Got a copy of Hennessy and Patterson's textbook on Architecture, and I am enjoying catching up on all the low-level…

  • (no subject)

    Finally the end is in sight for unpacking my books. Heartstrings are pulled over the desire to slim down and get rid of some of them, but so many are…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded