weird class error

Stream: lean4

[Michael Jam]

On nightly-2021-11-06, I expected the following piece of code to type check:

class C where c (p : Sort u) : Nat
class D extends C
def fc [C] : Nat := C.c (0 = 0)
def fd [D] : Nat := C.c (0 = 0)

However, fd does not compile with the following error message:

  D.toC
argument has type
  D
but function has type
  [self : D] → C

Is this a bug or do I misunderstand something?
When I replace extends by a manual instance, I still see the error.
When I replace Sort u by Prop, or by any type with a fixed universe, the error goes away.
Thanks for suggestions...

[Michael Jam]

Hi, here is perhaps a more convincing mwe:

class C where f : Sort u → Nat
class D extends C
def a [C] := C.f Nat
def b [D] := D.toC.f Nat
def c [D] := C.f Nat

Oddly, b compiles but not c and I can't figure out why. I might be wrong but it looks like a bug to me. Any idea what could be wrong?

To give more context I was trying to formalize Nat's with a philosophy of avoiding inductive types completely.
But the problem is that my Nat class extends Nat_induction, and then I got stuck so I reduced my problem to the above mwe.

section
variable (N : Type _)
class Zero where
  zero : N
export Zero (zero)
class Succ where
  succ : N → N
export Succ (succ)
class Succ_Not_Zero [Zero N] [Succ N] where
  succ_not_zero {n : N} : succ n ≠ zero
export Succ_Not_Zero (succ_not_zero)
class Eq_Of_Succ_Eq_Succ [Succ N] where
  eq_of_succ_eq_succ {n m : N} (h : succ n = succ m) : n = m
export Eq_Of_Succ_Eq_Succ (eq_of_succ_eq_succ)
class Nat_Induction [Zero N] [Succ N] where
  nat_induction {P : N → Sort _}
    (P0 : P zero)
    (ih : (k : N) → P k → P (succ k))
    (n : N) : P n
export Nat_Induction (nat_induction)
end

section
variable (N : Type _)
class Natural
extends Zero N, Succ N, Succ_Not_Zero N, Eq_Of_Succ_Eq_Succ N, Nat_Induction N
end

section
variable {ℕ} [Natural ℕ]
def pred_with_proof (n : ℕ) (h : n ≠ zero) : Σ' m, n = succ m :=
  by
  revert h
  let P (k : ℕ) := k ≠ zero → Σ' m, k = succ m
  exact (nat_induction (by simp ; exact False.elim) (λ k _ _ => ⟨k, rfl⟩) n : P n)

def pred (n : ℕ) (h : n ≠ zero) : ℕ := (pred_with_proof n h).fst
end

pred_with_proof will fail to type check...

Thanks in advance for any suggestions you might have ...

[Kevin Buzzard]

classes are inductive types ;-) The difference is that they only have one constructor.

[Reid Barton]

I think nat_induction does not mean what you think it means

[Reid Barton]

The class Nat_Induction has two universe levels, one for N and one for the universe level that you can eliminate into

[Reid Barton]

Maybe you already realize this... but it's pretty suspect; for example how could Lean figure out that the instance Natural ℕ in pred_with_proof has to be of the level that allows elimination into the type ℕ? I mean we can see this because we know that [Natural ℕ] is intended to discharge the class assumption in the single use of nat_induction, but Lean doesn't think this way

[Reid Barton]

The behavior in your original post still seems strange though--I don't get an error with the Lean 3 translation:

class {u} C := (c (p : Sort u) : nat)
class D extends C
def fc [C] : nat := C.c (0 = 0)
def fd [D] : nat := C.c (0 = 0)

[Michael Jam]

Classes might be implemented as inductive types under the hood, but I like to think of them as an orthogonal system separate from inductive types that lean provides.

The reason I put a Sort _ in nat_induction instead of a Prop, is just because I saw that Nat.rec signature uses a Sort _. I essentially copied Nat.rec's signature. I acknowledge that my naming conventions are kind of inaccurate here and there.
I am aware that there are 2 universes in nat_induction but I didn't really understand why according to you that would be an issue. To help lean with the nat_induction call I am giving the return type : P n explicitly. Alternatively I could be explicit about P and say (P := P)

If this was an issue about universes, why would b type check and not c in the below example on lean4 nightly-2021-11-10 ?

class C where f : Sort u → Nat
class D extends C
def a [C] := C.f Nat
def b [D] := D.toC.f Nat
def c [D] := C.f Nat

All the universes revolving around c also revolve around b as I understand it.

I'll translate my longer code to lean3 to get clearer ideas when I find some time.
Thank you for your comments.

[Reid Barton]

