Add `this` and `infer` members to tuples

[kontheocharis]

Consider a tuple

bing : (foo: str, bar: i32)

Even though it contains a str, bing cannot be used as one without .foo.
However, it is sometimes desirable to allow a tuple to be used as one of its members, without having to add the explicit access.
This could be done with the addition of a new parameter modifier this. Initially this could be implemented as an attribute #this on parameters. When this is present on a parameter list q : (this X, ...Y), it means that q can be used in place of something expecting X.

Additionally, a second modifier infer could be added which infers the requested parameter from context (or at least attempting to) when the tuple is created. Similarly this can be also done through an attribute #infer. In some ways, infer is the inverse of this: this is relevant for tuple destruction (on field access, ignoring the other fields), while infer is relevant for tuple construction (inferring the other fields). It is useful when you have a x: X and need to fulfil the type (this X, infer Y): instead of providing (x, get_y_somehow()) you could provide x and expect that due to the presence of infer, get_y_somehow() will be inferred. Of course, the inference is a best-effort, and if it fails the compiler will request the parameter to be added manually.

Why is any of this needed or useful? See the use cases below.

Use cases

Struct inheritance

Animal := struct (age: Age)

Cat := struct (this Animal, meow: Sound) // could also write (this animal: Animal, ..)
c := Cat(..)
c.meow : Sound 
c.age : Age

alloc_animal := (a: Animal) => {..}

// Both valid
alloc_animal(c)
alloc_animal(c.0)

Constraints

Consider an extension of the syntax where P where Q means (this P, infer Q). This can be used to write constraints, with Q being inferred from context if possible.

AsType <bool> ((b) => type b ~ true)

arcsin : (x: f32) where { x in -1..1 } -> (r: f32) where { r in (-PI/2)..(PI/2) } 
       = (x) => { ... }

bing := (x: f32) => {
  if x in -1..1 {
    // implicitly exists:  _p: {x in -1..1}

    print(arcsin(x)) // desugared/inferred to print(arcsin((x, _p)))
  }
}

Traits

The expression (T: Type) where Foo<T>, where Foo is a struct with a type parameter, can be used to write generics with trait bounds, where Foo represents a trait.

Iterator := struct <I, T> (
  next: &mut I -> Option<T>
)

VecIter := struct <T> (
  data: &mut Vec<T>,
  current_index: usize
)

vec_iter_iterator := <T> => Iterator <VecIter<T>, T> (
  next = (v) => {
    if v.current_index == len(v.data) {
      None
    } else {
      result := v.data[v.current_index];
      v.current_index += 1;
      Some(result)
    }
  }
)

collect_nodes := <I where Iterator<I, Node>> => (nodes: I) -> NodeCollection => {
  ...
}


build_ast := () => {
  node_vec := vec()
  // .. build the ast
  
  nodes := collect_nodes(iter(node_vec)) 
  // desugared to: 
  nodes := collect_nodes<(VecIter<Node>, vec_iter_iterator<Node>)>(iter(node_vec))

  pass_to_next_stage(nodes)
}

[feds01]

I think this is a good idea, it’s definitely useful for alot of cases, especially with kind of mimicking inheritance with the Cat and Animal example.

[feds01]

The constraint part with infer is also interesting, I think this will be something that will take to sometime to implement before all the other things we have to do 😅

[kontheocharis]

The actual proof generation of the constraints is no easy feat, indeed. For example

AsType <bool> ((b) => type b ~ true)

arcsin : (x: f32) where { x in -1..1 } -> (r: f32) where { r in (-PI/2)..(PI/2) } 
       = (x) => { ... }

bing := (x: f32) => {
  if x < 0.5 && x > 0 {
    // implicitly exists:  _p: {x < 0.5 && x > 0}
    print(arcsin(x))
  }
}

The call to arcsin(x) generates a proof obligation of Ctx -> (x in -1..1), where Ctx : (..., _p: {x < 0.5 && x > 0}). So basically there must be a process which can analyse boolean functions over specific domains such as float arithmetic in this case, and be able to conclude a result such as x in -1..1.

