feat: profunctor optics

Mathlib.lean

@@ -2,7 +2,11 @@ import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Algebra.Ring.Basic
+import Mathlib.Control.Basic
+import Mathlib.Control.Optics
+import Mathlib.Control.Profunctor
 import Mathlib.Control.Random
+import Mathlib.Control.Traversable
 import Mathlib.Control.Writer
 import Mathlib.Data.Array.Basic
 import Mathlib.Data.Array.Defs
@@ -24,6 +28,7 @@ import Mathlib.Data.Prod
 import Mathlib.Data.String.Defs
 import Mathlib.Data.String.Lemmas
 import Mathlib.Data.Subtype
+import Mathlib.Data.Sum
 import Mathlib.Data.UInt
 import Mathlib.Data.UnionFind
 import Mathlib.Init.Algebra.Functions

Mathlib/Control/Basic.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2022 E.W.Ayers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: E.W.Ayers
+-/
+
+/-- `Const κ α = κ`. The constant functor with value `κ`. -/
+def Const (κ : Type u) (_α : Type v) : Type u := κ
+
+namespace Const
+
+instance : Functor (Const κ) where
+  map _ k := k
+
+/-!
+# Using const as a writer.
+
+If we think of `κ` as a monoid then there is a nice applicative structure that
+we can add to it. You can interpret the applicative structure as returning the
+product of all of the `κ`s.
+
+As with `WriterT`, `∅, ++` is preferred to `1, *` as the monoid.
+-/
+
+instance [EmptyCollection κ] : Pure (Const κ) where
+  pure _ := (∅ : κ)
+
+instance [EmptyCollection κ] [Append κ] : Applicative (Const κ) where
+  seq (f : κ) (x : Unit → κ) := f ++ x ()
+
+end Const
+
+/-- AKA `Copure`. -/
+class Extract (F : Type u → Type v) where
+  extract {α} : F α → α
+
+export Extract (extract)
+
+/-- AKA `Cobind`. -/
+class Extend (F : Type u → Type v) where
+  extend {α β} : (F α → β) → F α → F β
+
+class Comonad (F : Type u → Type v) extends Extract F, Extend F

Mathlib/Control/Optics.lean

