what is a diamond?

Stream: general

[Kevin Buzzard]

The Category 5 Diamond (Xena).

What is a typeclass diamond (note : this has nothing to do with Scholze's diamonds, it's an unfortunate name-clash)? I think it's something like the above link. Two distinct instance routes from A to D, with typeclass inference giving us two terms of type D which are provably distinct. I am assuming that the system should be regarded as having failed at this point. How much can I get away with? I think there are other lower category diamonds as well though, right? What other things can go wrong? Instances which are equal but not computably equal? Instances which are equal but not definitionally equal? Is there some sort of complete catalogue of diamonds?

[Keeley Hoek]

With regard to auto-naming, what do you think a good strategy for naming those would be? It would probably be really easy to implement

[Kevin Buzzard]

I was going from xena.B to xena.D in my example, in the xena namespace, and getting a name which depended only on D. I guess I want to have B tagging along somehow. Is there some clever thing you can do with dots?

[Floris van Doorn]

I think the term type class diamond is used whenever there are two ways to go from class A to class D, regardless of whether the two resulting instances are definitionally equal or not. I think it will be quite a big problem if you have a diamond and the resulting instances are not definitionally equal (whether they are provably equal is less important. I think we should restrict instances enough so that we don't get these kinds of bad diamonds.

[Floris van Doorn]

golf:

theorem you_are_in_typeclass_trouble_now : d1 ≠ d2 := by rintro ⟨⟩

[Johan Commelin]

If the class is a subsingleton, I want to be able to use non-defeq instances.

[Johan Commelin]

That ought to be possible, right?

[Kevin Buzzard]

That currently is annoying. @Sebastian Ullrich I know the type class system will not be changing, but this issue about typeclass inference failing to do subsingleton elimination is something we mathematicians are beginning to run into. Am I asking for rfl++ or something?

[Patrick Massot]

I don't think Sebastian said the type class system won't change. He wrote they didn't know yet what would be a better system. It's clear it has to improve, the current system simply doesn't scale.

[Patrick Massot]

Part of the problem is indeed type-theoretic but, as far as I understand, most of the issues are completely generic (in which order do we search, what is cached, etc.)

[Wojciech Nawrocki]

Ralf Jung, who's a Coq expert, just wrote a blog post (link) about the problems diamonds cause and possible solutions. It seems that it's still a mostly unsolved problem, and possibly some issues you encounter here are due to the exponential blowup described there.

[Reid Barton]

Interesting post. How did you come across it, by the way?

[Reid Barton]

The diamonds mentioned in that post are of a different type, related to classes extending other classes

[Reid Barton]

For example, B and C both extend A and D extends both B and C. If you have a D then you probably want the As to be defeq, but there's no way to even express that.

[Simon Hudon]

In both Coq and Lean?

[Reid Barton]

I think the issues are mostly the same in both. I guess I didn't pick the best example--in this case Lean will deduplicate the A fields in D if you use the old structure command, I think?

[Reid Barton]

A better example is if you don't want to make the class D at all

[Reid Barton]

because you have lots of things that extend A, and you don't want to make all the combinations.
Then you have no way to say "A which is both B and C"

[Johan Commelin]

@Wojciech Nawrocki Thanks for sharing this! Interesting read.

[RalfJ]

Hi! Author of that post here. Lean was also just mentioned in our Coq-side discussion of this post. I am very curious how Lean compares here.

[RalfJ]

The diamonds mentioned in that post are of a different type, related to classes extending other classes

Yeah, the diamonds I saw mentioned in the backlog here are diamonds in the inference search tree, not in the algebraic hierarchy (which are the kinds of diamonds that bundling approaches have problems with). I mention that issue in my post as well though I dont call it a dimaond -- this is the exponential blowup coming from the Monoid A -> Semigroup A instance together with the prod instances, where there are now two ways to derive Monoid (A*A) -> Semigroup (A*A).

[Johan Commelin]

Cool, welcome!

[Mario Carneiro]

@RalfJ Lean has the same foundational problem, but it isn't yet a big issue. The blog post doesn't discuss the style used in mathlib, which is to have "partially unbundled" structures, where the type is a parameter but none of the operators. This minimizes the nesting level, although there are some examples where we have deeper depth like modules (that use two variables) and there was an example using three variables that floated on the chat recently

[Mario Carneiro]

Also, not mentioned in that asymptotic analysis is the amount of subterm sharing in the term. I think the size of those instances is actually linear, but if you write it as a tree instead of a dag then it becomes quadratic or cubic etc

[Johan Commelin]

But it is very likely to become a problem in the (near?) future?

[Mario Carneiro]

I don't think so... you have to be dealing with some pretty complicated objects for it to come up, so if it was an issue it would have stopped us already

[Mario Carneiro]

We have issues with typeclass search order, but that's a different matter

[Scott Morrison]

This is a really great thing about the lean-perfectoid-spaces project: we've made a definition which is about as complicated as they come (at least in algebraic geometry / number theory?), and Lean could cope.

[Kevin Buzzard]

One of my main motivations for doing perfectoids was to see if Lean could handle them -- it was clear from the start that it was theoretically possible but Patrick pointed out very early on that this didn't mean that it was possible, and at times I was (incorrectly) worried that it might not be. I am still trying hard to understand what Mario wrote about timeouts. I've taken to trying to compile the perfectoid project with smaller values for the timeout parameter and am trying to understand what makes part of it slow to compile -- everything so far is pointing at naivity in the code -- poor proof engineering, as Mario calls it.

[Kevin Buzzard]

In short, I have no formal training in programming and this is now beginning to show

[Kevin Buzzard]

But at the end of the day the project does compile

[RalfJ]

"partially unbundled" structures, where the type is a parameter but none of the operators

I mentioned having the operators unbundled but the superclasses bundled, that gives you O(n^3) If you just have the type unbundled you get O(n^2), but you have even more sharing problems and you cannot even use the typeclasses for the operators and their notation before having shown the axioms. We had some cases where that was annoying, but the real trouble here is sharing once your inheritance hierarchy has a diamond.

[RalfJ]

@Mario Carneiro

not mentioned in that asymptotic analysis is the amount of subterm sharing in the term. I think the size of those instances is actually linear, but if you write it as a tree instead of a dag then it becomes quadratic or cubic etc

I explicitly mention that in the conclusion. :) And yes, if you fully exploit sharing I think it remains linear. But then you have to ensure that every pass traversing your AST (unification, reduction, elaboration, type checking, whatever...) exploits sharing. A single lapse and your get the bad complexities back. At least in the Coq world people tell me that is not feasible.

