Lang: Support non-garbage collected local data

[phated]

In Discord, @EduardoRFS suggested an implementation of local data that avoids garbage collection. This is possible at the type level because we don't support GADTs.

Here's his exact idea:

Another random proposal this one I think may be useful for the smart contract land, a simple way to avoid GC is to prevent value from escaping the scope through levels in the typer, this can easily be done if there is no GADT in the language by having something like the following. The infrastructure is already present in the typer.

record local Data { a: Number } 
let mut mut_variable = None
let f = (x) => {
  let a = x.a
  // this will fail because it will escape it's scope.
  mut_variable = Some(x)
  a
}
// the following is still allowed
let f = (x) => {
  let mut mut_variable = None
  let a = x.a
  // this will work as mut_variable level is bigger than x level
  mut_variable = Some(x)
  a
}

What are our thoughts about this?

[phated]

I personally really like this! It seems like Rust lifetimes but miserable to work with.

[EduardoRFS]

Just explaining the implementation, the idea is that on every parameter with a local type we introduce a type variable that, so local types are actually similar to a GADT pattern matching and it will introduce a local type.

So, x: Data can actually be seen as x: Data<$Ex_a>, this is hidden from the user

During unification, when an a is unified with Data it actually results in Data<$Ex_a> and this $Ex_a will be introduced in the same level that a was introduced and it cannot escape its scope anymore, any mutability case outside the scope will trigger an error and then we just need to detect that the variable that escaped was introduced by a local type and give a proper error message.

And after typing the function that introduces the parameter we ensure that the variable can be generalized, this needs to happen on every lambda, probably for grain is not a problem because lambdas are not that common.

Good thing about that is that we can do similar to affine types, and introduce a free automatically if you're not using the variable and for something like a smart contract that you don't need to collect memory, no operation is inserted.

The problem with GADTs is that this cannot easily be enforced during unification as a GADT can hide a type variable.

Theory

I don't know any theory to describe this feature, probably it constitutes affine types, but it's not directly exposed the control to the user, so it may be quite ergonomic.

But I believe(strongly) that assuming no parallelism this can definitely be done in a type safe manner with the implementation above.