@@ -0,0 +1,182 @@
+/-
+Copyright (c) 2022 E.W.Ayers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: E.W.Ayers
+-/
+import Mathlib.Control.Profunctor
+import Mathlib.Data.Prod
+import Mathlib.Control.Traversable
+/-!
+# Profunctor optics
+Definitions of profunctor optics.
+
+One way to think about profunctor optics is to look at traversal:
+
+```
+traverse : (f : α → M β) → (l : List α) → M (List β)
+```
+
+`traverse` selects all the objects in `l` and performs `f` to them under
+the monad `M`, then wraps all these up back in to a list.
+
+Optics generalise this notion of unpacking a datastructure, performing some arbitrary action and then repackaging the datastructure.
+Let's define `P α β := α → M β`, then we have `traverse : P α β → P (List α) (List β)`.
+
+
+### References:
+- https://hackage.haskell.org/package/profunctor-optics-0.0.2/docs/index.html
+- https://dl.acm.org/doi/pdf/10.1145/3236779
+- https://golem.ph.utexas.edu/category/2020/01/profunctor_optics_the_categori.html
+- http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/poptics.pdf
+- https://github.com/hablapps/DontFearTheProfunctorOptics
+-/
+
+namespace Control
+
+open Profunctor
+
+set_option checkBinderAnnotations false in
+/-- A general profunctor optic. -/
+def Optic (π : (Type u → Type u → Type v) → Type w) (α β σ τ : Type u) :=
+  ∀ ⦃P⦄ [π P], P α β → P σ τ
+
+namespace Optic
+
+def Iso := Optic Profunctor
+
+def Lens               := Optic Strong
+def Lens' (α β)        := Lens α α β β
+
+def Prism              := Optic Choice
+def Prism' (α β)       := Prism α α β β
+
+/-- Also known as an affine traversal or a traversal0.
+
+I am going off-book here and calling it "modification" because that is what it is doing.
+You can also think of it as a `Traversal` where the inner profunctor is 'called' at most once.
+ -/
+def Modification            := Optic Affine
+def Modification' (α β)     := Modification α α β β
+
+def Traversal          := Optic Traversing
+
+def Setter := Optic Mapping
+
+def Grate := Optic Closed
+
+variable {α β σ τ χ : Type u}
+
+namespace Iso
+  def mk (g : σ → α) (f : β → τ) : Iso α β σ τ
+  | _, _, p => Profunctor.dimap g f p
+end Iso
+
+namespace Lens
+  def mk (g : σ → α) (s : β → σ → τ) : Lens α β σ τ
+  | _, _, f => dimap (Prod.intro g id) (Prod.elim s) $ first σ $ f
+
+  def view (l : Lens α β σ τ) : σ → α :=
+    let p : Star (Const α) α β := id
+    l p
+
+  def update (l : Lens α β σ τ) (b : β) (s : σ) : τ :=
+    let p : Star (Reader β) α β := fun _ b => b
+    l p s b
+
+  def matching (sca : σ → γ × α) (cbt : γ × β → τ) : Lens α β σ τ :=
+  mk (Prod.snd ∘ sca) (fun b s => cbt (Prod.fst $ sca s,b))
+
+  protected def id : Lens α β α β := mk (λ a => a) (λ b _ => b)
+
+end Lens
+
+
+namespace Prism
+
+  def view (p : Prism α β σ τ) : σ → τ ⊕ α :=
+    let f : Star (Sum α) α β := Sum.inl
+    Sum.swap ∘ p f
+
+  -- [todo] there will be a more general form but not sure what it is.
+  private instance : Choice (Costar (Const β)) := {
+      left := fun _ fab b => Sum.inl <| fab b,
+      right := fun _ fab b => Sum.inr <| fab b,
+    }
+
+  def update (p : Prism α β σ τ) : β → τ :=
+    let f : Costar (Const β) α β := id
+    p f
+
+  def mk (g : σ → τ ⊕ α) (s : β → τ) : Prism α β σ τ
+    | _, _, f => dimap g (Sum.elim id s) $ right _ $ f
+
+end Prism
+
+namespace Modification
+
+  def mk (f : σ → τ ⊕ α) (g : σ → β → τ) : Modification α β σ τ
+    | _, _, p => dimap (Prod.intro id f) (Function.uncurry $ Sum.elim id ∘ g) $ second σ $ right τ p
+
+end Modification
+
+namespace Grate
+
+  def Concrete (α β σ τ : Type u) := ((σ → α) → β) → τ
+  instance : Closed (Concrete α β) where
+    dimap := fun yx st g yab => st $ g $ fun xa => yab $ xa ∘ yx
+    close := fun _ g f s => g <| fun i => f <| fun j => i <| j s
+
+  protected def mk (f : ((σ → α) → β) → τ) : Grate α β σ τ
+    | _, _, p => dimap (fun a s => s a) f (close (σ → α) p)
+
+  def run (g : Grate α β σ τ) : ((σ → α) → β) → τ :=
+    let o : Concrete α β α β := fun x => x id
+    g o
+
+  def zipWith {F : Type u → Type u} [Functor F] : Grate α β σ τ → (F α → β) → (F σ → τ)
+    | g, c => show Costar F σ τ by exact g c
+
+  def zip2:  Grate α β σ τ  → (α → α → β) → σ → σ → τ
+    | g, p =>
+      let p : Costar Prod.Square α β := Function.uncurry p
+      Function.curry $ g $ p
+
+  def distributed [Functor F] [Distributive F] : Grate α β (F α) (F β) :=
+    Grate.mk fun k => k <$> Distributive.distReader id
+
+  def endomorphed (χ : Type u) : Grate α α (χ → α) (χ → α)
+    | _, _, p => close _ p
+
+end Grate
+
+def traversing (F) [Traversable F] : Traversal σ τ (F σ) (F τ)
+| _, t => Representable.lift (@traverse _ _ _ t.a _ _)
+
+def arrays (t : Traversal α β σ τ) : σ → Array α :=
+  let f : Star (Const (Array α)) α β := fun a => #[a]
+  t f
+
+def united : Lens PUnit PUnit α α :=
+  Lens.mk (fun _ => PUnit.unit) (fun _ a => a)
+
+def voided : Lens α α PEmpty PEmpty :=
+  Lens.mk (fun e => by cases e) (fun _ e => e)
+
+def fst : Lens α β (α × χ) (β × χ) :=
+  Lens.mk Prod.fst (fun b (_,x) => (b,x))
+
+def snd : Lens α β (χ × α) (χ × β) :=
+  Lens.mk Prod.snd (fun b (x,_) => (x,b))
+
+def the : Prism α β (Option α) (Option β) :=
+  Prism.mk (fun | none => Sum.inl none | some a => Sum.inr a) some
+
+def both : Traversal α β (α × α) (β × β) :=
+  traversing Prod.Square
+
+def never : Prism PEmpty PEmpty α α :=
+  Prism.mk Sum.inl (fun x => by cases x)
+
+end Optic
+
+end Control

