Confused about ListToRow

#1

Extremely simple question, something very silly that I’m missing. Why doesn’t this work?

call :: forall r. ListToRow (Cons "aaa" Int Nil) r => Record r
call = {aaa: 3}

The error is

Could not match type

    r0

  with type

    ( aaa :: Int
    | t1
    )


while checking that expression { aaa: 3
                               }
  has type Record r0
in value declaration call

The ListToRow class has a functional dependency which should determine r i.e. (aaa :: Int) satisfies the instance ListToRow (Cons "aaa" Int Nil) r. The reverse also doesn’t work:

call :: forall r. RowToList r (Cons "aaa" Int Nil) => Record r
call = {aaa: 3}

What am I getting wrong?

#2

I haven’t read the PureScript compiler in detail, so I could be wrong, but as far as I know PureScript does not infer type x when there is an expression a :: forall x. C x => F x , and x is inferred only when a is used.
Thus, the following program also causes an error.

call2 :: forall x. TypeEquals x Int => x
call2 = 1

How to create a Record type from a RowList is … I have no idea.
Basically, RowList is used when defining a function that converts Row → RowList and then uses RowList to derive instances and then back to Row again.
In this case, the type of Row is inferred when using this function, and it works well from there.

1 Like
#3

TypeEquals is the “correct” way to solve this isolated example, but you need to call from, and it’s inconvenient. The compiler does not implicitly utilize type equality constraints (unlike GHC, which will allow an equality in scope to solve here).

test
  :: forall r
   . TypeEquals (Record r) { wat :: Int }
  => ListToRow (Cons "wat" Int Nil) r
  => Record r
test = from { wat: 42 }

Note that you still have to declare the type for your coercion.

I personally don’t use ListToRow, and I’ve done a lot of metaprogramming with records and row types. IMO, since it’s not a builtin and does it’s own row list induction and produces no evidence, all it’s going to do is slow down your compile times.

But regardless, it’s useful when you are writing a function that is structurally polymorphic on some Record or Variant. If you are constructing a concrete record, it’s not polymorphic, so you need the above type equality nonsense. In that case, you are really only using it as some sort of type function, and I’d absolutely agree that concrete type functions are not a usecase that the compiler prioritizes right now.

2 Likes
#4

I was indeed trying to use it as just a type function, my code is littered with abuse of functional dependency classes to this end haha. I never wanted to create records whose rows satisfied the RowToList constraints anyway, this was just to check my understanding. It works fine for what I actually wanted, which is define instances of the aforementioned classes on a consumed record. Thanks!

1 Like