This is called refinement types in the literature, basically having some base type B, as well as some property P: B -> Prop, which defines the subset { x : B | P(x) }, and then being able to use it in place of another subset { x : B | Q(x) } where Q: B -> Prop. This is done by trying to satisfy forall (x : B) . P(x) -> Q(x).

If P and Q are sufficiently simple this can be fed through an SMT solver such as z3 which will output sat or unsat or that it doesn't know. If it doesn't know, there should be a way to prove forall (x : B) . P(x) -> Q(x) in the language. In Hash would correspond to providing a function (x: B) -> P(x) -> Q(x) where P, Q: B -> Type.

In the example above, B = f32, P = (x: f32) => type {x < 0.5 && x > 0}, Q = (x: f32) => type {x in -1..1}, and we can see intuitively that P(x) implies Q(x) for all x: f32. z3 would be able to take care of this easily, since it also supports floating point and machine integer theories.

All that being said, the infer stuff can be added before all the solving is implemented, and some simple constraints can be satisfied easily. For example, if you have a constraint (x: f32) where {x > 0} and you are trying to pass in 3, there will be a produced proof obligation 3 > 0 which will be CTEd to true, at which point as_type(true) = true ~ true is trivially refl(true). So for these cases (or where you explicitly check/assert the where clause before the invocation), there is no need for fancy SMT reasoning. This is also the case for the example in the issue description, because _p: x in -1..1 already exists in the context so no extra work is needed.

[feds01]

I particularly like the example where you can do something like:

Animal := struct(
   age: f32,
);

Cat := struct(
  #this animal: Animal,
  ...
);

animal_age := (animal: Animal) -> f32 {
   ...
}

// Perhaps you could even allow:
impl Animal {
  age(&self) -> f32 { ... }
}

main := () => { 
    wasabi := Cat(...);
    print(f"{animal_age(wasabi)}");

    // Perhaps this involves a lot of resolution though...
    print(f"{wasabi.age()}"); 
}

It can allow for some places to avoid dynamic dispatch by simply using #this feature to share common logic or interfaces between different entities.

[feds01]

In terms of syntax, I think these two features should be kept as directives since they allow you to augment some of the properties of the code that you write, I think we shouldn't introduce too much syntax for this kind of thing.

[feds01]

Interestingly, would something like:

Engine := struct(...)

V8Engine := struct(
   #this: engine,
   ...
)

Car := struct(
     #this engine: V8Engine,
)

engine_horse_power(engine: &Engine) -> f64 {
    ...
}

main := () => {
   car := Car(...);
   print(f"{engine_horse_power(&car)}");
}

Here, you see that #this has a dependency Car -> V8Engine -> Engine, or would it only allow a single this operation? Also, would this allow for multiple #this annotations?

[kontheocharis]

Interestingly, this can be used to emulate impl blocks as well.

Consider:

Animal := (
    this struct(age: f32),
    get_age := (a: Animal) => a.age
)

a := Animal(age=3)
Animal.get_age(a) // maybe a.get_age() for sugar

Indeed, tuples and mod blocks have no real difference other than syntax (and mod blocks have more lenient out-of-order referencing rules but this can be extended to tuples as well..).
So perhaps the following syntax

// (1)
Animal := struct(age: f32)

impl Animal {
    get_age := (a: Animal) => a.age
}

could be more or less sugar for

// (2)
Animal := (
    this struct(age: f32),
    get_age := (a: Animal) => a.age
)
// or equivalently with `where`:
Animal := struct(age: f32) where (
    get_age := (a: Animal) => a.age
)

That being said, I am a proponent for simplicity and I think that just having syntax (2) is enough, if out of order tuple referencing is a thing.

[kontheocharis]

Here, you see that #this has a dependency Car -> V8Engine -> Engine, or would it only allow a single this operation?

this would be transient, so Car can be used both as a V8Engine and Engine.

Also, would this allow for multiple #this annotations?

It is possible, if two types are distinctly different. I think to begin with it can be limited to a single field per tuple though

[kontheocharis]

In terms of syntax, I think these two features should be kept as directives since they allow you to augment some of the properties of the code that you write, I think we shouldn't introduce too much syntax for this kind of thing.

Sure, I think they can be attributes, but I also think eventually we should consider making them keywords if they become quite central for all of these patterns..