Add an inverse use block

[jimbxb]

Once a resource is in scope it is always in scope for the current block. Adding an inverse use block (disuse, name tentative) would allow you to have a block of code where a resource is unavailable inside, assuming it was previously in scope. This would allow you to ensure that you have not accidentally used a resource.

For example,

resource counter:int = 0

def foo use !io, counter {
    disuse counter {
        !println("can't use counter in here!")
    }
    !println(counter)
}

I'm unsure of how this would be handled in the case of higher order calls, as there's no way to ensure a higher order call doesn't use a resource. It could be a useful way of ensuring a resource isn't used inside a closure, too.

This could be extended to variables in general without much difference. Mode checking could simply place these variables/resources as out of scope inside this block.

[pschachte]

So this would essentially create a "hole" (or maybe "shadow" is a better metaphor) in the use of a resource. I'm not sure why this would be useful. Can you sketch an example of where you'd want it?

[PaulBone]

This was something I was proposing for Plasma, I was thinking about some supply chain and similar attacks that can happen when dependencies change. One day you have some code that's like:

A logging library provides this function, which uses the logging resource.

func writeLog(string) uses LogResource;

So you use it in your code:

func login(...) uses LogResource, PWDBResource {
   ...
   writeLog!("Login successful")
   ...
}

Note that the ! tells you that a resource is used in the writeLog call, but you can't tell from the caller what resources are used, you must look at the callee's declaration. Then someone changes the logging code, maybe it's library code that you're replying on and it changed maintainers and the new maintainer has different motivations. Now the declaration is:

func writeLog(string) uses LogResource, PWDBResource;

When you re-compile your application you're not aware that the logging code now has access to the password database. It can read and change passwords! But you never chose that because you hadn't read the updated declaration.

There's probably other ways to solve this, like checking changed declarations. Having a scope that white/black-lists particular resources is one way you can make it very clear in your code what's acceptable within the scope:

func login(...) uses LogResource, PWDBResource {
   ...
   scope uses LogResource {
      writeLog!("Login successful")
   }
   ...
}

Now an update to the library that adds additional resources will cause a compilation error. And you'll be asking "why would a logging framework need access to the password database?"

[pschachte]

That's an interesting example, Paul, not something I've thought about.

To use something like disuse for this purpose, you'd need each function that needs access to the PWDB to declare that it uses it, access it at the start of the definition, wrap disuse around the rest of the body, then wrap use around the calls that actually need to use it. It's easier and safer to just explicitly pass it to the bits of code that you want to have access to it.

[PaulBone]

So I imagine that you'd only use one of these scopes when you want to change what's implicitly available. if you don't use any scope then the same things are available to "capture". And the trap with resources is that they're captured less obviously than variables (eg in lambdas). My example above uses a whitelist of "these are the resources that should be available, everything else is denied".

I'm not sure if the example is all that motivating. It'd have to be a pretty targeted supply chain attack, but there may be other reasons to do this also.

[pschachte]

If you have some "sensitive" value that you don't want widely shared, you shouldn't put it in a resource. So the motivating example for a disuse statement would need to be a value that's not generally sensitive, but you don't want threaded through some particular piece of code.

You have a good point about resources being easily captured. Each proc that uses a resource controls what they have access to, but they don't control what resources are used by the procs they call, except that it must be a subset of the resources they have access to themselves. But if they want to, they can control that, too, by calling a proc they write themselves with a limited use list, and have that proc call the ones they want to restrict.

[jimbxb]

Interesting. That means that something like disuse is semantically equivalent to simpler constructs.

i.e.,

def foo use a, b {
    disuse b {
        !bar
    }
}

is equivalent to

def foo use a, b {
    !wrapped_bar
}

def wrapped_bar use !a {
    !bar
}

This would differ slightly when there are variables being bound in the block, but they can be passed in/out as additional parameters, as would the arguments of bar be.

I think there would be some merit to having this as a language feature, with a similar argument to wanting a lambda block, though a little bit weaker as I'd consider this less useful than a lambda.

[pschachte]

That's what I assumed the semantics of disuse would be.

I agree that disuse makes sense, except that we can't currently implement it (because of resources in HO code).

Can't you achieve the effect of lambda with code like let {?x=@; ?y=@; ?z=@} in ...?

[jimbxb]

Why couldn't we handle HO resources as we currently do, in that we can't stop a HO term from using a resource.

In essence, a HO term can always use it's in scope resources, even if the resource isn't in the current scope.

That would mean something like this is possible

def foo(f:{resource}() use !io {
    disuse io {
        !f
    }
}

!foo({resource}{ !print 123 })

This is inline with the current semantics of HO resources, as this is possible

def bar(f:{resource}() {
    !f
}

!bar({resource}{ !print 123 })

These procs, foo and bar are equivalent from what I believe the semantics should be.

---

I don't think let { ?x= @ } in ... supplants lambdas. Holes (@) are only allowed inside lambdas, some perhaps I'm misunderstanding your snippet.

[pschachte]

Why couldn't we handle HO resources as we currently do, in that we can't stop a HO term from using a resource.

In essence, a HO term can always use it's in scope resources, even if the resource isn't in the current scope.

We could, but this is a flaw, as it violates interface integrity. I'm hoping we can eventually add an analysis to check that HO code is using resources properly, without violating interface integrity, and report an error if not.

I don't think let { ?x= @ } in ... supplants lambdas. Holes (@) are only allowed inside lambdas, some perhaps I'm misunderstanding your snippet.

I think I'm just misunderstanding what you mean by "lambda". If code like map( {let {?x=@} in x*x}, list) is supported, that effectively acts just like a lambda in any functional language. Being able to write map( {@1 * @1}, list) is just icing on the cake.