Up to this point, I have attempted to give an overview of what substructural type systems are, in order to help establish a baseline understanding that I do not need to explain further. From here on out, I will attempt to explain my own vision for a programming language building upon this baseline.
Instead of trying to define my own syntax right now, which is incomplete anyway, I will instead begin by trying to explain the important concepts using Rust syntax. Rust has become relatively mainstream, and furthermore has C-style syntax, so I am hoping that this will help get to the essence of what I am trying to explain without needing to involve other complications. However, it is necessary to explain where I will be diverging from what is already in Rust:
Drop
trait, but this cannot replace the default destruction of
the structure of all types, nor can the latter be suppressed,
except for means that risk the resource being leaked.
My language would have one trait that defines whether
or not a linear type has a destructor that can be implicitly
called (which would make it affine). Types that do not
have such a destructor must be used explicitly.
To get around the exception unwinding problem, we will also
need some sort of Unwind
trait implemented by all types, which
would define a destructor-like
subroutine but only in the context of exception unwinding.
Unlike with real destructors, an unwind implementation
can abort the entire program if there is no safe way to
clean up or leak the resource - which is more palatable
given my separate opinion that exceptions should be reserved
for extreme situations.Unpin
marker trait
and the Pin
type. In my language, not all types are moveable.
In an actual Rust-like setting, this could work similarly to
?Sized
, where the Sized
trait is always referenced by default
and ?Sized
is used to mark situations where we want to go beyond
that.