Home

A better way to enforce pre & postconditions

This post assumes knowledge of linear types. If you'd like to learn them this is a good introduction.

I was browsing the austral discord. When Verdagon said:

Verdagon: hey! just had a bit of a revelation about linear types
Verdagon: linear types are great for enforcing preconditions and postconditions

What I believe he means here is that you can create an API like this.


type Array[T: Type]: Linear;

-- just a wrapper type around Array[T]
type SortedArray[T: Type]: Linear;

generic [T: Type]
function sort(arr: Array[T]): SortedArray[T];

generic [T: Type]
function binarySearch(arr: SortedArray[T], ...): Option[T];

Here there is no way to create a sorted array without calling sort() and therefore it is impossible to call binarySearch() with an unsorted array which would be a bug. Which has now been prevented at compile time.

I thought this was interesting and wanted to use it to create a file API. I decided I wanted to have the following ways to open a file.

Read
Write
ReadWrite
Append
ReadAppend

Any combinations with both Write and Append are not useful as write allows appending. The issue is we end up with the following API:


-- all of the types wrap this one
type FileInternal: Free;

type FileRead: Linear;
type FileWrite: Linear;
type FileReadWrite: Linear;
type FileAppend: Linear;
type FileReadAppend: Linear;

-- this isn't exposed in the interface but 
-- you should know it exists
typeclass FileWrapper[T: Type] is
    method getInternal(): FileInternal;
    method open(filename: String): T;
    -- arguably, close should be here but it doesn't need to be so???
end;
instance FileWrapper(FileRead);
instance FileWrapper(FileWrite);
instance FileWrapper(FileReadWrite);
instance FileWrapper(FileAppend);
instance FileWrapper(FileReadAppend);

-- no methods
typeclass FileReadable[T: Type(FileWrapper)] is end;
instance FileReadable(FileRead);
instance FileReadable(FileReadWrite);
instance FileReadable(FileReadAppend);
-- no methods
typeclass FileWriteable[T: Type(FileWrapper)] is end;
instance FileWriteable(FileWrite);
instance FileWriteable(FileReadWrite);
-- no methods
typeclass FileAppendable[T: Type(FileWrapper)] is end;
instance FileAppendable(FileWrite);
instance FileAppendable(FileReadWrite);
instance FileAppendable(FileAppend);
instance FileAppendable(FileReadAppend);

generic [T: Type(FileReadable), R: Region]
function read(file: &[T, R], length: Index): String;

generic [T: Type(FileWriteable), R: Region]
function write(file: &[T, R], bytes: String): Unit;

generic [T: Type(FileAppendable), R: Region]
function append(file: &[T, R], bytes: String): Unit;

generic [T: Type(FileWrapper)]
function close(file: T): Unit;

This is not a fun API to write. Using it isn't too bad but it's far from ideal. Additionally, this pretty simple file API has many instances that take up lots of code and many methods would have nearly identical internals.

Now many functions that use files have to awkwardly ask for a generic with the features that it uses rather than one File type.

Solution?: Type properties

This is a novel idea (I think?). All syntax after this point is poorly defined. Imagine a type like the following:


record File: Linear has
    Readable: Yes or No;
    EditMode: Write or Append or None;
is
    -- some internal stuff
end;

function open(filename: String, r: File#Readable, w: File#EditMode): File(r, w);

generic [F: File(Readable is Yes), R: Region]
function read(file: &[F, R], length: Index): String;

generic [F: File(EditMode is Write), R: Region]
function write(file: &[F, R], bytes: String): Unit;

generic [F: File(EditMode is Write or Append), R: Region]
function append(file: &[F, R], bytes: String): Unit;

function close(file: File): Unit;

The idea here is that type properties can be solved at compile time. Additionally, I believe that this can be done with a decidable type system. This can? be implemented in other languages at compile time as well, like in C++ but it abuses the type systems capablities.

This even handles branching to an extent:


-- API:
record Example: Linear has
    Prop1: A or B;
    Prop2: A or B;
is
    -- irrelevant
end;

function create(): Example(A, A);
-- the syntax for writeable borrow is poorly/undefined as of now
generic [R: Region]
function setProp1ToB(e: &![Example(Prop1 to B), R]): Unit;

-- doesn't depend on Prop1 so it can be used when Prop2
-- is ambiguous
function consume(e: Example(Prop2 is A)): Unit;



-- Use/Example:
let e: Example := create();
if randomBool() then
    setProp1ToB(&!e)
end if;
-- here on out Prop1 could be A or B
consume(e);
-- compiles

Basically, if a property is ambiguous (may have changed). the variable can still be used if the functions used afterward don't require that property to be defined or any values that it may hold are allowed. For example, if a type allows A or B or C or D and we know the function accepts A or B or C and it is ambiguous between B or C that would be valid. In this case, that a property is ambiguous when its information is needed, the compiler would throw an error.

I think that this type-state programming is quite a useful idea for preventing bugs at compile time. In fact linear types are arguably syntatic sugar over this type of restriction, where at the end of a linear type's scope a function call that expects its linearity property to be Consumed at the end of scope, and where all functions that take it as input take it as input but with the restriction that it is Unconsumed.

This could prevent whole classes of bugs, similar to how linear types can prevent write after close or double close. While linear types can in theory do all of the things these type properties do (without the ambiguoity handling), however this creates many typeclasses and types that aren't needed. For instance, the SortedArray example from the beginning would require SortedArray to have all the methods that Array does.

I'd like to thank Verdagon and Fernando Borretti for giving feedback on draft versions of this post.