[RalfJ]

I don't think so... you have to be dealing with some pretty complicated objects for it to come up, so if it was an issue it would have stopped us already

in our case, it was really when we started to put the hierarchy to use that the performance became an issue. as long as you are just defining your algebraic classes and show all sorts of properties about them it's good, but then we ended up defining our logic with 5 or more nested combinators (i.e., the equivalent of Zn 5), and then we nest that again in several more layers, so we end up with n=10 and more -- and then we have quite a few lemmas about that, and everything got slow. I have no idea what people have been doing in Lean so I cannot compare.

[Mario Carneiro]

what do you mean about Zn 5?

[RalfJ]

I was referring to my post; I mean that we had something like iProp := T*U*V -> A -> B, where * and -> have TC instances like prod in my post. This is like Zn 5 = Z*Z*Z*Z*Z.

[Mario Carneiro]

so you are trying to infer that e.g. Z^5 has a ring structure?

[RalfJ]

and then we built things like ((X -> iProp) -> T -> iProp) -> ((X -> iProp) -> T -> iProp). So if you count the number of combinators here, it's... 20 or more.

[Mario Carneiro]

I'm confused about the role of T,U,V etc in those examples

[RalfJ]

just random types that are in our hierarchy

[Mario Carneiro]

You have a theorem that has 20 type arguments, plus all their typeclasses?

[RalfJ]

like, random rings, if we stick to that example

[RalfJ]

no, these are all concrete types

[RalfJ]

well, most of them

[Mario Carneiro]

Inferring that Z^5 has a ring structure should be quadratic, since you have to talk about Z^n itself and the ring structure for each of the subterms

[Mario Carneiro]

it's not quintic

[RalfJ]

with the fully unbundled approach and if ring is a subclass of group, the power is 6 at least

[RalfJ]

that's what I explained in my post

[Mario Carneiro]

So in mathlib if ring is a subclass of group that only increases things by a constant factor, I think, since the typeclass args will be twice as big

[Mario Carneiro]

I think fully unbundled is the killer here

[RalfJ]

I think fully unbundled is the killer here

it definitely is

[RalfJ]

but we've also had loads of problems with bundling^^

[Mario Carneiro]

with partially unbundled style you won't get that kind of thing unless you have n different type arguments, which is quite rare for mathematical structures

[RalfJ]

the sheer number of arguments doesnt even matter

[RalfJ]

only their "level of nesting" -- like arguments that have arguments

[Mario Carneiro]

So I guess this is another variant on "don't use dependent types in DTT"

[RalfJ]

;)

[Johan Commelin]

@RalfJ I don't know if you have Lean installed. I ran this code to illustrate how mathlib/Lean deals with this:

section
set_option pp.all true

lemma inst01 : ring ℤ := by apply_instance
lemma inst02 : ring (ℤ × ℤ) := by apply_instance
lemma inst03 : ring (ℤ × ℤ × ℤ) := by apply_instance
lemma inst04 : ring (ℤ × ℤ × ℤ × ℤ) := by apply_instance
lemma inst05 : ring (ℤ × ℤ × ℤ × ℤ × ℤ) := by apply_instance

