Add a Prim.Row.Closed compiler solved class

[natefaubion]

I've found the occasional want to do RowToList magic on a function that takes a record as an argument. The problem is these are inferred polymorphically, or at least the record tail is left unknown.

conjure ::
  forall r rl z.
  RowToList r rl =>
  Conjure rl r =>
  ({ | r } -> z) -> z
conjure = ?conjure

example =
  conjure \{ foo, bar } -> ...

Something like this doesn't compile because the type of r in this case will involve an unknown for the tail and RowToList requires an empty row terminator. Making this compile requires a type signature on the lambda closing the row. However, if we can conjure a record with only the required fields, this is totally safe.

Could we have something like

class Closed :: forall k. Row k -> Row k -> Constraint
class Closed open closed | open -> closed

Where the compiler yields a closed row with only the known components of the row? This would allow us to type the example as

conjure ::
  forall r rl z.
  Closed r r =>
  RowToList r rl =>
  Conjure rl r =>
  ({ | r } -> z) -> z

Forcing the unknown tail to unify with ().

[garyb]

Seems reasonable to me 👍

[hdgarrood]

This seems a bit dodgy to me. Doesn’t it depend on how far we are through type checking; unknowns could become concrete types as a result of later inference?

For example, would something like this be a problem?

eg =
  [ conjure \r@{ a } -> r
  , conjure \r@{ b } -> r
  ]

[natefaubion]

Can you define "be a problem"? It isn't clear to me what problem you are illustrating.

An alternative may be just asserting it's closed and unifying it's tail with () if it's unknown (so no output row).

[MonoidMusician]

I agree with Harry, I find it a little concerning that the solution to the constraint would change depending on when/where it's solved. To me that breaks something like a principle of substitution: C x (for x a unification variable) should never have a different solution from C (T y) (once we unify x with T y).

I mean, instance chains have to guard for apartness before they can reject a match, right? I see this as the same kind of thing. Just because we have AreEqual x y b in the current context, and x and y can't unify, doesn't mean they couldn't unify later. And just because we list a set of known fields in an open record ( a :: Int | r1 ) doesn't mean we wouldn't need to unify it with ( b :: String | r2 ) later (especially since unification is not local).

[hdgarrood]

I guess I’m imagining that this might cause implementation details of the compiler (i.e. the order in which things are checked) to affect resolving this class in potentially surprising ways. In that example I’m not sure whether I should expect the first conjure to resolve to a row with just a which would then make the second one fail to resolve, or whether both should resolve and produce rows with both a and b labels.

[natefaubion]

OK, lets take a step back then. Basically I want it to accept the most specific thing possible, rather than the most general thing possible, which to me means early solving and unification, effectively short-cutting the compilers desire to make record consumption as polymorphic as possible. You are saying "It could be more later", and I don't really want it to be more later, I want it to commit to something as early as possible based on the argument provided. Maybe the class proposed is too general and there's something else that can be done.

[MonoidMusician]

I understand your use case, and I'll try my utmost to respect it. But I am still concerned about how it fits into the larger scheme – that is, I'm not convinced that constraints are the right way to solve this problem.

Would it ever make sense to use/have a Closed constraint in context? Would it ever be used? (For most type classes, the answers to both of these would be yes, of course) What about a Closed constraint on an open row? I realize that this is not your use case, but I think it's a reasonable question to ask of the proposed solution.

constraintInContext ::
  forall r. Closed ( a :: String | r ) => ... =>
  ({ a :: String | r } -> z) -> z
constraintInContext f =
  let
   r = conjure f
  in ...

I suppose the difference would be that r here would be a skolem, not a unification variable, so Closed wouldn't solve it. That means solving Closed would have to case on whether the open row ends in a unification variable or not. I guess it would still be sound, just unprecedented ...

---

Why not approach your problem in other ways? I recognize it is more typing, but something like \({ a, b, c } :: { a :: _, b :: _, c :: _ }) -> ... should work, or even this cute solution, which should let the pattern matching syntax { a, b } be copied directly to specify the closed record { a, b }:

specify :: forall a b. (a -> Tuple a b) -> a -> b
specify f a = snd (f a)

toBeJust :: forall a b. a -> b -> Tuple a b
toBeJust = Tuple

-- test :: forall r. Semiring r => { a :: r, b :: r } -> r
test = specify \{ a, b } -> toBeJust { a, b } $ a + b

Output:

No type declaration was provided for the top-level declaration of test.
It is good practice to provide type declarations as a form of documentation.
The inferred type of test was:

  test ::
    forall t5.
      Semiring t5 => { a :: t5
                     , b :: t5
                     }
                     -> t5

