The question about type-class inference and RowList in particular


#1

The original discussion took place on the slack channel ( #purescript-beginners ), where after some time of intensive staring and partially clueless tinkering I was defeated by the compiler’s:

 Main.purs    82   3 error    NoIns…   No type class instance was found for
 Prim.RowList.RowToList ( login :: String, passwd :: String | p3) t4

spewed on my code:

apiGetBad
  ∷ ∀ e m p
  . MonadJsonHttp e m
  ⇒ MonadApiAccess m
  ⇒ Lacks "login" p
  ⇒ Lacks "passwd" p
  ⇒ WriteForeign { | p }
  ⇒ ApiRoute
  → { | p }
  → ExceptV e m Json
apiGetBad route params = do
  {login, password, apiUrl} <- lift getApiAccess
  get (apiUrl <> route) (insert (SProxy :: SProxy "login") login (insert (SProxy :: SProxy "passwd") password params))

get :: forall p.  WriteForeign { | p } => String → { | p } → ExceptV e m Json
..

I came up with the question on the slack, and was helped by some better equipped for the job, namely: dariooddenino, justinw, and monoidmusician. Dario presented the following solution:

apiGet
  ∷ ∀ e m p rl x
  . MonadJsonHttp e m
  ⇒ MonadApiAccess m
  ⇒ Lacks "login" p
  ⇒ Lacks "passwd" p
  ⇒ WriteForeign { | p }
  ⇒ RowToList (login :: String, passwd :: String | p) rl
  ⇒ WriteForeignFields rl (login :: String, passwd :: String | p) () x
  ⇒ ApiRoute
  → { | p }
  → ExceptV e m Json
apiGet route params = do
  {login, password, apiUrl} <- lift getApiAccess
  get (apiUrl <> route) (insert (SProxy :: SProxy "login") login (insert (SProxy :: SProxy "passwd") password params))

to highlight the lines that had made the difference:

  ⇒ RowToList (login :: String, passwd :: String | p) rl
  ⇒ WriteForeignFields rl (login :: String, passwd :: String | p) () x

So while I see what is happening (if I squint), it’s not entirely clear to me, why the compiler couldn’t see the RowList instance, and what exactly had changed in the terms of compiler’s “reasoning”. I’d be grateful if someone could provide more step-by-step explanation of how the compiler is trying to solve this constraints.
Thanks is advance!


#2

Sorry! I forgot to reply to this earlier. Here it is now!

Setup

Lets insert an intermediate step quickly:

  let paramsPlusLogin = insert (SProxy :: SProxy "login") login (insert (SProxy :: SProxy "passwd") password params)

(insert has a complex type, but let’s not worry about that, since it is already working.)

Now we’re going to look at the last line of the do notation (get (apiUrl <> route) paramsPlusLogin). Let’s set up the local context first – this is one of the most important parts of how compilers work, knowing what is in scope:

Type Level Variables (and their kinds) Value Level Variables (and their types)
e :: # Type
m :: Type -> Type
p :: # Type

route :: ApiRoute
params :: { | p }
login :: String
password :: String
apiUrl :: String
paramsPlusLogin :: { login :: string, passwd :: String | p }

And we have some typeclasses constraints, which provide these values:

Class Methods
MonadJsonHttp e m get :: forall p. WriteForeign { | p } => String -> { | p } -> ExceptV e m Json
MonadApiAccess m getApiAccess :: m { login :: String, password :: String, apiUrl :: String }
Lacks "login" p none (but helps with insert)
`Lacks “password” p none
WriteForeign { | p } writeImpl :: { | p } -> Foreign

Now our task is to make this line happen:

  get (apiUrl <> route) paramsPlusLogin

Now’s where the fun typeclass solving begins!

get :: forall p. WriteForeign { | p } => String -> { | p } and we’re providing it with a string argument (check! :heavy_check_mark:) and an argument of type { login :: string, passwd :: String | p }. Hmm … that means we need WriteForeign { login :: string, passwd :: String | p }.

Solving for WriteForeign { login :: string, passwd :: String | p }

The compiler maintains a list of instances for each typeclass. A partial list can be found on pursuit for this class: class WriteForeign a.

We notice that there is a instance that pertains to records: instance (RowToList row rl, WriteForeignFields rl row () to) => WriteForeign { | row }. So now we choose row = ( login :: string, passwd :: String | p ) (do you see why?), and continue looking for instances.

In particular, we need both RowToList ( login :: string, passwd :: String | p ) rl and WriteForeignFields rl ( login :: string, passwd :: String | p ) () to, for some unsolved variables rl and to.

Solving RowToList ( login :: string, passwd :: String | p ) rl

Solving RowToList is usually pretty easy, and the compiler does it automatically, generating rl from the row. But this only works for closed rows! It can’t be solved for open rows like ( login :: string, passwd :: String | p ). This is because the RowList needs to be sorted, and you don’t know what the ordering of login and password will be with respect to the rest of p.

Therefore, we cannot reduce this constraint any further, and we have to add the constraint RowToList ( login :: string, passwd :: String | p ) rl to our top-level function. (Or do we?)

This also means that we need to add another type variable to the function too, since rl wasn’t defined. It will have kind RowList.

Solving WriteForeignFields rl ( login :: string, passwd :: String | p ) () to

This class has fundeps rl -> row from to which means that, as rl should be solved by the above, this class should be solvable now.

Unfortunately, we don’t know what rl is, so it can’t be reduced further. This means we again need to add it to the constraints on our function. And add the variable to.

Recap

As noted in the original post, we needed to add these constraints (along with variables rl and x) to let the compiler solve for the correct instance:

  ⇒ RowToList (login :: String, passwd :: String | p) rl
  ⇒ WriteForeignFields rl (login :: String, passwd :: String | p) () x

Bu actually, there was another solution too! We could have just added the constraint WriteForeign { login :: String, passwd :: String | p } directly!

What’s the difference? The difference is that the former set of constraints implies the latter one. It’s what the compiler looks for when it needs to solve an instance of WriteForeign for a record type. So having them in scope is sufficient to solve the WriteForeign instance. But it is possible to have it in scope directly too. (Then the caller of the function will end up solving for the sufficient constraints.)

But what about WriteForeign { | p }??

So the interesting thing is that we never mentioned this constraint. It’s actually not necessary!

The deal is, it makes sense conceptually, since solving both constraints requires each of the fields to have a WriteForeign constraint … but it’s not part of how the compiler solves for the WriteForeign { login :: String, passwd :: String | p } instance, so it contributes nothing.

Constraints on rows are complex and tricky; this is not a proof system

In general, that’s the hard part of dealing with rows and rowlists in PureScript. This is because the constraint system is a logical system (it basically models logic), but you can only use the basic inference steps represented by the instances directly. You can’t “prove” any shortcuts.

For instance, it is a true statement that RowCons "sym" t r1 r2 implies Union ( sym :: t ) r1 r2 (in the sense that, in any context t :: Type, r1 :: # Type, r2 :: # Type where the former is solvable, the latter must also be solved). This is essentially how Union works, by iterating over a bunch of RowCons constraints. But that’s not how it is implemented in the compiler, so this argument is not provable.

Or an even simpler example: given an instance for Union r1 r2 (), what do you know about r1 and r2? Well, directly you know that their union is empty … but that must mean they both are empty! However, that again is reasoning that is true, but outside the system of deduction for constraints, as they are solved by the compiler. (This also implies RowLacks sym r1 for any sym, etc.)

Constraint solving algorithm (basics)

The compiler begins by listing all instances that are in scope, in terms of variables and concrete types and whatnot. Then it seeks to match an instance, either directly (e.g. if WriteForeign { login :: String, passwd :: String | p } is in scope, it would use that), or by choosing an instance (which it does based on the fundeps) and continuing to solve the constraints on that instance.

(Of course, this all relies on a notion of unifying types (which assigns type variables to other values, often more concrete, as necessary), and of what types are “apart” and cannot be unified. But those should be pretty intuitive to grasp.)

But notice that it just has one path to go down to solve an instance – if WriteForeign { login :: String, passwd :: String | p } doesn’t exist directly, it’s bound to using the record instance and solving for its constraints instead.

It’s like skiing down a mountain: once you commit to a path, there’s no turning back. Hopefully you don’t hit a dead end :evergreen_tree: :boom: :skier: :dash:

Follow the instances!

I think that’s the gist of how it works. Maybe others can add to it :slight_smile:


#3

That’s a really great post! Just one comment wrt

I don’t think it can’t be solved because it needs to be sorted. It can’t be solved because what would a RowList be for an unknown tail? You could sort for what you know and probably add another case to RowList for UnknownTail rather than just Nil. But pretty much all cases require a fully solved RowList to remain sound. For example, if a hypothetical Eq instance allowed UnknownTail, then equality would only be performed based on the fields you know about, which means two records may either be equal or not equal in different contexts, depending on how much is known about them. That’s pretty problematic I think.


#4

Thanks Nate! :smile:

I think I actually meant partially solving it.

You know how ListToRow (Cons "sym" t rl) ( sym :: t | r ) is valid given ListToRow rl r (by the inductive definition)? (Thus the compiler can reduce requiring the former constraint to just the latter.) I just wanted to point out that the converse is not true with RowToList


#5

@monoidmusician
Thank you, for this detailed answer. Since the original problem I’ve spend several more hours with complex type annotations and your answer has been a help.
I think the most important thing for me, that eluded me till I read your answer is that constraints that cannot be resolved at call-site must be propagated to the caller, which now seems pretty obvious. And that the compiler’s ability to resolve these constraints depends on whether it is provided with polimorphic or concrete instance, which as well pretty apparent.
Well, I guess there should be more introductory materials to this topic.

Atm I feel more confident about what’s going on on the type class constraints level.
Cheers!


#6

Yes! Those are important takeaways, thank you for reiterating them :slight_smile: I’m glad it was helpful!!


#7

@anks Where would you look first to find more introductory materials on this topic? I can make a note to add or improve the docs there.