Mutual Recursive Typeclass Methods Between Two Instances?

Stream: general

[Segev Elazar Mittelman]

Is there any way to create two typeclass instances, each of which containing a function, with those functions being mutually recursive, without defining the functions in a mutual block outside the instances first?

[Kenny Lau]

probably not

[Aaron Liu]

if the typeclass is an abbrev for a function then maybe

[Aaron Liu]

if the typeclass is a structure then no

[Segev Elazar Mittelman]

What would a typeclass that is an abbrev for a function look like? Just a typeclass with a single function method and nothing else or do I have to use the abbrev keyword somewhere?

[Kenny Lau]

I don't think that's legal, I think the following is what Aaron intended, but Lean complains:

@[class] abbrev Foo := Nat → Nat

[Aaron Liu]

docs#DecidableEq

[Aaron Liu]

is a typeclass

[Aaron Liu]

but also an abbrev for a function

[Segev Elazar Mittelman]

Ah, and it supports mutual types right?

[Aaron Liu]

no idea what that means

[Aaron Liu]

like mutual inductive types or

[Kenny Lau]

mutual recursion probably

[Aaron Liu]

oh

[Segev Elazar Mittelman]

Sorry brain misfire, I'm thinking in the context of deriving DecidableEq, how do they derive it for mutually inductive types

[Aaron Liu]

oh they don't

[Aaron Liu]

I don't think they do

[Aaron Liu]

not yet at least

[Segev Elazar Mittelman]

But it should be possible since its an abbrev?

[Kenny Lau]

there's basically not much support :tm: for anything "mutual" that you want to make

[Segev Elazar Mittelman]

Ah that's trouble. I'm trying to derive some mutually dependent typeclasses via metaprogramming, one example being a typechecker mutually defined with a type inferrer.

[Kenny Lau]

by metaprogramming do you mean "I won't prove anything with my definitions"?

[Segev Elazar Mittelman]

That's not what I mean by it but I probably won't prove anything with these definitions. They're for use in a QuickChick style PBT library.

[Segev Elazar Mittelman]

The metaprogramming is for syntactically analyzing an inductive relation then extracting various functions from it.

[Segev Elazar Mittelman]

Btw, deriving DecidableEq does support mutual inductives, it just defines a mutual block of the decEq functions then later creates instances.