#print inst01
#print inst02
#print inst03
#print inst04
#print inst05
end

The output of the last two prints is:

theorem inst04 : ring.{0} (prod.{0 0} int (prod.{0 0} int (prod.{0 0} int int))) :=
@prod.ring.{0 0} int (prod.{0 0} int (prod.{0 0} int int))
  (@domain.to_ring.{0} int
     (@to_domain.{0} int
        (@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
           (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
              int.decidable_linear_ordered_comm_ring))))
  (@prod.ring.{0 0} int (prod.{0 0} int int)
     (@domain.to_ring.{0} int
        (@to_domain.{0} int
           (@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
              (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
                 int.decidable_linear_ordered_comm_ring))))
     (@prod.ring.{0 0} int int
        (@domain.to_ring.{0} int
           (@to_domain.{0} int
              (@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
                 (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
                    int.decidable_linear_ordered_comm_ring))))
        (@domain.to_ring.{0} int
           (@to_domain.{0} int
              (@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
                 (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
                    int.decidable_linear_ordered_comm_ring))))))

and

theorem inst05 : ring.{0} (prod.{0 0} int (prod.{0 0} int (prod.{0 0} int (prod.{0 0} int int)))) :=
@prod.ring.{0 0} int (prod.{0 0} int (prod.{0 0} int (prod.{0 0} int int)))
  (@domain.to_ring.{0} int
     (@to_domain.{0} int
        (@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
           (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
              int.decidable_linear_ordered_comm_ring))))
  (@prod.ring.{0 0} int (prod.{0 0} int (prod.{0 0} int int))
     (@domain.to_ring.{0} int
        (@to_domain.{0} int
           (@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
              (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
                 int.decidable_linear_ordered_comm_ring))))
     (@prod.ring.{0 0} int (prod.{0 0} int int)
        (@domain.to_ring.{0} int
           (@to_domain.{0} int
              (@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
                 (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
                    int.decidable_linear_ordered_comm_ring))))
        (@prod.ring.{0 0} int int
           (@domain.to_ring.{0} int
              (@to_domain.{0} int
                 (@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
                    (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
                       int.decidable_linear_ordered_comm_ring))))
           (@domain.to_ring.{0} int
              (@to_domain.{0} int
                 (@linear_ordered_comm_ring.to_linear_ordered_ring.{0} int
                    (@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring.{0} int
                       int.decidable_linear_ordered_comm_ring)))))))

[Johan Commelin]

It is slightly repetetive, but it's clearly linear (-;

[Mario Carneiro]

import algebra.pi_instances
set_option pp.all true

lemma inst01 : ring ℤ := by apply_instance
lemma inst02 : ring (ℤ × ℤ) := by apply_instance
lemma inst03 : ring (ℤ × ℤ × ℤ) := by apply_instance
lemma inst04 : ring (ℤ × ℤ × ℤ × ℤ) := by apply_instance
lemma inst05 : ring (ℤ × ℤ × ℤ × ℤ × ℤ) := by apply_instance

meta def count_int : list char → ℕ
| [] := 0
| l@(_::l') :=
  if l.take 3 = "int".to_list then count_int (l.drop 3) + 1 else
  count_int l'

open tactic
meta def count_int_in_decl (n : name) : tactic ℕ :=
do d ← get_decl n, e ← pp d.value,
   return $ count_int e.to_string.to_list
#eval do
  l ← mmap count_int_in_decl
    [``inst01, ``inst02, ``inst03, ``inst04, ``inst05],
  trace l, -- [5, 12, 20, 29, 39]
  guard $ l = (λ n, (n^2 + 13*n) / 2 + 5) <$> list.range 5

[Mario Carneiro]

it's quadratic

[Mario Carneiro]

but the linear term is pretty large, so the quadratic behavior doesn't assert itself until n = 13 or so

[Mario Carneiro]

to see why, notice that (prod.{0 0} int (prod.{0 0} int (prod.{0 0} int int))) appears on line 1, (prod.{0 0} int (prod.{0 0} int int)) appears on line 5, (prod.{0 0} int int) appears on line 10 and so on in inst05

[Kevin Buzzard]

I experimented with this stuff a few weeks ago. IIRC when you go up to 6 factors it doesn't work!

[Kevin Buzzard]

Some search gives up before it finds it. Is my memory correct?

[Mario Carneiro]

yes, you have to raise the instance search depth to get past 5 factors

[RalfJ]

@Johan Commelin @Mario Carneiro given that this uses just the type as an index, quadratic is exactly what my blog post predicts :)

[RalfJ]

what I am curious about now is if lean can keep the inference and/or checking times linear by exploiting sharing

[Mario Carneiro]

Heh, this just appeared on the isabelle mailing list: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-May/msg00089.html . Looks familiar...