Restore late-binding for constraints within typealiases

[bioball]

This is one proposal to fix https://github.com/apple/pkl/issues/446.

This changes the behavior of typealiases such that:

• If the current frame's receiver is amending the typealias's declared module, set the constraint to the current receiver.
• Otherwise, set it to either the receiver of a qualified type declaration, or the typealias's enclosing receiver.

This implies that the meaning of a typealias can change depending on where it is resolved from. Given the following:

// module1.pkl
typealias MyTypeAlias = Any(isValid)

isValid = false

// module2.pkl
amends "module1.pkl"

isValid = true

These two properties have different type checks:

import "module1.pkl"
import "module2.pkl"

propA: module1.MyTypeAlias // always fails
propB: module2.MyTypeAlias // always passes

Despite this, they are considered the same typealias.

import "module1.pkl"
import "module2.pkl"

res = module1.MyTypeAlias == module2.MyTypeAlias // true

This is somewhat quirky. An alternative solution to this problem is to require any references from a constraint to be const. This is just like how classes work. However, this solution would limit the usefulness of typealiases.

[stackoverflow]

Late-bound typealiases are useful, but they also make for harder to understand code (you can't just follow the typealias to understand the type). This would be a breaking change, but I think forcing them to be const, like classes, is a more principled approach, while also solving the equality problem.

[holzensp]

I've been thinking about equality of types (and especially of typealiases). As with classes, the equality of lambdas is by source location of definition (let's call that "locational equality");

facts {
  ["equalities"] {
    local f = (it) -> it
    f != (it) -> it   // same function, but not equal, because undecidable
    f == f            // same function, same definition site, so equal
    local g = f
    f == g            // after resolution, still same definition site, so equal
  }
}

This is an imperfect equality operator, but it's an understandable concession to the fact that you can't generally decide functional equality. There are easy intuitions to this, because it only has false negatives (as in facts["equalities"][0]). You could say the implementation of == for functions (and therefore typealiases) is a strict subset of an "ideal" equality definition.

The problem with late-bound constraints in typealiases, is that they introduce false positives for their equality (case in point: module1.MyTypeAlias == module2.MyTypeAlias).

I've been thinking; what if we can keep == a strict subset of ideal equality, but grow it to include equality on amendable constraints in typealiases?

Lets define == of typealiases as dependent on the constituent parts (types, including their type constraints). When our operands are not locationally equal, we still conclude false, but when they are, we inspect them further. Formally, you'd define the equality with rules, such as:

• unions: A|B == X|Y iff A == X && B == Y
• constraints: A(f, g) == X(v, w) iff A == X && f == v && g == w
• functions: ((a) -> b) == ((x) -> y) iff a == x && b == y
• ...

However, since we already know our operands have the same definition, they're structurally equal (so a==x in the above function equality is a given, for example). We only want to know whether any module members inside the type constraints have been amended. In other words, given typealiases P and Q, we say that P == Q iff both:

• P and Q are locationally equal; and
• for every late-bound member p_i in P and the structurally corresponding member q_i in Q, p_i == q_i

This does require that sometimes _|_ == _|_ (where _|_ denotes undefinedness, such as a declared property that has never been given a value), but I propose that locational equality for _|_ is enough. Basically, we substitute the source location of the undefined thing, so if on line 5 of mymod.pkl there's a foo: Any that gets evaluated, we say it evaluates to _|_(mymod.pkl:5:1).

Very concretely, in terms of your example, I'm proposing the following evaluation:

  module1.MyTypeAlias == module2.MyTypeAlias
    => Any(module1.isValid) == Any(module2.isValid)
    => module1.isValid == module2.isValid
    => false == true
    => false

and even if we change module1.pkl to be

typealias MyTypeAlias = Any(isValid)

isValid: Boolean

we get

  module1.MyTypeAlias == module2.MyTypeAlias
    => Any(module1.isValid) == Any(module2.isValid)
    => module1.isValid == module2.isValid
    => _|_(module1.pkl:3:1) == true
    => false

However, if we also remove the overwrite of isValid in module2, we get

  module1.MyTypeAlias == module2.MyTypeAlias
    => Any(module1.isValid) == Any(module2.isValid)
    => module1.isValid == module2.isValid
    => _|_(module1.pkl:3:1) == _|_(module1.pkl:3:1)
    => true

The cost of this equality operation grows linearly with number of late-bound members in the type constraint of the typealias.

... and for folks who rely on the current locational equality of typealiases for anything, they can use pkl:reflect to still resolve the location of the definition and compare that.

[holzensp]

And, for context, a few observations about lambda equality currently:

amends "pkl:test"

local class Given {
  // Notice late-bound `value`:
  func: (Any) -> Boolean = (it) -> value == it
  value: Any
  unrelated: Any = null
  otherFunc: (Any) -> Any = (it) -> it
}

facts {
  local a = new Given {}
  local b = (a) {}
  ["unamended, lambdas in objects are equal"] {
    a.func == a.func
    a.func == b.func
  }

  local c = (a) { unrelated = 1337 }
  local d = (a) { value = 5 }
  ["amending anything loses lambda-equality for all lambdas"] {
    a.func != c.func
    a.func != d.func
    a.otherFunc != c.otherFunc // even independent lambdas
  }

  local e = (a) { value = 5 }
  ["even when amending the same way in a different location"] {
    d.func != e.func
  }

  local newFunc = (it) -> false
  local f = (a) { func = newFunc }
  local g = (a) { func = newFunc }
  ["except when amending to the locationally equal thing"] {
    f.func == g.func
  }
}

[bioball]

I agree that we can find a way to get around the equality problem. Although, I don't think that's actually the problem with this proposal. This proposal still seems like strange behavior to me because you can change a typealias's behavior and identity by amending the module.

We enforce that schemas cannot be changed by amending (hence, why a class body can only reference const members when exiting their scope). I feel that this same principle applies to typealiases too; a typealias is schema, and so it probably shouldn't be able to be redefined by way of object amending.

Let's consider classes. This seems like obviously a bad thing:

// module1.pkl
name = "Bob"

class Person {
  name: String(startsWith(module.name))
}

// module2.pkl
amends "module1.pkl"

name = "Sarah"

import "module1.pkl"
import "module2.pkl"

person1: module1.Person = new { name = "Bobby" }  // okay
person2: module2.Person = new { name = "Bobby" } // fail; name needs to start with "Sarah"

This would mean that the meaning of a class can be changed by amending its enclosing module, and this is a behavior that we do not want (classes should be statically defined).

Given the above, I feel that typealiases would break this principle in the same way.

// module1.pkl
name = "Bob"

typealias PersonName = String(startsWith(name))

// module2.pkl
amends "module1.pkl"

name = "Sarah"

import "module1.pkl"
import "module2.pkl"

person1: module1.PersonName = "Bobby" // okay
person2: module2.PersonName = "Bobby" // fail; name needs to start with "Sarah"

I don't know how this is any different than the problem we see with classes.

The alternative proposal here is: references from a typealias body must be const. My concern here initially was that this will limit the usefulness of typealiases (you cannot just copy/paste property types and turn them into a typealias). I've since spent quite some time looking through existing Pkl code, though, and have yet to find a single typealias where a const requirement would be problematic. So, I'm now leaning away from the proposal put forth in this PR, and instead adding a rule that enforces that references are const.

[bioball]

Closing this; I believe this approach presents more problems than it solves; more details can be found here: https://github.com/apple/pkl-evolution/blob/1707776862c12d10fc57f4d38a3b3610793a2bc5/spices/SPICE-0007-const-checks-in-typealiases.adoc#alternatives-considered