Lambda the Ultimate

...linear proof irrelevance shows up all over the place in systems aimed at practical use: ATS, Fstar, alias types, typestate systems, and the calculus of capabilities all have some version of linear proof irrelevance.

In this regard, our contribution is realizing that since lots of people have had this idea, it's worth formalizing as an independent concept. :)

Oops, I misinterpreted what was going on with this technique.

I've been hoping for a system that would unify dependent typing with a more resource-conscious model. If type information is a resource available at compile time, then since types depend on type information, types must depend on resources. Linear logic encourages a certain interpretation of "resource," but I haven't seen a system where a type can depend on a linear variable.

As I went casually through this paper, I think in my wishful thinking, I misunderstood the [A] syntax to mean "Linear variables can be abused in here because this expression is strictly hypothetical." I misinterpreted [e |-> X] as an intuitionistic term with a linear subterm e, and it's actually the opposite of that.

...linear proof irrelevance shows up all over the place in systems aimed at practical use: ATS, Fstar, alias types, typestate systems, and the calculus of capabilities all have some version of linear proof irrelevance.

Thanks a lot for the list. I did read the part about ATS in your paper, but in my misinterpretation, I didn't make the connection.

see Concurrent Clean re: uniqueness types documentation. too bad it is dead. (the ide it came with was pretty sad, anyway, in my limited experience.)

Both Fstar and Spiwack's Dependent L permit restricted forms of what you want.

Awesome! I'll go have a look at some point.

For reasons which are presently unclear to me, both of these setups seem to rely upon the evaluation order being explicit.

I'm obviously more than a little overeager to say ill-informed things about this stuff, but I'll say that makes sense to me. If the evaluation order is sequentialized, then we essentially have an implicit conduit for carrying linear resources through the steps of evaluation, and this conduit can be the store-passing basis for some imperative side effects. For instance, we can have operators that take an in-out linear variable and do anything to it, since any two in-out variable occurrences have a deterministic ordering. To restore referential transparency, it might be useful to design the syntax so the only in-out variables are for things that leave the linear resource alone anyway, merely siphoning off some information about its current state.

If I want to be able to treat information itself as a resource, even this siphoning is a form of impurity for me. I like the idea of siphoning only for proof-irrelevant purposes, i.e. at a time when the siphoned information's existence is still merely hypothetical. Sounds like I should look at Fstar and Dependent L.

Speaking of evaluation order, the paper contains this:

If we had given a general fixpoint operator fix x. e, even with an irrelevant termination metric, then looping computations would be definable. (This is connected to the ability of intersection types to detect evaluation order.)

This paper taught me some things about intersection types already, but how do they detect evaluation order?

To restore referential transparency, it might be useful to design the syntax so the only in-out variables are for things that leave the linear resource alone anyway, merely siphoning off some information about its current state.

I've realized I don't know why evaluation order would matter here after all.

Evaluation order matters for the more impure version of what I was talking about. However, if a variable is never imperatively re-bound, then all its occurrences do indeed refer to an unambiguous moment in the linear resource's history even without the help of evaluation order.

Both Fstar and Spiwack's Dependent L permit restricted forms of what you want.

I looked into these a little this past week, and I'll probably come back to them. Fstar in particular looks like just what I was asking for.

I'm still figuring out the kind of information control I'm looking for. After I looked into Fstar, my exploration wandered into bunched typing and hybrid logic. I've started implementation of something that combines multiplicative linear logic and hybrid logic. I shouldn't make any claims yet, but it seems to be clear sailing for now. :)