logo

Austral Programming Language

Posted on: 2023-01-02

Conclusion

Overall I'm impressed - it seems simple, powerful and well thought through. I don't agree with all of the choices, but it's really helpful to be able to read the rationale to work out why the decision was made.

On thinking about linear types some more, it raises a variety of questions that are not answered by looking through the Austral standard library, documentation or examples.

Interesting

Good

Not sure

Bad

Ugly

Discussion

Has a platform dependent Index type. This seems like a good idea, although they have chosen it to be unsigned. Which might not be the right choice, for reasons not argued here.

It uses Nat for unsigned types. That actually works relatively well.

In order to have different operator behavior, it includes functions such as modularAdd. The default behavior is to abort on overflow. This requires runtime checking.

Out of bounds accesses to fixed arrays abort.

Has named arguments using => syntax.

Records are constructed via a ctor like syntax.

Has sum types through union.

Has a borrow mechanism, where a linear type, can be made a reference over a block. The region is used to limit that access. When accessed as a reference, the linear type cannot be accessed.

borrow buf as bufref in Reg do
    -- For the duration of this block, the value `buf` is
    -- unusable, since it has been borrowed, and `bufref`
    -- has type `&[ByteBuffer, Reg].
end borrow;

Uses & and &! to access a read or read/write reference.

The type “read reference to a value of type T” is denoted &[T, R], where R is the region, which we will discuss below. The type “mutable reference to a value of type T” is denoted &![T, R]

Dereferencing is performed via -> and !.

Generic parameters are specified using [] style. You have to specify the universe of type parameters either Linear or Free. If either is possible then we can use Type. Linear, Free, Type Region are Kinds. A kind being a type of a type in effect. (Seems like a limited form of higher-kinded types ).

Has return-type polymorphism - when used it's necessary to specify the return type to disambiguate.

A type class seems to be something like an interface.

Questions

Pointer example

In one of the examples there is an implementation of a Ptr that tracks allocation. The load/store methods can only take a type that is free. If that wasn't the case it would mean its possible to take a linear type and copy it (into the pointer target or out of it), which isn't allowed. When the object is freed it returns the contained type.

type Pointer<T: Type>: Linear;

generic <T: Type>
Pointer<T> allocate(T value)

generic <T: Type>
T deallocate(Pointer!<T> ptr)

generic <T: Free>
Pair<Pointer<T>, T> load(Pointer<T> ptr)

generic <T: Free>
Pointer<T> store(Pointer<T> ptr, T value)

Allocate, if T is linear then passing to the function must in effect be the same as consume. That makes sense linear types must be used once.

If load or store is used they must take a free type. That makes sense in so far as if that wasn't the case it would be possible to copy or overwrite a linear type, thus breaking the use once rule. What does this mean in practice though? Do these function not exist for linear types? Is it possible to overload for linear types?

Interestingly deallocate returns the contained value. This makes sense because if T is linear we need a way to use it. We cannot write a mechanism to not return T, because T doesn't have a dtor and so we have no way of the generic knowing how to use T.

Swap

If there was a swap, that might simplify some operations on linear types.

Container

Lets say we have an Array<T>. It is not possible to access an element to take ownership, without removing from the array. You could have a non owning reference to an element though.

Having swap might allow a way to access an element of the array without having to change ordering. If the element being accessed is being referenced then that could potentially be okay, although it introduces some issues

Array<T> array;
//...
doThing(@read T a, @own T b);

// If i == 1 we have a problem, as we would be aliasing the same item
// one via ownership and the other via reading, which wouldn't be allowed.
// 
// Also if the array is passed in if it is altered, it's backing memory may 
// change, and that could break things.
doThing(array[1], array[i]);

Also note at the end of the arrays scope a function would have to be called to free it.

Constructing/using Linear types

It not clear how Linear types work wrt to construction. Say I wanted to do

SomeType t;
if (someTest()) {
    t = makeSomeType();
}
destroySomeType(t)

If an assignment moves the linear type, then that consumes the makeSomeType result, but it also overwrites whats in t. It implies it's necessary to be able to construct a default T for this to work. It would additionally mean we should swap, to consume?

Or as another example take. A buffer can be allocated of Type - but if it's linear, how can it be constructed without constructing T[N]?

In the implementation of Standard.Buffer, the buffer appears to only be able to hold Free types. That makes sense, but not being able to have a dynamic array/buffer holding linear types seems like a problem.

Borrow

The borrow syntax seems to use a Region as a local named type to limit scope.

In the write up it appears as if a reference is always a pointer, but you could imagine in practice, when using a read reference, passing the value (if small) would be fine and more optimal.

Other

Doesn't appear to be defer. Does talk about Destructable(T) typeclass.

I'm not sure I entirely buy the argument around exceptions as it relates to error handling. You could have a type system that has destructors without exceptions. Errors could be returned via Option/Result and the program flow is explicit with try (or some destructuring/handling) required to call code that can fail.

If a contract violation could return an error, that does mean the failure return would have to apply to everything, which is problematic. That probably means assert can't return an error, if it fails it panics. If we have checks (for a testing system), perhaps it returns an error code with check. Often (say) in a unit test, we can continue if there is a check failure, so perhaps that isn't necessary.

I suppose there is some kind of "middle ground" around affine and linear types. A problem with linear types (as used here) is that you have to know to call a function that consumes the linear type. There is no "default" behavior, making it unclear how a container of linear types can work, without manually removing and consuming. You could though have dtors, but make their usage explicit.

So

Array[T] array;
array.add(thing); // say

// ...
// Implicitly destroys any contained things.
destroy array;

In this way it's not necessary to explicitly consume everything. Perhaps if a linear type contains a dtor then this can be used. Or perhaps we can mark the dtor if it can only be used explicitly or not.

The dtors double throw issue, is not an issue if we don't have exceptions. If the dtor returns void, we can't return an error.

Perhaps a dtor can be written such that it can return an error, and for that type it's dtor can't be automatically executed.

Throwing has this "interesting" idea of capturing linear types in the environment at the point of throwing and storing them in the exception. The problem there being - there can be different environments (live linear values). So the best you could have would be some structure that held a set of live linear types, which isn't super useful.

Links