inference of conditional conformance with type classes

Stream: lean4

[Gabriel gomez]

Hi, I'm trying to learn more about category theory with Lean. I'm a software devloper. I learned a little of Haskell and I'm learning Lean 4 now. So, my question is in this code:

  class Functor (f : Type u → Type v)  where
    map : {α β : Type u} → (α → β) → f α → f β
    mapConst : {α β : Type u} → α → f β → f α :=
      λ a fb => map (λ _ => a) fb

  instance FunctorOption : Functor Option where
    map f fa := match fa with
    | some a => some (f a)
    | none => none
    mapConst a _ := a

  instance FunctorList : Functor List where
    map := List.map
    mapConst a _ := [a]

  instance FunctorProd {f g : Type u → Type v} [Functor f] [Functor g] : Functor (fun α => f α × g α) where
    map f fga := match fga with
    | (fa, ga) => (Functor.map f fa, Functor.map f ga)

  #eval FunctorProd.map (fun x => x + 1) ([1, 2, 3], some 4)
  #eval Functor.map (fun x => x + 1) ([1, 2, 3], some 4)

Why the first eval works but the second eval is not working? I'm getting this error on second eval:

x : Option Nat
failed to synthesize instance
Functor (Prod (List ?m.1074))Lean 4
failed to synthesize instance
HAdd (Option ?m.1080) Nat ?m.1001Lean 4

[Henrik Böving]

Looking at the typeclass trace Lean is not even trying to apply the prod instance because it is not understanding that the type on the right hand side can be interpreted as (fun α => List α × Option α) but instead ends up interpreting it as (Prod (List Nat)) where the rhs of the Prod type is the generic parameter of the functor.

But I'm not an expert on the implementation of this part of Lean so I cannot tell you whether we want this to work out in the way you expect. @Gabriel Ebner is this something the type inference should be able to detect correctly?

[James Gallicchio]

(deleted)

[James Gallicchio]

If you give it a unification nudge it compiles:

  #eval Functor.map (f := fun α => List α × Option α) (fun x => x + 1) ([1, 2, 3], some 4)

But yeah, can't give more insight into which syntactic forms do/don't get explored

[Reid Barton]

We can see what you had in mind but Lean tries to guess what f should be before it looks at what instances there are--so it's not that likely to get it right, as there is little for it to go on.

[Reid Barton]

This is a "higher-order unification problem": Lean needs to guess f but all it knows is f Nat (in fact, it doesn't even know yet that the argument should be Nat).

[James Gallicchio]

Another potentially interesting alternative formulation:

  class Functor (f : Type u → Type v)  where
    map : {α β : Type u} → (α → β) → f α → f β
    mapConst : {α β : Type u} → α → f β → f α :=
      λ a fb => map (λ _ => a) fb

  instance FunctorOption : Functor Option where
    map f fa := match fa with
    | some a => some (f a)
    | none => none
    mapConst a _ := a

  instance FunctorList : Functor List where
    map := List.map
    mapConst a _ := [a]

  def FProd (f g : Type u → Type v) := fun α => f α × g α

  def FProd.mk {f g : Type u → Type v} (fa : f α) (ga : g α) : FProd f g α := (fa,ga)

  instance FunctorFProd {f g : Type u → Type v} [Functor f] [Functor g] : Functor (FProd f g) where
    map f fga := match fga with
    | (fa, ga) => (Functor.map f fa, Functor.map f ga)

  #eval FunctorProd.map (fun x => x + 1) ([1, 2, 3], some 4)
  #eval Functor.map (fun x => x + 1) (FProd.mk [1, 2, 3] (some 4))

this is much more reflective of how typeclass inference is ""intended"" to be used, where your types have a nice head term (here FProd)

[Reid Barton]

Note that e.g. f a = List a \x Option Nat is also a functor, that will have a different result for Functor.map (fun x => x + 1).

[Reid Barton]

(You don't have that instance yet, but you could.)

[Gabriel gomez]

James Gallicchio said:

Another potentially interesting alternative formulation:

  class Functor (f : Type u → Type v)  where
    map : {α β : Type u} → (α → β) → f α → f β
    mapConst : {α β : Type u} → α → f β → f α :=
      λ a fb => map (λ _ => a) fb

  instance FunctorOption : Functor Option where
    map f fa := match fa with
    | some a => some (f a)
    | none => none
    mapConst a _ := a

  instance FunctorList : Functor List where
    map := List.map
    mapConst a _ := [a]

  def FProd (f g : Type u → Type v) := fun α => f α × g α

  def FProd.mk {f g : Type u → Type v} (fa : f α) (ga : g α) : FProd f g α := (fa,ga)

  instance FunctorFProd {f g : Type u → Type v} [Functor f] [Functor g] : Functor (FProd f g) where
    map f fga := match fga with
    | (fa, ga) => (Functor.map f fa, Functor.map f ga)

  #eval FunctorProd.map (fun x => x + 1) ([1, 2, 3], some 4)
  #eval Functor.map (fun x => x + 1) (FProd.mk [1, 2, 3] (some 4))

this is much more reflective of how typeclass inference is ""intended"" to be used, where your types have a nice head term (here FProd)

So, I need that additional indirection level. The nice head term (like FProd) is nice because... it doesn't have a type lambda as parameter on the instance?

P.D. Thanks you, it worked!

[James Gallicchio]

Yeah -- it's an application FProd List Option instead of a lambda abstraction (even though it reduces to a lambda) so typeclass search will look for an FProd instance instead of having to solve a higher order unification problem :)

[Sebastian Ullrich]

?f ?A =?= FProd List Option Nat is still a HO unification problem, like the original ?f ?A =?= Prod (List Nat) (Option Nat) (note that there are no lambdas yet at this point, as we don't even get to the instance). As these problems are outside of the HO pattern fragment, Lean falls back to first-order unification ?f =?= FProd List Option, ?A =?= Nat and ?f =?= Prod (List Nat), ?A =?= Option Nat. So basically for functors you want to make sure that the type parameter occurs exactly once as the last argument.