Applying a pair of functions to a pair of values

Stream: lean4

[Markus Schmaus]

Is there a canonical way to apply a pair of functions to a pair of values?

def f (a : Nat) : Nat := a + 1

def g (a : String) : String := "hello " ++ a

#eval (g, f) ("world", 0) -- doesn't work
#eval (g, f) <*> ("world", 0) -- doesn't work

[Yaël Dillies]

docs#Prod.map

[Notification Bot]

Markus Schmaus has marked this topic as resolved.

[Notification Bot]

Markus Schmaus has marked this topic as unresolved.

[Markus Schmaus]

Thanks for the quick reply, but this isn't quite what I was looking for. Prod.map expects the two functions as individual values, but it can't handle the pair (g, f):

def f (a : Nat) : Nat := a + 1
def g (a : String) : String := "hello " ++ a

#eval Prod.map (g, f) ("world", 0) -- doesn't work
#eval Prod.map g f ("world", 0) -- intended use

[Yaël Dillies]

Why do you care about providing the functions as a pair?

[Yaël Dillies]

If you really do, then you can use docs#Function.uncurry, as in Function.uncurry Prod.map (g, f) ("world", 0)

[Markus Schmaus]

I'm looking into products of Functors and I'm trying to decide whether it makes sense to use the existing Prod type or define my own structure from scratch.

[Yaël Dillies]

I'm not sure what that has to do with pairs of functions. Can you clarify?

[Eric Rodriguez]

I mean I guess this could be a Functor instance?

[Eric Rodriguez]

ah, no, only the boring one for Prod x x

[Kyle Miller]

(@Yaël Dillies You can make a category whose object type is Type × Type and whose morphism type for (α, β) ⟶ (α', β') is (α → α') × (β → β').)

[Yaël Dillies]

Yeah but that's only useful in a categorical setting, no?

[Kyle Miller]

@Markus Schmaus If you're hoping to restrict to only functions that come from pairs, I think you're out of luck with Functor, since it allows any Type* -> Type* function, not just the ones that would respect cartesian products.

One thing you could do is create a CoeFun coercion to make tuples of functions be able to be used as functions:

instance {α β α' β' : Type _} : CoeFun ((α → β) × (α' → β')) (fun _ => α × α' → β × β') where
  coe := Function.uncurry Prod.map

def f (a : Nat) : Nat := a + 1

def g (a : String) : String := "hello " ++ a

#eval (g, f) ("world", 0)

[Kyle Miller]

Though using the uncurried Prod.map seems more reliable:

def Prod.map' {α β α' β' : Type _} (f : (α → β) × (α' → β')) : α × α' → β × β' :=
  Prod.map f.1 f.2

#eval Prod.map' (g, f) ("world", 0)
#eval (g, f).map' ("world", 0)

[Markus Schmaus]

It's quite easy to create what I want as a new structure:

structure ProductF (F₁ : Type u → Type v) (F₂ : Type u → Type w) (α : Type u) : Type (max v w) where
  fst : F₁ α
  snd : F₂ α

instance ProductF.instFunctor {F₁ : Type u → Type v} [Functor F₁] {F₂ : Type u → Type w} [Functor F₂] :
    Functor (ProductF F₁ F₂) where
  map := fun {α β : Type u} (f : α → β) (x : ProductF F₁ F₂ α) =>
    ⟨f <$> x.fst, f <$> x.snd⟩

Of course since this is a new structure, none of the lemmas in Lean or Mathlib apply to it. So I was wondering if I could build this up using pre-existing constructions, which already have some lemmas proven about them. Based on notation I know from category theory, I would have written this as (F₁, F₁) ο Δ, where Δ is the diagonal map x ↦ (x, x). But since this doesn't seem to translate to Lean, the above construction works fine.

[Kyle Miller]

By the way, the following will do for the instance:

instance {F₁ : Type u → Type v} [Functor F₁] {F₂ : Type u → Type w} [Functor F₂] :
    Functor (ProductF F₁ F₂) where
  map f x := ⟨f <$> x.fst, f <$> x.snd⟩

You could keep the fun, but you can omit the implicit arguments and the types.

[Kyle Miller]

You can also reuse Prod using a sort of type synonym that's opaque to typeclass inference.

def ProdF (F₁ : Type u → Type v) (F₂ : Type u → Type w) (α : Type u) : Type (max v w) :=
  F₁ α × F₂ α

instance {F₁ : Type u → Type v} [Functor F₁] {F₂ : Type u → Type w} [Functor F₂] :
    Functor (ProdF F₁ F₂) where
  map f := Prod.map (f <$> ·) (f <$> ·)

[Kyle Miller]

With (F₁, F₁) ο Δ, I'm not exactly sure what(F₁, F₁) means. It seems like it would be a functor for the product category Type u × Type u? That's what I was sort of referring to earlier -- Functor doesn't let you deal with any category but Type u. There's a category theory library with its own notion of functor that should let you express this, but it's not connected to Functor, which is more for programming.