type class synonym

Stream: lean4

[MangoIV]

How can I write something like this in lean4?

class A a b
class B a b
class (A a b, B b c) => C a b c
instance (A a b, B b c) => C a b c

[Mario Carneiro]

class A (a b : Type)
class B (a b : Type)
class C (a b c : Type) [A a b] [B b c]
instance (a b c : Type) [A a b] [B b c] : C a b c := ⟨⟩

[MangoIV]

what's the difference between that and extends?

[MangoIV]

thank you!

[Mario Carneiro]

With extends, they aren't actually arguments to C: if you look at the type of C it will be C (a b c : Type) : Type instead of C (a b c : Type) [A a b] [B b c] : Type

[Mario Carneiro]

and instead there are instances like instance (a b c : Type) [C a b c] : A a b

[Mario Carneiro]

But an instance like that is problematic, because when searching for A a b it will start looking for C a b ?c with unbound ?c

[MangoIV]

ah makes sense, is that the reason why it needs to pass the variables to the supreclass in that step already? I.e. causing the weird error where it says that it cannot decide the synthetization order?

[Mario Carneiro]

and so you get a weird error about synthesization order :P

[MangoIV]

I see, perfect, that's the reason I was asking in the first place (tried with extends but it didn't work)

[Mario Carneiro]

I'm not actually sure what the class (A a b, B b c) => C a b c haskell syntax is equivalent to, but I think it is the one with arguments rather than extends

[MangoIV]

I think in core it's the one with arguments, I'm not sure whether this distinction can be made in Haskell in a good way anyways/ the one with extends even exists.

[Mario Carneiro]

Can you say instance (C a b c) => ... and have A a b available in the context?

[Mario Carneiro]

or do you have to write instance (A a b, B b c, C a b c) => ...

[MangoIV]

yes, the former. This is the goal of the exercise, actually. :D

[MangoIV]

And I just saw that it's not like that in lean4.

[MangoIV]

another thing you can do in Haskell is actually

type C a b c = (A a b, B b c)

[Mario Carneiro]

that's class abbrev

[Mario Carneiro]

although it's probably subject to the same issues regarding synth order

[MangoIV]

oh nice, then I'll just use that one. I hope it doesn't have the same limitation like that haskell type synonyms

[MangoIV]

Mario Carneiro said:

although it's probably subject to the same issues regarding synth order

yes, same issue :/ So does that mean that this is not possible in Lean? that would be very unfortunate.

[Mac Malone]

@MangoIV The synth order check is not mandatory. You can turn it off and things will work as expected:

set_option synthInstance.checkSynthOrder false in
class C (a b c : Type) extends A a b, B b c
example [C a b c] : A a b := inferInstance -- works

[Mac Malone]

The error is just a warning that this class and instance has bad properties for certain type class inference situations. If your use case does not fall prey to those circumstances, then everything can still work out fine.

[Mac Malone]

In your case, you may, in fact, want to use class abbrev to get the A + B -> C instance for free:

set_option synthInstance.checkSynthOrder false in
class abbrev C (a b c : Type) :=  A a b, B b c
example [C a b c] : A a b := inferInstance -- works
example (a b c : Type) [A a b] [B b c] : C a b c := inferInstance -- works

The last instance would need manual definition with just extends.

[Mac Malone]

In this case, afaik, the warning is simply saying that the [C a b c] : A a b and [C a b c] : B b c instances will never be conventionally synthesizable. They can only be synthesized if an C a b c is already available in the context or c or a are manually set (because of the unbound ?c or ?a).

[Mac Malone]

Usually this is not a desirable property of instances (hence the error), but in your case it may be perfectly fine.

[Anne Baanen]

Mac Malone said:

Usually this is not a desirable property of instances (hence the error), but in your case it may be perfectly fine.

In fact, I claim it is perfectly fine exactly when a and c are functional dependencies on b, so you should make them outParams:

class A (a : outParam Type) (b : Type)
class B (a : Type) (b : outParam Type)
class abbrev C (a : outParam Type) (b : Type) (c : outParam Type) :=  A a b, B b c
example [C a b c] : A a b := inferInstance -- works
example (a b c : Type) [A a b] [B b c] : C a b c := inferInstance -- works

[Anne Baanen]

However, practically I would suggest going with Mario's class C (a b c : Type) [A a b] [B b c] (my technical term is "unbundled inheritance"). You are much less likely to encounter errors this way.

