HInv?

Stream: new members

[Ben Selfridge]

Is there a heterogeneous inverse type? I expected to find HInv along with HPow, but I could not find one.

[Yakov Pechersky]

How would that work, given that inv is a unary function? What would be heterogenous about it?

[Aaron Liu]

Takes an α, returns a β

[Yakov Pechersky]

And the return type would be inferred from the context? I think even for HFoo binary functions, the return type is usually constrained by the two input types.

[Ben Selfridge]

Ah, that makes sense. I figured if it didn't exist, there would have to be a reason.

[Ben Selfridge]

It could work if there were a way to encode functional dependencies or open type families in Lean, but I'm not sure if there is.

[Yakov Pechersky]

Functional dependencies is approximated by outParam

[Yakov Pechersky]

but then you might as well have a plain Inv X and then Coe X Y

[Ben Selfridge]

Oh, maybe I will try that then. I just want nice notation for the inverse of an isomorphism.

[Ben Selfridge]

(with an isomorphism type i'm custom defining for my own purposes)

[Eric Wieser]

That's a nice example where a Coe wouldn't work

[Ben Selfridge]

Why wouldn't that work?

[Alfredo Moreira-Rosa]

Digging on this subject. Could'nt we define HInv as :

class HInv .{u} (α : Type u) (β : outParam (Type u)) where
  hInv : α → β

Example usage, for Dimensional analysis :

variable {α δ : Type} [AddCommGroup δ] [Repr δ]

structure Quantity (dim : δ) (α : Type) [AddCommGroup δ] where
    val : α
    deriving Inhabited, BEq, DecidableEq

instance  [Inv α] : HInv (Quantity d α) (Quantity (-d) α) where
    hInv := ⟨q.val⁻¹⟩

Would it not work for everyone ?
That what i want to do on my lib. But today it clash with Inv because the notation is not targetting HInv. For it to work we need this decl on Std so that notation is targeting HInv instead of Inv. And When defining an Inv have an instance of HInv automatically provided like for other H<Op> we have.

[Alfredo Moreira-Rosa]

And maybe the same could be done for HNeg

[Kenny Lau]

Ben Selfridge said:

Oh, maybe I will try that then. I just want nice notation for the inverse of an isomorphism.

but the inverse of an isomorphism is still an isomorphism? (i.e. i don't see why you need heterogeneous)

[Aaron Liu]

Kenny Lau said:

Ben Selfridge said:

Oh, maybe I will try that then. I just want nice notation for the inverse of an isomorphism.

but the inverse of an isomorphism is still an isomorphism? (i.e. i don't see why you need heterogeneous)

The inverse of an isomorphism FooEquiv α β is a FooEquiv β α (which is a different type)