list.traverse

Stream: mathlib4

[Kevin Buzzard]

In mathlib3 we have docs#list.traverse defined in data.list.defs. To my surprise there is no Data.List.Defs in mathlib4 even though there is plenty of list stuff, which makes me think that Data.List.Defs is somehow being subsumed by other files. But I can't find docs4#List.traverse . It's not hard to write -- but where do I put it?

[Kevin Buzzard]

PS looking up what mathlib3port has to say about the matter I see there's a dubious translation claim:

/- warning: list.traverse -> List.traverse is a dubious translation:
lean 3 declaration is
  forall {F : Type.{u} -> Type.{v}} [_inst_1 : Applicative.{u v} F] {α : Type.{u_1}} {β : Type.{u}}, (α -> (F β)) -> (List.{u_1} α) -> (F (List.{u} β))
but is expected to have type
  forall {F : Type.{u} -> Type.{v}} [_inst_1 : Applicative.{u v} F] {α : Type.{_aux_param_0}} {β : Type.{u}}, (α -> (F β)) -> (List.{_aux_param_0} α) -> (F (List.{u} β))
Case conversion may be inaccurate. Consider using '#align list.traverse List.traverseₓ'. -/
protected def traverse {F : Type u → Type v} [Applicative F] {α β : Type _} (f : α → F β) : List α → F (List β)
  | [] => pure []
  | x :: xs => List.cons <$> f x <*> traverse xs
#align list.traverse List.traverse

But the only thing dubious about that translation is that a universe seems to have an exotic name in the Lean 4 version. Is this somehow telling me that there might be universe unification issues with this declaration in Lean 4?

[Floris van Doorn]

This doesn't look dubious, and it being flagged as such is probably a bug in mathport.
Similar to https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/why.20dubious.3F

[Floris van Doorn]

I think making a Data.List.Defs makes sense. Maybe there is some other stuff in that file that isn't already in Lean 4.

[Kevin Buzzard]

OK I'll add the new file and make a note that it's not an actual port.

[Arien Malec]

I'm on Data.List.Defs

[Arien Malec]

It's going slowly -- most of it is #align statements to map to the right files in Std4

[Kevin Buzzard]

Oh nice! I'd just started looking at this and was trying to work out whether it was suitable for me. Did you open a PR? If so then I can link to it and move onto something else. Thanks for letting me know!

[Arien Malec]

I haven't PRd yet -- wanted to get the thing into shape. Will do shortly and post the PR here.

[Arien Malec]

mathlib4#804

Lots of odd type errors to fix and need to double check #aligns

[Mario Carneiro]

I had a suspicion on what is causing the issue, and it turns out to be correct. Here's the new output from mathport on this example:

/- warning: list.traverse -> List.traverse is a dubious translation:
lean 3 declaration is
  forall {F : Type.{u1} -> Type.{u2}} [_inst_1 : Applicative.{u1, u2} F] {α : Type.{u3}} {β : Type.{u1}}, (α -> (F β)) -> (List.{u3} α) -> (F (List.{u1} β))
but is expected to have type
  forall {F : Type.{u2} -> Type.{u3}} [_inst_1 : Applicative.{u2, u3} F] {α : Type.{u1}} {β : Type.{u2}}, (α -> (F β)) -> (List.{u1} α) -> (F (List.{u2} β))
Case conversion may be inaccurate. Consider using '#align list.traverse List.traverseₓ'. -/
protected def traverse {F : Type u → Type v} [Applicative F] {α β : Type _} (f : α → F β) :
    List α → F (List β)
  | [] => pure []
  | x :: xs => List.cons <$> f x <*> traverse xs
#align list.traverse List.traverse

I said before that it matches the types modulo universe names, but that's not quite correct. Actually it has a specific order of universe parameters in mind, but the universes are being named different things. The names of the universes don't matter but the order of arguments is important and will cause type mismatches if they are messed up.

In the output above, universe names are overwritten with their ordinal positions in the list of universes. So u1 is the first universe in the list, u2 is the second and so on. (Also bound variable names have been normalized to match to make diffing easier.)

We can now see the issue clearly: There are three universes involved, corresponding to the named universes u and v in F and the unnamed universe which is the type of α. In Lean 3, this resulted in the list [u, v, u_1] where u_1 is the anonymous universe, and in lean 4 it results in [_aux_param_0, u, v] where _aux_param_0 is the anonymous universe. Note that the order is different, and this causes the mismatch.

[Kevin Buzzard]

Aah so this really is a dubious translation!

[Arien Malec]