Mathlib/Control/Profunctor.lean

@@ -0,0 +1,152 @@
+/-
+Copyright (c) 2022 E.W.Ayers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: E.W.Ayers
+-/
+import Mathlib.Data.Sum
+import Mathlib.Data.Equiv.Basic
+import Mathlib.Control.Basic
+import Mathlib.Control.Traversable
+
+/-!
+# Profunctors
+
+Definitions for (non-lawful) profunctors.
+
+-/
+
+/-- A profunctor `P` is a function `Type u → Type u → Type v` that is a functor
+on the second argument and a contravariant functor on the first.
+
+Reference: https://en.wikipedia.org/wiki/Profunctor
+ -/
+class Profunctor (P : Type u → Type v → Type w) where
+  dimap {α α' β β'} : (α' → α) → (β → β') → P α β → P α' β'
+
+export Profunctor (dimap)
+
+namespace Profunctor
+
+class StrongCore (P : Type u → Type u → Type v) where
+  first {α β : Type u} (χ : Type u) : P α β → P (α × χ) (β × χ)
+  second {α β : Type u} (χ : Type u) : P α β → P (χ × α) (χ × β)
+
+export StrongCore (first second)
+
+class ChoiceCore (P : Type u → Type u → Type v) where
+  left  {α β} (χ : Type u) : P α β → P (α ⊕ χ) (β ⊕ χ)
+  right {α β} (χ : Type u) : P α β → P (χ ⊕ α) (χ ⊕ β)
+
+export ChoiceCore (left right)
+
+class ClosedCore (P : Type u → Type u → Type v) where
+  close {α β} : ∀ (X : Type u), P α β → P (X → α) (X → β)
+
+export ClosedCore (close)
+
+class CostrongCore (P : Type u → Type u → Type v) where
+  unfirst  {α β : Type u} (χ : Type u) : P (α × χ) (β × χ) → P α β
+  unsecond {α β : Type u} (χ : Type u) : P (χ × α) (χ × β) → P α β
+
+class Affine (P : Type u → Type u → Type v) extends Profunctor P, StrongCore P, ChoiceCore P
+/-- A strong profunctor is one that 'plays nice' with products.-/
+class Strong (P : Type u → Type u → Type v) extends Profunctor P, StrongCore P
+class Costrong (P : Type u → Type u → Type v) extends Profunctor P, CostrongCore P
+/-- A strong profunctor is one that 'plays nice' with sums.-/
+class Choice (P : Type u → Type u → Type v) extends Profunctor P, ChoiceCore P
+class Closed (P : Type u → Type u → Type v) extends Profunctor P, ClosedCore P
+
+/-- `Star F α β = α → F β`-/
+def Star (F : Type u → Type v) (α : Type w) (β : Type u) :=
+  α → F β
+
+/-- `Costar F α β = F α → β`. -/
+def Costar (F : Type u → Type v) (α : Type u) (β :Type w) :=
+  F α → β
+
+/-- `Comma F G α β := F α → G β`. -/
+def Comma (F : Type u → Type v) (G : Type w → Type v) (α : Type u) (β : Type w) :=
+  F α → G β
+
+/-- A profunctor is representable when there is a functor `Rep` such there is a
+natural isomorphism between  `P α β` and `α → Rep β`.
+
+Contrast this with the definition of a representable functor `F`, where there is a `R : Type` such that `F α ≃ R → α`
+  -/
+class Representable (P : Type u → Type u → Type v) where
+  Rep : Type u → Type v
+  eqv {α β} : P α β ≃ Star Rep α β
+
+export Representable (Rep)
+
+/-- Sends an element of `P α β` to its representative `α → Rep P β`. Inverse of `Representable.tabulate` -/
+def Representable.sieve [Representable P] : P α β → (α → Rep P β) := Representable.eqv.toFun
+/-- Inverse of `Representable.sieve`.-/
+def Representable.tabulate [Representable P] : (α → Rep P β) → P α β := Representable.eqv.invFun
+
+/-- Lists a transform `f : Star Rep ⇒ Star Rep` to `P ⇒ P`-/
+def Representable.lift [Representable P] {α β σ τ}
+  (f : (α → Rep P β) → σ → Rep P τ) : P α β → P σ τ :=
+  tabulate ∘ f ∘ sieve
+
+/-- A traversing profunctor is a representable functor where `Rep` is applicative. -/
+class Traversing (P) extends (Representable P) where
+  [a : Applicative Rep]
+
+class Mapping (P) extends (Traversing P) where
+  [d : Distributive Rep]
+
+namespace Comma
+  variable {F : Type u → Type v} {G : Type w → Type v}
+
+  instance [Functor F] [Functor G] : Profunctor (Comma F G) where
+    dimap f g h a := g <$> h (f <$> a)
+end Comma
+
+-- [todo] generalise to Comma
+namespace Star
+
+  variable {F : Type u → Type v}
+
+  instance [Functor F] : Profunctor (Star F) :=
+    ⟨fun f g h a => g <$> (h $ f a)⟩
+    -- (show Profunctor (Comma Id F) by infer_instance) -- [todo] why doesn't this work?
+
+  instance [Pure F] [Functor F] : Choice (Star F) where
+    left  := fun _ afb => Sum.elim (Functor.map Sum.inl ∘ afb)  (Functor.map Sum.inr ∘ pure)
+    right := fun _ afb => Sum.elim (Functor.map Sum.inl ∘ pure) (Functor.map Sum.inr ∘ afb)
+
+  instance [Functor F] : Strong (Star F) where
+    first  := fun _ f (a,c) => (fun a => (a, c)) <$> f a
+    second := fun _ f (c,a) => (fun a => (c, a)) <$> f a
+
+  instance {F : Type u → Type u} : Representable (Star F) where
+    Rep := F
+    eqv := Equiv.refl _
+
+  instance [EmptyCollection ω] [Append ω] : Traversing (Star (Const ω)) :=
+    have a : Applicative (Const ω) := inferInstance
+    { a := a }
+
+end Star
+
+namespace Costar
+  variable {F : Type u → Type v}
+
+  instance [Functor F] : Closed (Costar F) where
+    dimap f g h a := g $ h $ f <$> a
+    close _ fab fxa x := fab $ (· x) <$> fxa
+
+end Costar
+
+def Yoneda (P : Type u → Type u → Type v) (α β : Type u) :=
+  ⦃φ χ : Type u⦄ → (φ → α) → (β → χ) → P φ χ
+
+namespace Yoneda
+
+  def extract : Yoneda P α β → P α β
+  | y => y id id
+
+end Yoneda
+
+end Profunctor