Implementing functor for a Type -> N -> Type

Stream: general

[Ricardo Prado Cunha]

I have a type tuple (α : Type u) : ℕ → Type u and would like to implement functor on it. I already have definitions for map and map_const, but the instance statement keeps giving me errors due to a type mismatch. This seems to be because functor requires it to be a Type -> Type and the extra ℕ argument is causing issues. I've tried using a lambda to fix this, but Lean also complains about that since the name is not provided explicitly. Is there any way around this other than changing to tuple : ℕ → Type u → Type u? I can't seem to find an instance of functor for core.vector, which is basically the same as tuple (other than the fact that tuple works with the inductive definition directly rather than using a list internally), so this gives me doubt.

[Ricardo Prado Cunha]

Here's a MWE:

universes u v

inductive tuple (α : Type u) : ℕ → Type u
| nil : tuple 0
| cons {n : ℕ} (head : α) (tail : tuple n) : (tuple (n + 1))

open tuple

variables {α : Type u} {β : Type v}

def map : ∀ {n : ℕ}, (α → β) → tuple α n → tuple β n
| 0 _ _ := nil
| _ f (cons head tail) := cons (f head) (map f tail)

def map_const {n : ℕ} (x : α) : tuple β n → tuple α n := map (λ b, x)

instance {n : ℕ} : functor (λ γ, tuple γ n) := ⟨map, map_const⟩ -- doesn't work

[Anatole Dedecker]

Can't you just swap the arguments? That is your tuple becomes tuple' and then tuple n α := tuple' α n. Then you can state that each tuple n is a functor.

[Ricardo Prado Cunha]

Anatole Dedecker said:

Can't you just swap the arguments? That is your tuple becomes tuple' and then tuple n α := tuple' α n. Then you can state that each tuple n is a functor.

That does work, but then I can only use things like <$> with tuple' and not with regular tuple. Implementing cast between the two would probably help, but it would still be quite cumbersome.

[Jason Rute]

If your #xy is just to use <$> with your type, then you may consider switching to lean 4 and using the new |> notation. Instead of f <$> v you write v |>.map f. You can also chain them together, like v |>.map f |>.map (· + 1) |>.last.

[Jason Rute]

It’s a more flexible notation which doesn’t require type classes or hard-to-read symbols.

[Ricardo Prado Cunha]

The arguments to switch to lean4 get better each day... I might have to do that soon.