lens.agda

{-# OPTIONS --safe --without-K #-}

module Bits where

infixr 4 _×_ _,_
record _×_ (A : Set) (B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

data _+_ (A : Set) (B : Set) : Set where
  inl : A → A + B
  inr : B → A + B

record Lens (S : Set) (T : Set) (A : Set) (B : Set) : Set₁ where
  field
    X : Set
    Y : X → Set
    viewˡ : X → S
    viewʳ : X → A
    updateˡ : (x : X) → T → Y x
    updateʳ : (x : X) → B → Y x
open Lens

compose : ∀ {S T A B P Q} → Lens S T A B → Lens A B P Q → Lens S T P Q
compose xs ys .X = xs .X × ys .X
compose xs ys .Y (x , y) = xs .Y x + ys .Y y
compose xs ys .viewˡ (x , y) = xs .viewˡ x
compose xs ys .viewʳ (x , y) = ys .viewʳ y
compose xs ys .updateˡ (x , y) t = inl (xs .updateˡ x t)
compose xs ys .updateʳ (x , y) t = inr (ys .updateʳ y t)