type class inference notes

Stream: general

[Kevin Buzzard]

I'm writing some currently sketchy docs on type class inference (because if I don't then in 1 month's time I'll be back here asking to be reminded of letI again). Would I be right in thinking that one could think about the type class inference system as (amongst other things) a big directed graph, with classes as vertices, and with a directed edge from C1 to C2 iff type class inference gives you a way of getting a structure of type C2 from one of type C1? I'm aware that it's more complex than this, basically because the system works for families so you could in theory envisage type class inference showing that if X has structure C1 then X × X × bool has structure C2, but amongst other things is it reasonable to think about this graph? And then the condition I want to put on this graph is that any two routes from C to D have to be definitionally equal as functions; in particular I could have a directed edge from C to D and one from D to C but the composite both ways had better be the identity function, and basically I am suggesting that somewhere there is a category with at most one morphism between any two objects. Is this an oversimplification?

[Mario Carneiro]

It's not a bad way to think about it, but you really want the category to be generated by a directed acyclic graph, meaning that C -> D -> C will be disallowed. Besides the fact that composition of typeclass instances is almost never definitionally the identity (it usually is at best an eta expansion of the original instance), loops in the graph can lead to nontermination in typeclass inference.

[Kevin Buzzard]

So you're happy with two paths from C to E as long as they're defeq, but you are not happy with a loop even if it's defeq to id? Or are you just saying that this doesn't really ever happen in practice (basically it would be two typeclasses carrying the same data, so one might argue that there is no point).

[Kevin Buzzard]

I guess in the category language the two classes would be canonically isomorphic

[Kevin Buzzard]

Am I right in thinking that Haskell "does not have this problem"?

[Mario Carneiro]

It is really hard to write a pair of instances that compose to id. For example, suppose C has fields a,b and D has x,y; then f : C -> D might be defined by f inst = {a := inst.x, b := inst.y} and g : D -> C is g inst = {x := inst.a, y := inst.b}. Even though the composition is provably the identity, it reduces to f (g inst) = {a := inst.a, b := inst.b} != inst.

[Mario Carneiro]

But my second point is that even if you did have a loop that is defeq to id, it would cause typeclass inference to loop in many circumstances, for example if I want E and I have C I apply f : C -> D and then look for D -> E, and then apply g and look for C -> E, and repeat. The typeclass inference algorithm is not smart enough to check for loops, nor does it sort instances in a smart way, so even if the instance C -> E exists it may still loop if the C -> D instance comes first.

[Mario Carneiro]

Haskell doesn't have this problem because it doesn't have to deal with defeq at all (well it does, but only in much simpler cases), since it's not trying to prove theorems about the programs. It just needs to find some instance for the typeclass, so it can use it to call whatever function you've stated. Diamonds can still be a problem if you get an entirely different function as a result, but since you aren't stating theorems about it only "observational equivalence" matters, i.e. provable equality, and these can just be stated in comments or what have you, they aren't mechanically checked.