[p-dev] Resources and higher-order calls

[Paul Bone]

I'm now about to implement these features so I wanted to revisit what I
thought of them earlier.  To recap, the problem is the polymorphism of
resource usage in higher order code.  The concerns are that if you require
people to declare resources (even polymorphically) for higher order code
then they may write non-resourceful code (because that's easy) and later
find that they can't use it with resources (or a library they want to use
won't work).  Or if you allow implicit resources then you get double
standards for higher-order code: an extra set of rules and looser semantics.

So.  I'll comment inline on what my current thoughts and ideas are.  However
I think I'll also begin by implementing a reasonably conservative decision,
and seeing what it's like to use in practice.

Peter, have you thought of anything new since we last spoke?


On Fri, Sep 01, 2017 at 11:53:20PM +1000, Paul Bone wrote:
>
> Implicit resources
> ------------------
> 
> Peter feels that developers that don't imagine their code being used with
> resources simply wont write the resource declarations or ! on the calls.  I
> agree.  Peter continues by saying that therefore the resource unaware code
> should work with resources anyway, but the ordering of how the resource is
> used is either undefined or defined in a possibly not-obvious way.  So
> developers wouldn't have to use ! or say "uses r" and yet their code would
> handle resources implicitly.  I'm leaning towards "no".

This is still a "no", it's a fairly firm "no".  However see my new idea below..

> Evaluation order
> ----------------
> 
> Another idea is that just as statements have the declarative semantics of
> being executed one at a time, top to bottom, but that this is not
> necessarily their operational semantics, that expressions could have a
> similar declarative semantics.  And therefore you could have multiple uses
> of a single resource in a single statement, it'd be difficult to read and
> maybe your linter will give you a cleanliness warning, but it would be well
> defined.

I don't think this is necessary.

> Force developers to deal with resources explicitly
> --------------------------------------------------
> 
> In combination with this idea, we could also require that every higher order
> value has a "uses" or "observes" clause attached.  This defeats the YAGNI
> problem you mentioned
> (https://en.wikipedia.org/wiki/You_aren%27t_gonna_need_it taken to its
> logical conclusion people will never put in resource declarations until
> needed, but that need might arrise much later when you're using a 3rd party
> library).  However it may have the problem of turning people away from
> higher order code, or Plasma/Wybe.
> 
> We could take this idea further and suggest that a higher order value must
> always have a "uses", "observes" or "pure" annotation.  So the developer
> is always forced to think about it.  Then if they wish to omit the !
> symbols, they can say:
> 
>     func map(f : a -> b pure, l : List(a)) -> List(b) {
>         return switch (l) {
>             case [] -> []
>             case [x | xs] -> [f(x) | map(f, xs)]
>         }
>     }
> 
> The difference is it's not that they "forgot" to add a polymorphic resource,
> this changes it to a choice.  So it still suffers from the YAGNI problem,
> people will just say "pure" all the time, but a lot more code will be
> succinct.

I'd like to refine this proposal as a new proposal.

All higher order types can either have no resource annotation, or any number
of uses / observes, or exactly one of either pure or nondet.

  pure / no annotation: These are the same in semantics, the function does
                        not use or observe any resources.  A linter will
                        give a warning for code that is exported from a
                        module and doesn't have a resource annotation on any
                        higher order value, pure (or something else) should
                        be written to make the developer's choice clear.

  uses / observes:      The same as before.

  nondet:               Any resources can be used in any order-independent
                        way, including in parallel (or maybe add another
                        annotation for that).  The resource itself doesn't
                        need to be named.  However it will be treated by the
                        compiler as a resource variable.

So map would be:

    func map(f : a -> b nondet, l : List(a)) -> List(b) nondet {
        return match (l) {
            [] -> []
            [x | xs] -> [f(x) | map(f, xs)]
        }
    }

Note that nondet is on the higher order argument, and on map itself.  The
compiler will not guarantee the order of resource usage, and the resource
using functions do not need ! (unless another resource is also used).

A caller looks like:

    new_list = map!(my_function, list)

It does need the bang, and the resource used by my_function will match the
one used by map.  The recursive call to map (in map) does _not_ need the
bang because from its perspective this is a nondet resource.

If code does not call the higher order function, then it does not need the
nondet attached to it:

    func length(unused : a -> b nondet, l : List(x)) -> Int {
        return match (l) {
            [] -> 0
            [_ | xs] -> 1 + length(unused, xs)
        }
    }



> Placement of !
> --------------
> 
> There are two other ideas I discussed Peter and others recently.
> 
> The ! referring to an affect could be written before the statement as a
> whole, out-dented from the current block:
> 
>     x = calc_something()
>   ! do_something(x)
>     y = calc_something_else()
>   ! ok = do_something_with_result(x, y)
> 
> But in our map example this is far away from the actual effects.
> 
>     func map(f : a -> b uses r, l : List(a)) -> List(b) uses r {
>       ! return switch (l) {
>             case [] -> []
>             case [x | xs] -> [f(x) | map(f, xs)]
>         }
>     }
> 
> There's only one per statement and it still means "there's something to be
> aware of here".

I'm still not really okay with this.

> Placement of uses/observes
> --------------------------
> 
> The other idea is that the uses/observes clause should be moved closer to
> the 'arrow'.
> 
>     func map(f: (a) uses r -> b, l : List(a)) uses r -> List(a)
> 
> It doesn't 'look' right yet, but I think this helps.  This also helps when a
> function returns a function.

I haven't added support for resources here yet. but my syntax for function
types uses the "func" keyword.  So func(a) -> (b).  A current limitation is
that b must be in parens, but I will lift this later.

Yeah, there's some benefit to put the resource declaration in front of the
arrow...


> Higher-order and structures
> ---------------------------
> 
> One thing we didn't discuss is what happens when I higher order value is
> stored into a data type.  What does that data type's signature look like.
> 
>     data Foo = Foo (f : Int -> Int uses R)
> 
> If it's polymorphic then you have to write the type arguments on the LHS:
> 
>     data Foo(a, b) = Foo (f : a -> b uses R)
> 
> But what if its resource polymorphic.
> 
>     data Foo(a, b) with r = Foo (f : a -> b uses r)
> 
> That is probably required to make something sound, but I'm not sure.  If we
> adopt one of the ideas above, for example that all higher order calls
> implicitly use a polymorphic resource (resource-agnostic code is implicitly
> resource-safe).  That what implicit types happen when you put a
> resource-agnostic higher order value in a data structure?  Or is it just
> always pure in this context if you don't write a resource?

First, I've decided on the less haskell-ish syntax (we don't need so much
partial application, and instead this last one is:

    data Foo(a, b) with r = Foo (f : func(a) uses r -> b)

It will be illegal to put a nondet function into a structure.  That's more
or less a placeholder for something with an abstract resource anyway, so
maybe it should be cast that way.


-- 
Paul Bone
http://paul.bone.id.au