Is there a porting hint to fix the output from mathport or does this not have implications for downstream code?

[Kevin Buzzard]

I suspect that this will have implications for downstream code if and only if there is an instance in mathlib3 of someone using explicit universe annotations with traverse. Do you know what, I suspect that you could probably actually get the universes right; I think it's just a case of variables being declared in the wrong order. But changing variable order might cause problems in other places. And searching for traverse.{ gives 0 results in mathlib (if someone was explicitly giving universes to the function then it would look like traverse.{u v w}) so I suspect that you should just leave a porting note saying that universes are now in a different order and just leave it at that. It happens for List.traverse and Sum.traverse I think.

[Arien Malec]

I think I #alignd away most of the defs that had this issue, but I'll double check.

[Reid Barton]

In category theory, though, explicit universe levels are passed a lot and it would be better to try not to change the order, if it's just a matter of being a bit careful with variables and such.

[Reid Barton]

Where by "category theory", I mean category_theory/.

[Kevin Buzzard]

@Mario Carneiro because Reid's comment made me paranoid I thought I would revisit this. You posted the new output from mathport on List.traverse (which is no longer my problem as it's being ported in a different file) above with no out_param universes in. But in Sum.traverse here it's still reporting a possibly dubious translation, the universes look to match up, we still have out_param universes, and it's hard for me to tell whether there is still an issue with the translation or not because I don't know how to tell whether the order of the universes has been swapped. Do I just ignore and continue or is there still a possibility that something here is dubious?

[Mario Carneiro]

I think I didn't update mathport to use the u1, u2 style yet, that example above was only my local copy. But I did hunt down where these weird _aux_param_0 universes are coming from and it is actually a bug in lean 3, see lean#788. The issue is that we are actually aligning sum.traverse._main to Sum.traverse (because lean 3 generates this useless extra definition when you use the equation compiler and lean 4 doesn't), but even just aligning sum.traverse._main to sum.traverse is dubious because the _main definition uses an _aux_param_0 universe and puts it at the start, while sum.traverse uses u_1 and puts it at the end.

[Mario Carneiro]

That is all to say that there is still a bug in generating these definitions that causes the translations to be dubious. You know you are in this case if you see a reference to _aux_param_0 in the dubious translation message. For now, you should handle this like other implicit reorderings: add an #align with \_x, and mention in the comment that this is about reordered universes.

[Kevin Buzzard]

But I checked the order of the universes in sum.traverse and Sum.traverse and they were in the same order

[Mario Carneiro]

Did you check sum.traverse._main?

[Kevin Buzzard]

No. But why is that relevant if Sum.traverse is going to be aligned with sum.traverse?

[Kevin Buzzard]

lol

sum.traverse.{u_1 u_2} :
  Π {σ : Type u_1} {F : Type u_1 → Type u_1} [_inst_1 : applicative.{u_1 u_1} F] {α : Type u_2} {β : Type u_1},
    (α → F β) → σ ⊕ α → F (σ ⊕ β)
sum.traverse._main.{u_1 u_2} :
  Π {σ : Type u_2} {F : Type u_2 → Type u_2} [_inst_1 : applicative.{u_2 u_2} F] {α : Type u_1} {β : Type u_2},
    (α → F β) → σ ⊕ α → F (σ ⊕ β)

So you're absolutely right: the universes get switched! But as I say, this shouldn't matter I guess, because traverse._main isn't ever used in mathlib, and the universes for Lean 3 sum.traverse and the Lean 4 Sum.traverse are the same way around, so we align those and everything should be fine.

[Mario Carneiro]

The reason this matters for mathport is because binport performs the translation in declaration order, treating whichever of sum.traverse._main and sum.traverse comes first (and of course sum.traverse._main comes first, since sum.traverse is a wrapper over it). So binport ends up actually just translating sum.traverse._main to Sum.traverse (it needs to use the one that actually has a substantive definition), and then when it gets to sum.traverse it just says "oh I guess I already translated this" and moves on. We end up with two definitions that mapped to one, which would be fine if they had the same signature, but...

[Kevin Buzzard]

So I can see that in theory there might be a problem, but in practice given that traverse._main never shows up in mathlib and neither does traverse.{ I suspect that we can just not worry about this. Right? Or am I missing something?

[Mario Carneiro]

You are free to align with \_x, but if you align it directly it will cause failures in binport and the usual degradation of output. I have some ideas for how to fix mathport so that it uses the signature of sum.traverse instead of sum.traverse._main as the source of truth, but it hasn't been implemented yet.