Decide on linear typing/uniqueness types design

[snordgren]

Approaches to resource-aware functional programming

Shared values; kinded-lite

All values except those

frugal : & a -> & (& a, & a)
frugal x =
  (x, x)

type Int = 
  & BuiltInInt

Shared values can be defined using the & wrapper type. These values must be immutable. A function which uses only shared values can be safely shared, even as a partially applied closure. This has some interactions with field access which requires special care in the compiler, accessing a field on a & value should return the field as & too.

Values are implicitly converted to their &-form when passed. Only lambdas that take only & values as parameters can be implicitly converted to &; only tuples whose components are all shared can be shared. Shared enums only provide shared access to their fields, except for function members, which can only be accessed * at all * if their parameters are all shared.

One solution to this issue is to decide that functions cannot be invoked if they are placed in & and have their own wrapper named something like Pure to show that the function does not reference any mutable state and can be safely invoked multiple times.

Another possible design is that functions in & cannot be invoked at all. You'd have to implement callbacks as functions that return a new function every time they are invoked. a -> IO b would have to be implemented as type Callback m a b = a -> m (b, Callback m a b).

Top-level definitions would be implicitly converted to their borrowed counterparts just like some variables, which has implications on type inference. Requiring borrowing to be explicit with a keyword share would make it easier to write very efficient, resource-aware code, but would also break as top-level definitions are referenced multiple times in one function. You could fix this by requiring that top-level definitions are referenced only once, or by interpreting top-level definitions as "macros" that you mentally inline when they are referenced, lambda-calculus style.

Unique kind

Some types belong to a unique kind, some belong to the regular kind of types. This means that we have to abstract over the type of kind at some points, which might make it difficult to comply with the limitations of the unique kind. And abstracting over kind isn't something I'm too happy about doing.

Linear arrows

This is what Haskell uses. A linear arrow a -* b does not require that a is unique, it only requires that a is only used once in the body of the function. This has some disadvantages when it comes to implementation, because it is harder to implement record updates as mutation, because the individual function does not know whether its parameter is

Another weakness of the arrow-based approach is that it's hard to determine the potential linearity of returned values. You might want to return a unique point from a function Int -> Point, while a -> (a, a) should be an immutable value.

Two kinds of arrows, all returned values must be unique

This is another approach, in some ways a dual to linear arrows: all returned values are unique. -o functions only take unique arguments and only use them once. All values are unique except those taken as parameters in -> functions, and those values cannot be returned because -> functions also have unique returns. Values can go from unique to shared by being passed to a -> function.

This approach has the issue of deciding what happens to a value after being passed to a -> function. The unique reference to the value has been lost, which is problematic when dealing with things like file handles which should be unique at all times. One way to fix this is to only allow some types to be passed to -> functions. Another is to allow mutable access to a value that is borrowed in the same expression, as long as the mutable access happens after the immutable access.

One downside to this approach is that all types, even integers, need to be explicitly dropped. This can be fixed by adding a "magic method" forget, that, when defined, is automatically inserted. For most types this value should be an alias for drop, effectively degrading types with forget to affine.

share : forall a . a -> (forall b . a -> b) -> b
share a f = 
  f a

illegal : a -* (forall b . a -> b) -> b
illegal a = 
  drop (share a) a

To avoid use-after-free in the above, add the following restriction: a partially applied -> may not be unique. There is no way to copy a function, so it is not possible to from non-unique closure to unique closure. Another necessary restriction is that you can't reference a unique value in the body of a -> function. illlegal is illegal because share a is non-unique but drop requires a unique argument.

So this option becomes "every return is unique except a partially applied ->", so you sacrifice some consistency for ergonomics.

Uniqueness kinds

Use three kinds to support uniqueness typing: T (base type, e.g. Int, String), U (uniqueness attribute unique, non-unique), and * (the inhabited of the three, meaning it has values, and requires a T and a U).

You might want to abstract over usage.

If you pass a unique value to const, you can only use that value once. If you pass a non-unique value to const, you may use the value as often as you want to.

const :: u : a -> u : (b -> a)

Here, u is a type of kind uniqueness attribute, that is shared by the input and the returned function. This makes sense but I want to be able to share values freely before de-allocating them, and I don't want to force all their usage to be inside a closure.

Below notation is courtesy of edsko.net, with ω: swapped to & for typability. One could also remove the 1: and let uniqueness be the default.

drop :: 1:a -> 1:b -> 1:a -- magic

share :: &a -> &(&a -> 1:b) -> 1:b
share a f = f a

illegal :: 1:a -> &(&a -> 1:b) -> 1:b
illegal a = 
  drop (share a) a

-> takes and returns shared, -* takes and returns unique

Any function which takes a unique argument must return a unique result. A partially applied -> is never unique, which prevents illegal from being valid. drop necessarily takes two unique arguments. A -> cannot reference unique values and cannot invoke a -* passed as an argument, a -* can reference non-unique values. This enforces a certain ordering, where -> must come before -*.

If value constructors always return unique values, we get the useful distinction that -> can never allocate memory, on the other hand that severely limits the usefulness of -> to only accessing the values in its arguments.

Managing stack-allocated values like Int: a function copy : forall a . Copy a => a -> () -* a, that the compiler automatically inserts. (+) receives the type Int -* Int -* Int and the compiler automatically inserts copy invocations.

Other approaches

Granule, have a look at that.

Conclusions

As of right now, I think this design space is full of unwanted tradeoffs, which I suppose is why this design has never taken off in any other programming language apart from Rust.