http://perso.ens-lyon.fr/patrick.baillot/ENSEIGNEMENT/CR04_2010/Hofmann_NSI_IC2003.pdf
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∃n.◇n⊸A
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.