------------------------------------------------------------------------
-- Comparisons of different kinds of lenses, focusing on the
-- definition of composable record setters and getters
------------------------------------------------------------------------

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

-- This module uses both dependent and non-dependent lenses, in order
-- to illustrate a problem with the non-dependent ones. It also uses
-- two kinds of dependent lenses, in order to illustrate a minor
-- problem with one of them.

module README.Record-getters-and-setters where

open import Equality.Propositional
open import Prelude hiding (_∘_)

open import Bijection equality-with-J as Bij using (_↔_; module _↔_)
open import Equality.Decision-procedures equality-with-J
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J as F hiding (_∘_)

import Lens.Dependent
import Lens.Non-dependent.Alternative

------------------------------------------------------------------------
-- Dependent lenses with "remainder types" visible in the type

module Dependent₃ where

  open Lens.Dependent

  -- Nested records.

  record R₁ (A : Set) : Set where
    field
      f     : A  A
      x     : A
      lemma :  y  f y  y

  record R₂ : Set₁ where
    field
      A  : Set
      r₁ : R₁ A

  -- Lenses for each of the three fields of R₁.

  -- The x field is easiest, because it is independent of the others.
  --
  -- (Note that the from function is inferred automatically.)

  x : {A : Set} 
      Lens₃ (R₁ A) ( λ (f : A  A)   y  f y  y)  _  A)
  x = Eq.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to   = λ r  (R₁.f r , R₁.lemma r) , R₁.x r
        ; from = _
        }
      ; right-inverse-of = λ _  refl
      }
    ; left-inverse-of = λ _  refl
    })

  -- The lemma field depends on the f field, so whenever the f field
  -- is set the lemma field needs to be updated as well.

  f : {A : Set} 
      Lens₃ (R₁ A) A  _   λ (f : A  A)   y  f y  y)
  f = Eq.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to   = λ r  R₁.x r , (R₁.f r , R₁.lemma r)
        ; from = _
        }
      ; right-inverse-of = λ _  refl
      }
    ; left-inverse-of = λ _  refl
    })

  -- The lemma field can be updated independently.

  lemma : {A : Set} 
          Lens₃ (R₁ A) (A × (A  A))  r   y  proj₂ r y  y)
  lemma = Eq.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to   = λ r  (R₁.x r , R₁.f r) , R₁.lemma r
        ; from = _
        }
      ; right-inverse-of = λ _  refl
      }
    ; left-inverse-of = λ _  refl
    })

  -- Note that the type of the last lens may not be quite
  -- satisfactory: the type of the lens does not guarantee that the
  -- lemma applies to the input's f field. The following lemma may
  -- provide some form of consolation:

  consolation : {A : Set} (r : R₁ A)   y  R₁.f r y  y
  consolation = Lens₃.get lemma

  -- Let us now construct lenses for the same fields, but accessed
  -- through an R₂ record.

  -- First we define lenses for the fields of R₂ (note that the A lens
  -- does not seem to be very useful):

  A : Lens₃ R₂   _  R₂)
  A = id₃

  r₁ : Lens₃ R₂ Set R₁
  r₁ = Eq.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to   = λ r  R₂.A r , R₂.r₁ r
        ; from = _
        }
      ; right-inverse-of = λ _  refl
      }
    ; left-inverse-of = λ _  refl
    })

  -- The lenses for the three R₁ fields can now be defined by
  -- composition:

  x₂ : Lens₃ R₂ _  r  proj₁ r)
  x₂ = x ₃∘₃ r₁

  f₂ : Lens₃ R₂ _  r   λ (f : proj₁ r  proj₁ r)   y  f y  y)
  f₂ = f ₃∘₃ r₁

  lemma₂ : Lens₃ R₂ _  r   y  proj₂ (proj₂ r) y  y)
  lemma₂ = lemma ₃∘₃ r₁

  consolation₂ : (r : R₂)   y  proj₁ (Lens₃.get f₂ r) y  y
  consolation₂ = Lens₃.get lemma₂

------------------------------------------------------------------------
-- Dependent lenses without "remainder types" visible in the type

module Dependent where

  open Lens.Dependent
  open Dependent₃ using (R₁; module R₁; R₂; module R₂)

  -- Lenses for each of the three fields of R₁.

  x : {A : Set}  Lens (R₁ A)  _  A)
  x = Lens₃-to-Lens Dependent₃.x

  f : {A : Set}  Lens (R₁ A)  _   λ (f : A  A)   y  f y  y)
  f = Lens₃-to-Lens Dependent₃.f

  lemma : {A : Set}  Lens (R₁ A)  r   y  R₁.f r y  y)
  lemma = Lens₃-to-Lens Dependent₃.lemma

  -- Note that the type of lemma is now more satisfactory: the type of
  -- the lens /does/ guarantee that the lemma applies to the input's f
  -- field.

  -- A lens for the r₁ field of R₂.

  r₁ : Lens R₂  r  R₁ (R₂.A r))
  r₁ = Lens₃-to-Lens {-a = # 0-} Dependent₃.r₁

  -- Lenses for the fields of R₁, accessed through an R₂ record. Note
  -- the use of /forward/ composition.

  x₂ : Lens R₂  r  R₂.A r)
  x₂ = r₁  x

  f₂ : Lens R₂  r   λ (f : R₂.A r  R₂.A r)   y  f y  y)
  f₂ = r₁  f

  lemma₂ : Lens R₂  r   y  R₁.f (R₂.r₁ r) y  y)
  lemma₂ = r₁  lemma

