https://www.codewars.com/kata/54258ffb430ca2e4b5000239/train/haskell

MicroLens.agda

module MicroLens where

open import Function using (id; _∘_)
open import Data.Sum using (_⊎_) renaming (inj₁ to inl; inj₂ to inr)

record Profunctor (P : Set → Set → Set) : Set₁ where
  field
    dimap : ∀ {a' a b b'} → (a' → a) → (b → b') → P a b → P a' b'

  lmap : ∀ {a' a b} → (a' → a) → P a b → P a' b
  lmap f = dimap f id

  rmap : ∀ {a b b'} → (b → b') → P a b → P a b'
  rmap f = dimap id f

open Profunctor {{...}} public

record Choice (P : Set → Set → Set) {{_ : Profunctor P}} : Set₁ where
  field
    left  : ∀ {a b c} → P a b → P (a ⊎ c) (b ⊎ c)
    right : ∀ {a b c} → P a b → P (c ⊎ a) (c ⊎ b)

open Choice {{...}} public

_⇒_ : Set → Set → Set
A ⇒ B = A → B

either : ∀ {A B C : Set} → (A → C) → (B → C) → (A ⊎ B) → C
either ac _ (inl a) = ac a
either _ bc (inr b) = bc b

instance
  Arrow-Profunctor : Profunctor _⇒_
  Arrow-Profunctor = record { dimap = λ f g h → g ∘ h ∘ f }

  Arrow-Choice : Choice _⇒_
  Arrow-Choice = record
    { left  = λ f → either (inl ∘ f) inr
    ; right = λ f → either inl (inr ∘ f)
    }

record Covariant (F : Set → Set) : Set₁ where
  field
    comap : ∀ {a a' : Set} → (a → a') → F a → F a'

open Covariant {{...}} public

record Contravariant (F : Set → Set) : Set₁ where
  field
    contramap : ∀ {a' a : Set} → (a' → a) → F a → F a'

open Contravariant {{...}} public

record Applicative (F : Set → Set) {{_ : Covariant F}} : Set₁ where
  field
    pure : ∀ {a} → a → F a
    _<*>_ : ∀ {a b} → F (a → b) → F a → F b

  _*>_ : ∀ {a b} → F a → F b → F b
  _*>_ _ fb = fb

  _<*_ : ∀ {a b} → F a → F b → F a
  _<*_ fa _ = fa

open Applicative {{...}} public

record Monoid (A : Set) : Set where
  field
    unit : A
    _<>_ : A → A → A

open Monoid {{...}} public

record Id (A : Set) : Set where
  constructor mk-id
  field
    get-id : A

open Id {{...}} public

record Const (B A : Set) : Set where
  constructor mk-const
  field
    get-const : B

open Const {{...}} public

instance
  Covariant-Id : Covariant Id
  Covariant-Id = record { comap = λ { f (mk-id a) → mk-id (f a) } }

  Applicative-Id : Applicative Id
  Applicative-Id = record
    { pure = mk-id
    ; _<*>_ = λ { (mk-id f) (mk-id x) → mk-id (f x) }
    }

  Covariant-Const : ∀ {B} → Covariant (Const B)
  Covariant-Const = record { comap = λ { _ (mk-const b) → mk-const b } }

  Contravariant-Const : ∀ {B} → Contravariant (Const B)
  Contravariant-Const = record { contramap = λ { _ (mk-const b) → mk-const b } }

  Applicative-Const : ∀ {B} → {{_ : Monoid B}} → Applicative (Const B)
  Applicative-Const = record
    { pure = λ _ → mk-const unit
    ; _<*>_ = λ { (mk-const ba) (mk-const bb) → mk-const (ba <> bb) }
    }

Optic : (Set → Set → Set) → (Set → Set) → Set → Set → Set → Set → Set
Optic P F s t a b = P a (F b) → P s (F t)

Iso : Set → Set → Set → Set → ∀ {P F} → {{_ : Profunctor P}} → {{_ : Covariant F}} → Set
Iso s t a b {P} {F} = Optic P F s t a b

Lens : Set → Set → Set → Set → ∀ {F} → {{_ : Covariant F}} → Set
Lens s t a b {F} = Optic _⇒_ F s t a b

Traversal : Set → Set → Set → Set → ∀ {F} → {{_ : Covariant F}} → {{_ : Applicative F}} → Set
Traversal s t a b {F} = Optic _⇒_ F s t a b

Fold : Set → Set → ∀ {F} → {{_ : Contravariant F}} → {{_ : Covariant F}} → {{_ : Applicative F}} → Set
Fold s a {F} = Optic _⇒_ F s s a a

Prism : Set → Set → Set → Set → ∀ {P F} → {{_ : Profunctor P}} → {{_ : Choice P}} → {{_ : Covariant F}} → {{_ : Applicative F}} → Set
Prism s t a b {P} {F} = Optic P F s t a b