An Arrow instance for Lean functions

Stream: new members

[corrededCrustacean]

Hello, I'm trying to implement the Arrow typeclass in Lean, and I'm having trouble implementing it for Lean functions. Here's what I have:

class Arrow (Arrow : Type -> Type -> Type) where
  compose {A B C : Type} : Arrow B C -> Arrow A B -> Arrow A C
  first {A B X : Type} : Arrow A B -> Arrow (A×X) (B×X)
  second {A B X : Type} : Arrow A B -> Arrow (X×A) (X×B)

instance : Arrow (· -> ·) where
  compose := fun f g => f ∘ g
  first f := fun (a,x) => (f a, x)
  second g := fun (x,a) => (x, f a)

The following works, but I have to specify the arrow constructor:

#check Arrow.compose (·+1) (·*2) (Arrow := (· -> ·))

I would like to be able to do this:

#check Arrow.compose (·+1) (·*2)

But it gives the following error:

./src/./Circuit.lean:12:27: error: application type mismatch
  Arrow.compose ?m.446 fun x => x * 2
argument
  fun x => x * 2
has type
  Nat → Nat : Type
but is expected to have type
  ?m.391 ?m.393 ?m.394 : Type

I think it's because (· -> ·) is universe-polymorphic so it isn't precisely Type -> Type -> Type:

#check (· -> ·)
-- fun x x_1 => x -> x_1 : Sort u_1 -> Sort u_2 -> Sort (imax u_1 u_2)

And indeed if I make a simpler wrapper it works:

inductive Function : Type -> Type -> Type where
  | Fun {A B : Type} (f : A -> B) : Function A B

-- instance : Arrow Function where ...

#check Arrow.compose (Function.Fun (·+1)) (Function.Fun (·*2)) -- this works

I've tried making a universe-polymorphic Arrow class, but I couldn't find a way to make it work. I've tried this:

class Arrow (Arrow : Sort u_1 -> Sort u_2 -> Sort (imax u_1 u_2)) where
  compose {A : Sort u} {B : Sort v} {C : Sort w} :
    Arrow B C -> Arrow A B -> Arrow A C
  -- ...

Which doesn't work because the u_1 and u_2 are fixed for the Arrow type constructor, so Arrow B C doesn't typecheck since B : Sort v and not B : Sort u_1. I'd need to be able to write something like:

class Arrow (Arrow : {u_1 u_2 : Universe} -> Sort u_1 -> Sort u_2 -> Sort (imax u_1 u_2)
  -- ...

But I couldn't find how to do that in Lean.

[Chris Bailey]

I'm very tired, but I think this is just a typeclass synthesis issue you can fix either by making the type parameter an outParam, or making the instance a default instance.

class Arrow (Arrow : outParam (Type -> Type -> Type)) where
...

or

@[default_instance]
instance : Arrow (· -> ·) where
  compose := fun f g => f ∘ g
  first f := fun (a,x) => (f a, x)
  second g := fun (x,a) => (x, g a)

You can read about these features here and here.

I implore you to have mercy on your users/readers and consider not giving the type parameter the same name as the class.

[Chris Bailey]

Also I think if you use this in context, where the type can be inferred, you might not need either.

[corrededCrustacean]

Thank you, indeed both methods you proposed work!