Changing the functor typeclasses

Stream: general

[Eric Wieser]

(I split this to a new thread)

[Yaël Dillies]

How is it going?

[Yaël Dillies]

Something I noticed is that multiset does not have a docs#traversable instance because it does not commute with all applicative functors, but only all commutative applicative functors. data.multiset.functor currently contains the guts of what could be traversable multiset where it not for this problem. Should we thus change traversableto take in a specific functor?

[Reid Barton]

It's not really a problem. traversable is about things you can iterate over in a fixed order, multiset doesn't have an order, so there is no traversable multiset--that's just the way it is.

[Eric Wieser]

Eric Wieser said:

I explored this a little more in branch#eric-wieser/monad-universes, all the way up to applicative

For future reference, I was able to translate this to Lean 4 using default_instance:

Lean 4 version

import Mathlib.Data.List.Monad
import Mathlib.Tactic.TypeStar
import Mathlib.Data.Finset.Functor
import Mathlib.Data.Finset.Sort

open Function (const)

class IsMonadic (α : outParam Type*) (fα : Type*) : Prop

class Functor' {α β : outParam Type*} (fα fβ : Type*) [IsMonadic α fα] [IsMonadic β fβ] where
  map : (α → β) → fα → fβ
  mapConst : β → fα → fβ := map ∘ Function.const α

infixr:100 (priority := high) " <$> " => Functor'.map
infixr:100 (priority := high) " <$ "  => Functor'.mapConst

@[reducible] def Functor'.mapConst_rev {α β : outParam Type*} (fα fβ : Type*)
    [IsMonadic α fα] [IsMonadic β fβ]
    [Functor' fα fβ] : fα → β → fβ :=
  fun a b => b <$ a
infixr:100 (priority := high) " $> "  => Functor'.mapConstRev

class Pure' {α : outParam Type*} (fα : Type*) [IsMonadic α fα] where
  pure : α → fα

export Pure' (pure)

class Seq' {α β : outParam Type*} (fαβ : outParam Type*)
    (fα fβ : Type*) [IsMonadic α fα] [IsMonadic β fβ]
    [IsMonadic (α → β) fαβ] where
  seq : fαβ → (Unit → fα) → fβ


class SeqLeft' {α β : outParam Type*} (fα fβ : Type*) [IsMonadic α fα] [IsMonadic β fβ] where
  seqLeft : fβ → (Unit → fα) → fβ


class SeqRight' {α β : outParam Type*} (fα fβ : Type*) [IsMonadic α fα] [IsMonadic β fβ] where
  seqRight : fα → (Unit → fβ) → fβ

attribute [inherit_doc SeqLeft.seqLeft] SeqLeft'.seqLeft
attribute [inherit_doc SeqRight.seqRight] SeqRight'.seqRight

@[inherit_doc Seq.seq]           syntax:60 (priority := high) term:60 " <*> " term:61 : term
@[inherit_doc SeqLeft.seqLeft]   syntax:60 (priority := high) term:60 " <* " term:61 : term
@[inherit_doc SeqRight.seqRight] syntax:60 (priority := high) term:60 " *> " term:61 : term
macro_rules | `($x <*> $y) => `(Seq'.seq (fα := type_of% $y) $x fun _ : Unit => $y)
macro_rules | `($x <* $y)  => `(SeqLeft'.seqLeft (fα := type_of% $y) $x fun _ : Unit => $y)
macro_rules | `($x *> $y)  => `(SeqRight'.seqRight (fβ := type_of% $y) $x fun _ : Unit => $y)

class Applicative' {α β : outParam Type*} (fαβ fββ : outParam Type*) (fα fβ : Type*)
    [IsMonadic α fα] [IsMonadic β fβ]
    [IsMonadic (α → β) fαβ] [IsMonadic (β → β) fββ]
    extends Functor' fα fβ, Pure' fαβ, Seq' fαβ fα fβ, SeqLeft' fα fβ, SeqRight' fα fβ where
  map x y := (pure x : fαβ) <*> y

def Applicative'.mk' {α β : Type*} {fαβ fββ : Type*} {fα fβ : Type*}
    [IsMonadic α fα] [IsMonadic β fβ]
    [IsMonadic (α → β) fαβ] [IsMonadic (β → β) fββ]
    [Pure' fαβ] [i : Seq' fαβ fα fβ]
    [toFunctor₂ : Functor' fβ fαβ]
    [toFunctor₃ : Functor' fα fββ]
    [toSeq₂ : Seq' fββ fβ fβ] : Applicative' fαβ fββ fα fβ where
  seqLeft  b a := Seq'.seq (const α <$> b) a
  seqRight a b := Seq'.seq (const α id <$> a) b

namespace List
instance {α : Type*} : IsMonadic α (List α) := IsMonadic.mk

@[default_instance]
instance {α : Type*} : Pure' (List α) where
  pure := ([·])

@[default_instance]
instance {α β : Type*} : Functor' (List α) (List β) where
  map := List.map

@[default_instance]
instance {α β : Type*} : Seq' (List (α → β)) (List α) (List β) where
  seq f a := f.flatMap (fun g => (a ()).map g)

@[default_instance]
instance {α β : Type*} : Applicative' (List (α → β)) (List (β → β)) (List α) (List β) := .mk'
end List

namespace Array

instance {α : Type*} : IsMonadic α (Array α) := IsMonadic.mk

@[default_instance]
instance {α : Type*} : Pure' (Array α) where
  pure := (#[·])

@[default_instance]
instance {α β : Type*} : Functor' (Array α) (Array β) where
  map := Array.map

@[default_instance]
instance {α β : Type*} : Seq' (Array (α → β)) (Array α) (Array β) where
  seq f a := f.flatMap (fun g => (a ()).map g)

@[default_instance]
instance {α β : Type*} : Applicative' (Array (α → β)) (Array (β → β)) (Array α) (Array β) := .mk'

end Array

namespace Finset

instance {α : Type*} : IsMonadic α (Finset α) := IsMonadic.mk

@[default_instance]
instance {α β : Type*} [DecidableEq β] : Functor' (Finset α) (Finset β) where
  map := Finset.image

@[default_instance]
instance {α β : Type*} [DecidableEq β] : Seq' (Finset (α → β)) (Finset α) (Finset β) where
  seq f a := f.biUnion (fun g => (a ()).image g)

@[default_instance]
instance {α : Type*} : Pure' (Finset α) where
  pure := ({·})

@[default_instance]
instance {α β : Type*} [DecidableEq β] :
    Applicative' (Finset (α → β)) (Finset (β → β)) (Finset α) (Finset β) where
  seqLeft s t := if (t ()).card = 0 then ∅ else s
  seqRight s t := if s.card = 0 then ∅ else t ()

end Finset

which has test-case

#eval ([ULift.up.{32}] <*> [1, 2, 3])
#eval (ULift.up.{32} <$> [1, 2, 3])
#eval (#[ULift.up.{32}] <*> #[1, 2, 3])
#eval (ULift.up.{32} <$> #[1, 2, 3])
#eval (({ULift.up.{32}} : Finset _) <*> ({1, 2, 3} : Finset Nat))
#eval (ULift.up.{32} <$> ({1, 2, 3} : Finset Nat))