Record with multiple Cons

Hi,

I am trying to write a row polymorphic function working with a record of 2 fields, but field names are not fixed.

Snippet for a record with 1 field is working:

foo ::
  forall @f1 s b.
  IsSymbol f1 =>
  Cons f1 Boolean b s =>
  Record s ->
  Record s
foo = R.set (Proxy @f1) true <<< R.set (Proxy @f1) true

useFoo :: { f1 :: Boolean }
useFoo = foo @"f1" { f1: false }

Is there a way to compose types to describe a record more fields?

Try 1

bar ::
  forall f1 f2 s0 s1 s2.
  IsSymbol f1 =>
  IsSymbol f2 =>  
  Cons f1 Boolean s0 s1
  Cons f2 Boolean s1 s2  =>
  Record s2 ->
  Record s2
bar = R.set (Proxy @f1) true <<< R.set (Proxy @f2) true

Error:

  No type class instance was found for

    Prim.Row.Cons f16
                  t1
                  t2
                  s27


while applying a function set
  of type IsSymbol t0 => Cons @Type t0 t1 t2 t3 => Cons @Type t0 t4 t2 t5 => Proxy @Symbol t0 -> t4 -> Record t3 -> Record t5
  to argument Proxy

Try2:

bar ::
  forall @f1 @f2 s0 s1 s2 s.
  IsSymbol f1 =>
  IsSymbol f2 =>
  Union s1 s2 s =>
  Cons f1 Boolean s0 s1 =>
  Cons f2 Boolean s0 s2 =>  
  Record s ->
  Record s
bar = R.set (Proxy @f1) true <<< R.set (Proxy @f2) true

unsafeCoerce is not working with row types

Try 1 was close:

bar ::
  forall f1 f2 s0 s1 s2.
  IsSymbol f1 =>
  IsSymbol f2 =>  
  Cons f1 Boolean s0 s2 =>
  Cons f2 Boolean s1 s2 =>
  Record s2 ->
  Record s2
bar = R.set (Proxy @f1) true <<< R.set (Proxy @f2) true
1 Like

Thanks, now it is working, but could you explain why my first version is wrong?

Cons f2 Boolean s1 s2 <=> s2 type is a s1 type with field f2
Cons f1 Boolean s0 s1 <=> s1 type is a s0 type with field f1


s2 type should have both fields f2 and f1 because of transitivity

The Cons type class is a 4-way relation which asserts that one row of types can be obtained from another by inserting a new label/type pair on the left.

It’s ‘row types aren’t unordered’ week here on discourse.purescript.org!

When you call R.set (Proxy @f1) true, what the compiler needs to know is Cons f1 Boolean _ s2, because what you give that function is a Record s2. You’re effectively asking why the compiler doesn’t infer the existence of Cons f1 Boolean _ s2 from the Cons f1 Boolean s0 s1 and the Cons f2 Boolean s1 s2 it has in scope.

In this special case, the compiler theoretically could make that inference, because both Cons instances are talking about Boolean. But consider the more general case of inferring a Cons f1 a _ s2 from Cons f1 a s0 s1 and Cons f2 b s1 s2, where a and b are different types. Imagine making the following variable substitutions:

  • f1 = "x"
  • f2 = "x"
  • s0 = ()
  • s1 = (x :: a)
  • s2 = (x :: b, x :: a)

Now Cons f1 a s0 s1 and Cons f2 b s1 s2 both hold, but Cons f1 a _ s2 won’t hold for any row you put in the wildcard position. So it would be incorrect for the compiler to make that inference in the general case.

We probably don’t have logic for the special case of two Cons instances in scope with equal second argument type because it isn’t a case that comes up in practice that often, but maybe that’s worth revisiting in a feature request if you can make the argument.

As general advice, if a low-level function has a constraint, you’ll trip yourself up less if you propagate that constraint faithfully up your call chain instead of trying to infer clever ways you could adapt that constraint to something else that should be equivalent. Especially when row types are involved, the compiler doesn’t always have the same ideas about what constraints are equivalent—and regardless of whether the compiler is right or you are right (and both have been known to happen), at the end of the day the compiler decides what it accepts.