Is there mutually recursive classes?

Stream: Type theory

[Tesla Zhang]

Hi, this is a beginner question. Does Lean4 classes support mutual recursion? If so, does that always imply mutually recursive instances, and is there any obvious problems regarding mutual recursion in classes?

Apart from that, is there mutual recursion between classes & functions/inductives?

[Mario Carneiro]

No, classes cannot be recursive at all

[Mario Carneiro]

more specifically, structure cannot

[Mario Carneiro]

class is just @[class] structure

[Tesla Zhang]

I see, thank you very much! That's a fast and furious reply.

[Mario Carneiro]

you can use class inductive and those can be recursive

[Tesla Zhang]

??????????? How does class inductive work? What does it mean?

[Mario Carneiro]

@[class] inductive

[Tesla Zhang]

What do implementers implement? Constructing the instances? Is it useful in any scenarios?

[Mario Carneiro]

@[class] is just a signal to the typeclass inference mechanism that this type can be used in [] and inferred by tc inference by default

[Tesla Zhang]

Ok, I see, that's very intuitive

[Mario Carneiro]

similarly instance is just @[instance] def

[Mario Carneiro]

so you can also just make elements of that inductive and mark them as instances

[Tesla Zhang]

Ok, great da★ze

[Mario Carneiro]

The graph of instances doesn't have to mirror the definitions at all, it can have loops and whatnot (but you might hit issues if the instances are set up badly)

[Tesla Zhang]

I see, I guess I can find the rest of the answers in tabled typeclass resolution, right? Thanks again!

[Mario Carneiro]

it's just like a bunch of theorems saying given an A and a B you get a C and so on, and the TC inference mechanism just applies these eagerly

[Mario Carneiro]

that paper describes how it is able to present this interface without performance problems, it is not particularly relevant for users except insofar as it determines what kinds of patterns cause TC inference to fall over

[Mario Carneiro]

I think it is intended for implementers, e.g. if you wanted to write a TC inference implementation for another language

[Tesla Zhang]

Yeah, I am currently implementing classes for a theorem prover like Lean, and I'm thinking about mutual recursion support for classes.

The language has fancy inference for mutual recursions. You write them down like in Java and it'll be type checked with inferred orders. Compared to this, Coq & Agda are like C/C++ where we need forward declarations :) I'm unsure what Lean4 does though

[Mario Carneiro]

ah, in that case it is indeed the paper to read

[Mario Carneiro]

I believe it comes down to better caching support to help detect loops

[Mario Carneiro]

there are some simple patterns that lead to exponential behavior if you aren't careful with caching

[Tesla Zhang]

Yeah I can see that happening in Haskell/Agda

[Mario Carneiro]

In your description it is not clear whether you are talking about the typeclass inference mechanism (like in haskell) or recursive functions, where at run time functions call each other in a loop

[Mario Carneiro]

Coq / Agda / Lean all have to be very strict about recursive functions because you can prove false if you don't have a clear well founded metric

[Mario Carneiro]

for typeclass inference you can basically have an arbitrary graph of dependencies because everything is resolved at compile time

[Mario Carneiro]

Most programming languages are less strict about recursive functions, and allow arbitrary call graphs (possibly with forward declarations) because they aren't trying to prevent partiality

[Tesla Zhang]

I'm talking about the definition of classes and instances and its language-feature-interaction with termination check. I've heard of some bad stories so I'm a little worried :(

[Tesla Zhang]

Specifically, if you define the instance Show where show x = ? (I hope the idea is clear) for, say, inductive X := A : X | B : List X -> X, you'll end up invoking instance [Show X] => Show (List X) which is involved in the call graph and the termination check needs it to figure out the structural recursion-ness of the definition, while this is not clear simply by resolving the names