Snipped and backdated from a Reddit comment of mine.

There are a lot of interesting similarities here. I also found the original paper that the blog post was referencing: “First-class labels for extensible rows” with discussion on Lambda the Ultimate.

I didn’t as prominently show it in the example, but my examples use structural typing and union and intersection types (examples from my other comments).

It seems to me that what I’m suggesting effectively is the same as using row polymorphism as shown in the blog post. The example from the blog post again:

f :: {a: Number, b: Number | ρ} -> Number
let f x = x with {sum: x.a + x.b}
let answer = f {a: 1, b: 2, c: 100}

// "regular" structural typing
answer :: {a: Number, b: Number, sum: Number}

// row polymorphism
answer :: {a: Number, b: Number, c: Number, sum: Number}

And back to my made up syntax, the example above should be equivalent to the following:

f <'x> :: 'x: { a: Number, b: Number } -> 'x & { sum: Number } 
fn f(x) {
  x with { sum: x.a + x.b }
}

answer :: f('x) when 'x = { a: Number, b: Number, c: Number }
       :: { a: Number, b: Number, c: Number } & { sum: Number }
       :: { a: Number, b: Number, c: Number, sum: Number }
let answer = f { a: 1, b: 2, c: 100 }

To break the important line down:

f <'x> :: 'x: { a: Number, b: Number } -> 'x & { sum: Number } 

• <'x> declares the type variable 'x in the scope of the type definition

• the function take one parameter of type 'x: { a: Number, b: Number } (which essentially uses subtyping) to say that the type variable 'x needs to at least have the structure { a: Number, b: Number }.

• the function’s return type is 'x & { sum: Number } which says the return type must be whatever type variable 'x actually is and, in addition, must also have the structure { sum: Number }.