[MangoIV]

Mac Malone said:

In your case, you may, in fact, want to use class abbrev to get the A + B -> C instance for free:

set_option synthInstance.checkSynthOrder false in
class abbrev C (a b c : Type) :=  A a b, B b c
example [C a b c] : A a b := inferInstance -- works
example (a b c : Type) [A a b] [B b c] : C a b c := inferInstance -- works

The last instance would need manual definition with just extends.

Perfect, thank you so much, this makes a lot of sense!

[MangoIV]

On another note, is there a way to get actual functional dependencies? I e say I have an Add typeclass with three parameters and I want to hint lean that it can synthesise the third parameter every time that two others are given?

[Mario Carneiro]

that's the version Anne suggested

[Mario Carneiro]

outParam are outputs, everything else is an input

[Mario Carneiro]

(incidentally, the actual HAdd class does exactly this)

[Mario Carneiro]

/--
The notation typeclass for heterogeneous addition.
This enables the notation `a + b : γ` where `a : α`, `b : β`.
-/
class HAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- `a + b` computes the sum of `a` and `b`.
  The meaning of this notation is type-dependent. -/
  hAdd : α → β → γ

[MangoIV]

That’s not the same. With outParam I can only ever specify one fundep. But Add can theoretically compute all three parameters given two others.

[Mario Carneiro]

I'm not sure what you mean

[MangoIV]

type Add :: Nat -> Nat -> Nat -> Constraint
class Add m n res | m n -> res, res n -> m, res m -> n

This doesn't work in Haskell because of how instance resolution cannot backtrack and because of coherence but it should work in lean

In Haskell you can specify two of the dependencies because they don't need to backtrack

[Mario Carneiro]

no you can't have multiple functional dependency structures for the same class, they have to be different classes in that case

[Mario Carneiro]

it's not really clear how you would validate instances in that case

[MangoIV]

can you please elaborate on the second message or link to some resource about the constraints of the algorithm?

[Mario Carneiro]

the synth order check needs to know what the functional dependencies are

[Mario Carneiro]

it also comes up when initially setting up the typeclass search, the output variables are replaced by metavariables and unified after

[Mario Carneiro]

it's not really clear how you would do this if the class has multiple dependency structures

[Mario Carneiro]

What does haskell do with functional dependency information?

[MangoIV]

it's basically an injectivity annotation, it allows at call site to compute parameters from the others because all instances check some conditions for the instances to hold such that all of them are indeed injective (I'm not a maths person, I'm not talking about the injectivity that functions can have but the injectivity that functions must have (the other direction)). In the case that there are no fundeps, you can write more instances but you get an "ambiguous type" so something like leans metavariables? at the calll site.

[MangoIV]

https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/functional_dependencies.html?highlight=functionaldependencies#extension-FunctionalDependencies

[Mario Carneiro]

You can just turn off the synth order check and use it bidirectionally, if it works then great

[Mario Carneiro]

but lean typeclasses aren't really designed to be used this way

[MangoIV]

here goes the dream of prolog-like instance search

[Mario Carneiro]

oh you certainly can do that with lean typeclasses, it's not really advisable though

[Mario Carneiro]

there are a lot of limits that subtly imply that you're doing it wrong if you try

[Mario Carneiro]

not to mention the terms you get out are horrendous

[MangoIV]

Yeah the backtracking case runs out of fuel really quickly :sweat_smile:

[Notification Bot]

MangoIV has marked this topic as resolved.

[Notification Bot]

MangoIV has marked this topic as unresolved.

[MangoIV]

@Mario Carneiro actually the typeclass instance problem ist now stuck with turned off synth order and class abbrev when trying to use the function that requires that instance.

[MangoIV]

image.png
I now have to specify sig

[Mario Carneiro]

#mwe

[MangoIV]

nwm, it works with the correct fundeps. :)

[MangoIV]

@Anne Baanen I think your example is exactly the wrong way around, you want to compute the middle parameter from the outer ones.

[MangoIV]

https://git.sr.ht/~mangoiv/leff/commit/e3901ed788d2993338f5a85405e3b7f7f5844f5f

[Mac Malone]

MangoIV said:

I think your example is exactly the wrong way around, you want to compute the middle parameter from the outer ones.

This entirely depends on how your initial #mwe example works in practice. That is, what semantically A, B, and C. All three of the no synth check, outer out params, and middle out param work for different use cases (and do not work for others).