What I mean is the class Nat_Induction itself (and hence also the class Natural) has two universe parameters, and Lean won't guess which universe level instantiation of Natural you want to provide when you write variable {ℕ} [Natural ℕ].

[Reid Barton]

I'm guessing what you want/expect is for nat_induction to be quantified over all universes like Nat.rec is, but it's not.

[Reid Barton]

In this example with a b c, it's clear that you mean def a [C.{1}] := C.f Nat, def b [D.{1}] := ..., def c [D.{1}] := ..., but I'm not sure why Lean figures that out in some cases but not others.

[Reid Barton]

Actually we have (or used to have?) a similar issue in the category theory library, where it's hard to predict when you need to include universe variables, but maybe it was fixed?

[Mac]

@Michael Jam the error in your original post is likely a bug with Lean. Since D is a class, its auto-generated self parameters for fields are tagged as synthetic (i.e., using[self : D] for the binder). This results in the signature of D.toC being [self : D] -> C (with no explicit parameter). The automatic structure to parent conversion, however , is mistaking trying to insert an invalid D.toC d argument. In code:

def fd [D] : Nat := C.c (0 = 0)
-- (mistakenly) elaborates to roughly
def fd [d : D] : Nat := C.c (self := D.toC d) (0 = 0)

[Michael Jam]

@Reid Barton I see what you mean now. Thanks for clarifying.

Is there a way to quantify a universe variable in a class method? Or is there a reason its not possible? I tried to write

  nat_induction.{v} {P : N → Sort v}

in the class definition but it gives me some "invalid field" error.
The v universe seems to always get attached to the class itself which isn't what I want.

[Sebastian Ullrich]

Since the universe of the class must be at least as large as those of the class fields, you would need an ordinal as the universe level (as well as being able to quantify over universe levels at that position in the first place), which Lean does not support.

[Michael Jam]

I see ... So inductive types are in a way more expressive than type classes because they define some functions with universe quantifications

[Michael Jam]

I might ask a stupid question but, why does a class need to have a type? Couldn't it be a type-less set of requirements?

[Kevin Buzzard]

In Lean's type theory, everything needs to have a type. There might well be other set-ups where you can avoid this I guess.

[Sebastian Ullrich]

Interestingly, Coq's modules are not first-class values and thus do not have a type and can quantify like this even without ordinal universes. But one consequence of that is that they need special kernel support.

[Reid Barton]

You could get rid of the classes by just passing everything directly, but you still can't abstract over universe-polymorphic values.

[Mac]

You could statically "abstract" over universe polymorphic values though using a macro that produce a version of the class for each universe (like C++'s templates), but that isn't exactly in the spirit of Lean's type theory. That is, it would (in general) be better (and easier) to adapt one's approach to Lean's style, than try and force it to do what one wants.

[Michael Jam]

Is there like a good example or situation showing why it's useful for a typeclass to have a type? I don't really have one in mind, that's why I was just wondering...

[Kevin Buzzard]

It makes the kernel smaller, because you don't need special kernel support for them.

[Mac]

Michael Jam said:

Is there like a good example or situation showing why it's useful for a typeclass to have a type? I don't really have one in mind, that's why I was just wondering...

How exactly are your proposing for them to not have a type?

[Kevin Buzzard]

What you are saying really is "why do we use Lean's type theory instead of another type theory?" Other programs use other type theories.

[Michael Jam]

OK so its mostly a reason of implementation. I guess as you were saying it's because they are implemented as inductive types under the hood, so all the inductive type machinery can be reused.

[Mac]

Note that type classes in Lean 4 (if not in Prop) are data that can be passed around to functions and are thus compiled. Types in Lean provide info to the compiler as to the representation of the object in memory. Without a type for the class, Lean would have no way of knowing how to compile them.

[Sebastian Ullrich]

I mean, type classes in Haskell do not have a type either. It's not unimaginable, just very unlikely to change.

[Michael Jam]

Is the typeclass system part of Lean's type theory itself? isn't it external?

[Mac]

@Sebastian Ullrich ah, yes they do?

[Mac]

type classes in GHC are functions of the kind Constraint

[Sebastian Ullrich]

I take the +1 from a GHC dev to say that constraints really are not types in any reasonable sense

[Reid Barton]

Well, mainly GHC is not Haskell.

[Reid Barton]

Eq a isn't a type.

[Mac]

@Reid Barton what do you mean by that?

[Reid Barton]

The point that I think you're making is that there are sensible languages which don't treat classes and types as the same, and consequently have special-purpose mechanisms for passing instances (Eq a =>), or constructing values (instance Eq a), etc.

[Mac]

@Reid Barton But Lean does have special purpose mechanisms for type classes and does treat them differently. For example, you can't use a synthetic binder for a non-class object.

[Mac]

I don't see a significant difference in the way that GHC and Lean conceptual think of type classes (at a type theory level). They, however, do have different ideas of how type classes should be used (GHC's single instance resolution vs Lean's tabled multi-instance resolution).

[Reid Barton]

This doesn't seem like a good-faith discussion to me, so I'm going to drop it.

[Mac]

Huh? I am entirely confused. It appears that I have come off badly, but I am not really sure why. However, I do apologize if that is the case.

[Reid Barton]

Maybe there was a language issue about what it means to be (or to have) a type. In any case, I don't think the discussion was useful. The point is just that it's perfectly sensible to separate the world of values and types from the world of instances and classes. For example, Haskell (as defined by the language standard) works this way. Lean doesn't do this, and that is unlikely to change.

[Kyle Miller]

@Michael Jam For you pred_with_proof example, on an old version of Lean 4 (lean4:nightly-2021-06-02) I don't see any errors. (Maybe there are no errors because of a bug that's long been corrected.)