------------------------------------------------------------------------
-- Non-dependent lenses

module Non-dependent where

  open Lens.Non-dependent.Alternative
    renaming (Iso-lens to Lens; module Iso-lens to Lens)
  open Iso-lens-combinators

  -- Labels.

  data Label : Set where
    ″f″ ″x″ ″lemma″ ″A″ ″r₁″ : Label

  -- Labels come with decidable equality.

  Label↔Fin : Label  Fin 5
  Label↔Fin = record
    { surjection = record
      { logical-equivalence = record
        { to   = to
        ; from = from
        }
      ; right-inverse-of = to∘from
      }
    ; left-inverse-of = from∘to
    }
    where

    to : Label  Fin 5
    to ″f″     = fzero
    to ″x″     = fsuc fzero
    to ″lemma″ = fsuc (fsuc fzero)
    to ″A″     = fsuc (fsuc (fsuc fzero))
    to ″r₁″    = fsuc (fsuc (fsuc (fsuc fzero)))

    from : Fin 5  Label
    from fzero                                 = ″f″
    from (fsuc fzero)                          = ″x″
    from (fsuc (fsuc fzero))                   = ″lemma″
    from (fsuc (fsuc (fsuc fzero)))            = ″A″
    from (fsuc (fsuc (fsuc (fsuc fzero))))     = ″r₁″
    from (fsuc (fsuc (fsuc (fsuc (fsuc ())))))

    to∘from :  i  to (from i)  i
    to∘from fzero                                 = refl
    to∘from (fsuc fzero)                          = refl
    to∘from (fsuc (fsuc fzero))                   = refl
    to∘from (fsuc (fsuc (fsuc fzero)))            = refl
    to∘from (fsuc (fsuc (fsuc (fsuc fzero))))     = refl
    to∘from (fsuc (fsuc (fsuc (fsuc (fsuc ())))))

    from∘to :    from (to )  
    from∘to ″f″     = refl
    from∘to ″x″     = refl
    from∘to ″lemma″ = refl
    from∘to ″A″     = refl
    from∘to ″r₁″    = refl

  _≟_ : Decidable-equality Label
  _≟_ = Bij.decidable-equality-respects (inverse Label↔Fin) Fin._≟_

  -- Records.

  open import Record Label _≟_

  -- Nested records (defined using the record language from Record, so
  -- that we can use manifest fields).

  R₁ : Set  Signature _
  R₁ A =  , ″f″       _  A  A)
           , ″x″       _  A)
           , ″lemma″   r   y  (r · ″f″) y  y)

  R₂ : Signature _
  R₂ =  , ″A″    _  Set)
         , ″r₁″   r   _ (Record (R₁ (r · ″A″))))

  -- Lenses for each of the three fields of R₁.

  -- The x field is easiest, because it is independent of the others.

  x : {A : Set}  Lens (Record (R₁ A)) A
  x {A} = isomorphism-to-lens

    (Record (R₁ A)                                    ↝⟨ Record↔Recʳ 
     ( λ (f : A  A)   λ (x : A)   y  f y  y)  ↝⟨ ∃-comm 
     (A ×  λ (f : A  A)   y  f y  y)            ↝⟨ ×-comm ⟩□
     ( λ (f : A  A)   y  f y  y) × A            )

  -- The lemma field depends on the f field, so whenever the f field
  -- is set the lemma field needs to be updated as well.

  f : {A : Set} 
      Lens (Record (R₁ A))
           (Record ( , ″f″       _  A  A)
                      , ″lemma″   r   x  (r · ″f″) x  x)))
  f {A} = isomorphism-to-lens

    (Record (R₁ A)                                    ↝⟨ Record↔Recʳ 
     ( λ (f : A  A)   λ (x : A)   y  f y  y)  ↝⟨ ∃-comm 
     A × ( λ (f : A  A)   y  f y  y)            ↝⟨ F.id ×-cong inverse Record↔Recʳ ⟩□
     A × Record _                                     )

  -- The lemma field can be updated independently. Note the use of a
  -- manifest field in the type of the lens to capture the dependency
  -- between the two lens parameters.

  lemma : {A : Set} {f : A  A} 
          Lens (Record (R₁ A With ″f″   _  f)))
               (∀ x  f x  x)
  lemma {A} {f} = isomorphism-to-lens

    (Record (R₁ A With ″f″   _  f))  ↝⟨ Record↔Recʳ ⟩□
     A × (∀ x  f x  x)                 )

  -- The use of a manifest field is problematic, because the domain of
  -- the lens is no longer Record (R₁ A). It is easy to convert
  -- records into the required form, but this conversion is not a
  -- non-dependent lens (due to the dependency).

  convert : {A : Set} (r : Record (R₁ A)) 
            Record (R₁ A With ″f″   _  r · ″f″))
  convert (rec (rec (rec (_ , f) , x) , lemma)) =
    rec (rec (_ , x) , lemma)

  -- Let us now try to construct lenses for the same fields, but
  -- accessed through an R₂ record.

  -- First we define a lens for the r₁ field.

  r₁ : {A : Set} 
       Lens (Record (R₂ With ″A″  λ _  A)) (Record (R₁ A))
  r₁ {A} = isomorphism-to-lens

    (Record (R₂ With ″A″  λ _  A)  ↝⟨ Record↔Recʳ 
      _ (Record (R₁ A))             ↝⟨ Bij.↑↔ 
     Record (R₁ A)                   ↝⟨ inverse ×-left-identity 
      × Record (R₁ A)               ↝⟨ inverse Bij.↑↔ ×-cong F.id ⟩□
      _  × Record (R₁ A)           )

  -- It is now easy to construct lenses for the embedded x and f
  -- fields using composition of lenses.

  x₂ : {A : Set} 
       Lens (Record (R₂ With ″A″  λ _  A)) A
  x₂ = x  r₁

  f₂ : {A : Set} 
       Lens (Record (R₂ With ″A″  λ _  A))
            (Record ( , ″f″       _  A  A)
                       , ″lemma″   r   x  (r · ″f″) x  x)))
  f₂ = f  r₁

  -- It is less obvious how to construct the corresponding lens for
  -- the embedded lemma field.

  module Lemma-lens
    (r₁₂ : {A : Set} {r : Record (R₁ A)} 
           Lens (Record (R₂ With ″A″    _  A)
                            With ″r₁″   _  lift r)))
                (Record (R₁ A With ″f″   _  r · ″f″)))) where

    -- To start with, what should the type of the lemma lens be? The
    -- type used below is an obvious choice.

    lemma₂ : {A : Set} {r : Record (R₁ A)} 
             Lens (Record (R₂ With ″A″    _  A)
                              With ″r₁″   _  lift r)))
                  (∀ x  (r · ″f″) x  x)

    -- If we can construct a suitable lens r₁₂, with the type
    -- signature given above, then we can define the lemma lens using
    -- composition.

    lemma₂ = lemma  r₁₂

    -- However, we cannot define r₁₂.

    not-r₁₂ : 
    not-r₁₂ = no-isomorphism isomorphism
      where
      open Lens

      isomorphisms = λ A r 
                                                         ↝⟨ inverse Bij.↑↔ 
         _                                              ↝⟨ inverse Record↔Recʳ 
        Record (R₂ With ″A″    _  A)
                   With ″r₁″   _  lift r))            ↔⟨ equiv r₁₂ 
        R r₁₂ × Record (R₁ A With ″f″   _  r · ″f″))  ↝⟨ F.id ×-cong Record↔Recʳ ⟩□
        R r₁₂ × A × (∀ y  (r · ″f″) y  y)               

      isomorphism :  λ (A : Set₁)    A × Bool
      isomorphism =
        _ ,
        (                               ↝⟨ isomorphisms Bool r 
         R r₁₂ × Bool × (∀ b  b  b)    ↝⟨ F.id ×-cong ×-comm 
         R r₁₂ × (∀ b  b  b) × Bool    ↝⟨ ×-assoc ⟩□
         (R r₁₂ × (∀ b  b  b)) × Bool  )
        where
        r : Record (R₁ Bool)
        r = rec (rec (rec (_ , F.id) , true) , λ _  refl)

      no-isomorphism : ¬  λ (A : Set₁)    A × Bool
      no-isomorphism (A , iso) = Bool.true≢false (
        true                           ≡⟨⟩
        proj₂ (a , true)               ≡⟨ cong proj₂ $ sym $ right-inverse-of (a , true) 
        proj₂ (to (from (a , true)))   ≡⟨⟩
        proj₂ (to (from (a , false)))  ≡⟨ cong proj₂ $ right-inverse-of (a , false) 
        proj₂ (a , false)              ≡⟨ refl ⟩∎
        false                          )
        where
        open _↔_ iso

        a : A
        a = proj₁ (to _)

  -- Conclusion: The use of manifest fields limits the usefulness of
  -- these lenses, because they do not compose as well as they do for
  -- non-dependent records. Dependent lenses seem to be more useful.