in value declaration test

[natefaubion]

I am aware there are all sorts of ways to add annotations in cute ways. I've come up with several, but my use case is that the arguments demanded by the function are meant to be the annotations so the additional annotations are just faff that add no extra information. I'm fine with accepting that it makes no sense, but I would at least like to know with certainty why other than "it looks a little funny maybe" 😄. I fully recognize that in the truly general case, that may be true, but is it really a problem or just potentially unintuitive if used in a certain way? Like, does it break coherence or something? It's something that does come up with some frequency in the Slack chat.

Maybe another alternative is a class that eagerly returns the tail, and the user can do what it wants with it, which may be to constrain it or unify it with (). Or maybe it's something that we just don't attempt to solve while it's still OK to defer constraints. I don't actually know what consequences that might have.

[natefaubion]

Maybe it just doesn't make sense as a general constraint, as you said? Is there something that would make it make sense?

[natefaubion]

Another avenue might be, is there a way to have a Row.Cons like eliminator that only operates in some scope, but can be otherwise closed, thus making the unification local? My use case is that this record cannot outlive the scope of this function.

[natefaubion]

I think maybe the least gross thing with what we have would be indexed applicative-do (with type applications).

example = conjure Deref.ado
  foo <- deref @"foo"
  bar <- deref @"bar"
  in ...

[MonoidMusician]

Okay, I think I'm now fairly convinced that this can work. This is my current understanding of what the best solution would be:

• Add a compiler-solved class Closed :: forall k. Row k -> Constraint
• Solving it has four cases:
  1. Solve (closed): If the row is already closed, e.g. ( a :: _, b :: _ ), great – it can be considered solved.
  2. Make progress: If the row is open but has existing labels, e.g. ( a :: _ | r ), ask for Closed r to be solved.
  3. Solve & unify: If it is passed a unification variable, like when you call conjure, unify the variable with () and consider it solved.
  4. Defer: If it is passed a skolem variable, like in my constraintInContext example, ask for the instance to be in scope / refuse to solve it.

My arguments for this:

• It covers Nate's use case, which I agree is a common request and worth considering if we can find a way to make easier.
• I think cases iii. and iv. sufficiently address my question, and it means we can still support abstraction (i.e. deferring the constraint).
• I think having a single-parameter class makes more sense. In particular, because it asks for its argument to be unified with a closed row, it will never return two inconsistent results. I think this preserves consistency/confluence of unification/solving, because it will just fail if the "wrong" thing occurs, rather than giving different results in different places.

My only remaining concern is that, like Harry said, implementation details may be leaked, and we might solve too early. But I do think it is pretty clear when constraint solving happens, so hopefully that means it is okay to produce mild effects at the same time. We do solve constraints after unifying the function on the basis of its arguments, right? (If not, we would end up with it always wanting to unify to the empty row, and then realizing that the argument asked for labels a and b.)

If this actually works for the use case of conjure \{ a, b } -> ..., and behaves in a predictable manner for other similar use cases, then I would be fine with adding it. (Of course, I'm not a maintainer so I know my opinion doesn't carry much weight, I just want to be clear on the arguments.)

[natefaubion]

For reference, here is an indexed applicative approach.
https://gist.github.com/natefaubion/5efc2e487042ac0aa42ecd804e13cc04

Edit: Another that only lets you apply field names, and loses a parameter.
https://gist.github.com/natefaubion/b3b43fbc10bc1a50dc19de7e837cfa2c

[paf31]

Deferring the constraint doesn't make sense to me, since every row is "eventually closed". If it's not closed now, it will be closed when the function is instantiated, or that function's caller is instantiated, and so on ... by the time you reach main, you can't have any open rows left.

Regardless of whether this makes sense from a type system point of view (I feel like it doesn't, but I don't have a proof of unsoundness or anything), I think it would be a very unintuitive addition that wouldn't fit with the rest of the type system, hard to understand or teach. There are also workarounds, like creating a newtype over a closed row. That's what newtypes are for, after all, and if the solution to this case is a special thing in the compiler, it opens the door to all sorts of other changes solve slightly annoying things with classes for which the solution is "use a newtype".

[natefaubion]

A newtype doesn't help for this, because you still need a Newtype or Coercible constraint. Sure, "all it needs" is an annotation somewhere. Again, I'm willing to admit there's an XY problem here.

I think it would be a very unintuitive addition that wouldn't fit with the rest of the type system, hard to understand or teach