[Kyle Miller]

Michael Jam said:

I see ... So inductive types are in a way more expressive than type classes because they define some functions with universe quantifications

I think this is only in the sense that every universe quantification has to come first in a type. For class members, there's an implicit class instance argument, and since universe quantification has to come before that argument, the class has to be dependent on that universe level.

There's nothing really special with universe quantifications that inductive types can do, I think. All this means is that you have to give instances that quantify over the universe variables (i.e., there's a separate Nat_induction class for every single substitution of universe variables), but you're liable to run into typeclass inference issues since it's easy to get into situations where Lean's going to fail to find instances. It won't fill in universe metavariables for you without some reason to.

[Kyle Miller]

I guess (very) the awkward thing is that your proofs have to take Nat_induction instances for every universe variable that a proof depends on, rather than just a single instance, if you want to use classes for something like this.

[Kyle Miller]

That's a limitation of the type system, though -- you can't make a function that takes a universe-polymorphic function as an argument.

[Kyle Miller]

@Michael Jam For what it's worth, a reason you don't need recursors using the typeclass system is that if you had one, it's possible to prove that your type is isomorphic to some inductive type, so you can instead have a typeclass that holds a proof of equivalence. The recursor then becomes a theorem, and that theorem is able to quantify over universe variables.

structure Equiv (α β) where
  to_fun : α → β
  inv_fun : β → α
  left_inv : ∀ x, inv_fun (to_fun x) = x
  right_inv : ∀ x, to_fun (inv_fun x) = x

section
variable (N : Type _)
class Zero where
  zero : N
export Zero (zero)
class Succ where
  succ : N → N
export Succ (succ)

class Nat_Induction [Zero N] [Succ N] where
  from_nat : Equiv Nat N
  zero_eq : from_nat.to_fun 0 = zero
  succ_eq {n : Nat} : from_nat.to_fun (Nat.succ n) = succ (from_nat.to_fun n)

theorem nat_induction [Zero N] [Succ N] [Nat_Induction N]
  {motive : N → Sort _}
  (zero : motive zero)
  (succ : (k : N) → motive k → motive (succ k))
  (n : N) : motive n :=
  sorry
  -- prove this by induction on Nat_Induction.from_nat.inv_fun n

theorem succ_not_zero [Zero N] [Succ N] [Nat_Induction N]
   {n : N} : succ n ≠ zero := sorry

theorem eq_of_succ_eq_succ [Zero N] [Succ N] [Nat_Induction N]
  {n m : N} (h : succ n = succ m) : n = m := sorry

end

[Sebastian Reichelt]

@Michael Jam and @Mac, did you open a bug report for the erroneous explicit argument? I'm asking because I keep running into a somewhat similar issue and I'm wondering whether it is the same bug or not. Here is an MWE (though probably not completely minimal):

structure A

class B (a : outParam A) (α : Sort u)
class C {a : A} (α : Sort u) [B a α]
class D {a : A} (α : Sort u) [B a α] [C α]

class E (a : A) where
[c (α : Sort u) [B a α] : C α]

instance (a : A) [e : E a] (α : Sort u) [B a α] : C α := e.c α

def d (a : A) [E a] (α : Sort u) [B a α] : D α := sorry

On the last line, with lean4:nightly-2021-11-12 I get:

application type mismatch
  instC a
argument has type
  E a
but function has type
  [e : E a] → (α : Sort u) → [inst : B a α] → C α

[Mac]

@Sebastian Reichelt no, I did not. And yeah, that looks like it is probably the same error.

[Sebastian Reichelt]

Thank you. I've reported it as https://github.com/leanprover/lean4/issues/796 now.