Refinement scope and expressions

[jpolitz]

It's frustrating that refinements can't refer to one another, and that they can't be expressions.

For example, we can't write this example so nicely:

https://twitter.com/jameskjx/status/1534353153218445312?s=20&t=C-kuCLcS1P9dLTEscvL47w

fun get(n :: Number%(n >= 0), l :: List<String>%(l.length() > n)): ... end

Partly this is because refinements can't be expressions (so the above is a syntax error), but even allowing for that the scope simply doesn't work out; this is the way to express that idea:

fun get-nth-refined(n :: Number):
  length-pred = lam(l): (n >= 0) and (n < l.length()) end
  lam(c :: List<String>%(length-pred)):
      c.get(n)
  end
end

I think it's basically a “we didn't get that far and compiling expressions in type positions is tricky” kind of thing going on, not anything fundamental. The binding of n in the second parameter requires a little work to let* the parameters before checking the annotations, but that's already being code-generated as a sequence of checks inside function bodies so it's not so wild to make it work.

[jpolitz]

I realized the thing I suggested above is actually a breaking change to make work, since the refinements in the example are expressions that produce booleans, not functions (which they are currently expected to be). So really you'd need, say _ >= 0 for the refinement on n, and there's no terse _ expression for the refinement on l here.