Can you qualify this in some way? (I'm being genuine). You've just stated it's unintuitive and hard to teach without saying what about it is unintuitive or hard to teach. Surely no one has tried to teach this! I fully recognize that what I've proposed may be very unintuitive, but maybe there is something that isn't? Something like this does come up with some frequency among the community, and I even find myself wanting it. I would at least like to be able to explain it in a clear, simple way that's not "it might be a little funny". Right now it essentially goes "Why is it funny?", "Because that's how it is." and I recognize that I don't actually know why it (or something like it) is fundamentally a bad idea.

the solution to this case is a special thing in the compiler

I personally find this somewhat disingenuous. We have no maintenance guidelines as to what does or does not make a good compiler solution.

[paf31]

Like I said, I don't have a proof that something is wrong here. I don't have time to try to produce a proof, or I would try. This just jumped out at me as I was browsing the issue list as something that made me uncomfortable enough to comment. I don't know why you think I'm being "disingenuous", but I think it's best at this point if I just bow out of the discussion here, and maybe in general.

[natefaubion]

Like I said, I don't have a proof that something is wrong here. I don't have time to try to produce a proof, or I would try.

I wasn't asking for a proof, I just want to know what your thoughts are on it in more detail in a way that I can learn from and distill to others. "Unintuitive and hard to teach" followed by "special casing in the compiler" is a really strong criticism, but without elaborating why it doesn't help me or the discussion (especially when it garners thumbs ups) except to shut it down.

[paf31]

I'm not trying to "shut it down", I'm just trying to say that I think this is a bad idea in as succinct a way as I can. I appreciate that my role in the creation of the compiler probably means my comments tend to carry a bit of extra weight, which is a big part of why I don't really comment any more, but maybe that makes things worse, I don't know. Anyway, I'd still like a way to be able to make a comment on things that I find troubling.

I think @hdgarrood's example is a good one for illustrating why this isn't intuitive.

I don't understand how you could implement this without special-casing something somewhere. It just doesn't seem to interact well with the way solving works by unification/substitution already. That's what I mean by hard to understand and teach - users gain an intuition for how that works, and this seems like it will behave differently. Complex type classes already seem to act magically if you don't understand how they're solved, but you can always follow the chain of dependencies to figure it out, and you only need to understand a small core set of concepts (fundeps, instance chains, etc.) to do so. I don't think this maintains that property, but as I say, I don't have a better example than Harry's, or a proof, so take that for what it is, it's just an intuition.

[hdgarrood]

Would adding syntax for a record binder which only has the fields listed in the binder and no others solve the need? Eg, if I could write, I dunno,

f {! x, y } = [x, y]

which would then have the inferred type forall a. { x :: a, y :: a } -> Array a.

[hdgarrood]

(Because if so I’d be more comfortable with that.)

[paf31]

Ok, here's a concrete complaint. Given:

conjure \{ a } -> ...

Why is { a :: _ } the unique good instantiation of this? Why is { a :: _, b :: _ }, which is consistent with the binder, and also a closed row, not also a good instantiation? If the point is to infer the closed row type just from the binder then there should be presumably be a unique solution.

I prefer @hdgarrood's closed record binders idea, but personally, I'd be interested to see other use cases before adding either of these new features.

[natefaubion]

Yes, syntax is an option as well. My thinking was:

• It really needs syntax so that the typechecker knows the user intent so it can proceed with how to typecheck this (:: is syntax).
• Does the syntax need to be on the argument? Why can't the set of row constraints be left open on the argument?
• Is there a way to push the instantiation to the caller? You can add a type signature to instantiate something explicitly, but this can't be abstracted in anyway, it pushes the burden to every call site. It's kind of like always annotating what variables a closure captures whenever you write a lambda.
• Why can't the burden be on the usage of conjure? I want conjure to be the syntactic thing that tells the compiler to act this way, but the only way we have to talk about something like this is with a constraint.

Maybe it's that for this to work the way that's intended, this would have to be solved as part of typechecking and not constraint solving. Is that the special case?

[natefaubion]

Wrt to @hdgarrood's example:

eg =
  [ conjure \r@{ a } -> r
  , conjure \r@{ b } -> r
  ]

I would want this to just say it can't unify (a :: t0) with (b :: t1). conjure is the syntax that says this isn't open. It's basically making a new typechecker rule for an adhoc literal. Again, maybe the issue is that for this to work robustly, it can't be a Constraint constraint, and it needs to be part of typechecking.

[hdgarrood]

What would it mean for it to be part of typechecking?

[natefaubion]

I think it would mean that it would need to be solved eagerly as part of the application judgement, so that when it sees conjure applied to the function, it closes the row after checking the function against the type of the argument to conjure.