{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module Control.Refractor
  ( Lens, Iso,
    lens, iso,
    gets, get, set, modify,
    toListOf, foldrOf, foldlOf, mapAccumLOf, mapAccumROf,
    fstL, sndL, swapL, unitL, constL
  ) where

import Prelude hiding (Functor (..), id, map)

import Control.Applicative
import Control.Applicative.Backwards (Backwards (..))
import Control.Categorical.Functor
import Control.Category
import Control.Category.Dual
import Control.Category.Unicode
import Control.Monad.Trans.State (State, state, runState)
import Data.Functor.Identity
import qualified Data.Monoid as Monoid (Dual (..))
import Data.Morphism.Endo
import Data.Profunctor
import Data.Proxy
import Data.Tuple (swap)

type Refractor s t f α β a b = s a (f b) -> t α (f β)

type Lens s t α β a b = ∀ f . Functor s t f => Refractor s t f α β a b

type Iso σ τ s t α β a b = ∀ p f . (Functor (Dual σ) (NT (->)) p, ∀ x . Functor s (->) (p x), Functor τ s f) => Refractor p p f α β a b

lens :: (α -> a) → (b → α → β) → Lens (->) (->) α β a b
lens :: (α -> a) -> (b -> α -> β) -> Lens (->) (->) α β a b
lens get :: α -> a
get set :: b -> α -> β
set ret :: a -> f b
ret = ((b -> β) -> f b -> f β) -> (α -> b -> β) -> (α -> f b) -> α -> f β
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (b -> β) -> f b -> f β
forall α β (s :: α -> α -> *) (t :: β -> β -> *) (f :: α -> β)
       (a :: α) (b :: α).
Functor s t f =>
s a b -> t (f a) (f b)
map ((b -> α -> β) -> α -> b -> β
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> α -> β
set) (a -> f b
ret (a -> f b) -> (α -> a) -> α -> f b
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ α -> a
get)

iso :: ∀ σ τ s t α β a b . Proxy s -> σ α a → τ b β → Iso σ τ s t α β a b
iso :: Proxy s -> σ α a -> τ b β -> Iso σ τ s t α β a b
iso _ f :: σ α a
f g :: τ b β
g = s (f b) (f β) -> p α (f b) -> p α (f β)
forall α β (s :: α -> α -> *) (t :: β -> β -> *) (f :: α -> β)
       (a :: α) (b :: α).
Functor s t f =>
s a b -> t (f a) (f b)
map (τ b β -> s (f b) (f β)
forall α β (s :: α -> α -> *) (t :: β -> β -> *) (f :: α -> β)
       (a :: α) (b :: α).
Functor s t f =>
s a b -> t (f a) (f b)
map τ b β
g :: s _ _) (p α (f b) -> p α (f β))
-> (p a (f b) -> p α (f b)) -> p a (f b) -> p α (f β)
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ NT (->) (p a) (p α) -> forall (a :: k). p a a -> p α a
forall k1 k2 (s :: k1 -> k2 -> *) k3 (f :: k3 -> k1)
       (g :: k3 -> k2).
NT s f g -> forall (a :: k3). s (f a) (g a)
nt (Dual σ a α -> NT (->) (p a) (p α)
forall α β (s :: α -> α -> *) (t :: β -> β -> *) (f :: α -> β)
       (a :: α) (b :: α).
Functor s t f =>
s a b -> t (f a) (f b)
map (σ α a -> Dual σ a α
forall k k1 (k2 :: k -> k1 -> *) (a :: k1) (b :: k).
k2 b a -> Dual k2 a b
Dual σ α a
f))

get :: ((a → Const a b) → α → Const a β) → α → a
get :: ((a -> Const a b) -> α -> Const a β) -> α -> a
get l :: (a -> Const a b) -> α -> Const a β
l = ((a -> Const a b) -> α -> Const a β) -> (a -> a) -> α -> a
forall k k a c (b :: k) α (β :: k).
((a -> Const c b) -> α -> Const c β) -> (a -> c) -> α -> c
gets (a -> Const a b) -> α -> Const a β
l a -> a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

gets :: ((a -> Const c b) -> α -> Const c β) -> (a -> c) -> α -> c
gets :: ((a -> Const c b) -> α -> Const c β) -> (a -> c) -> α -> c
gets l :: (a -> Const c b) -> α -> Const c β
l f :: a -> c
f = Const c β -> c
forall a k (b :: k). Const a b -> a
getConst (Const c β -> c) -> (α -> Const c β) -> α -> c
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ (a -> Const c b) -> α -> Const c β
l (c -> Const c b
forall k a (b :: k). a -> Const a b
Const (c -> Const c b) -> (a -> c) -> a -> Const c b
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ a -> c
f)

set :: ((a → Identity b) → α → Identity β) → b → α → β
set :: ((a -> Identity b) -> α -> Identity β) -> b -> α -> β
set l :: (a -> Identity b) -> α -> Identity β
l = ((a -> Identity b) -> α -> Identity β) -> (a -> b) -> α -> β
forall a b α β.
((a -> Identity b) -> α -> Identity β) -> (a -> b) -> α -> β
modify (a -> Identity b) -> α -> Identity β
l ((a -> b) -> α -> β) -> (b -> a -> b) -> b -> α -> β
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ b -> a -> b
forall (f :: * -> *) a. Applicative f => a -> f a
pure

modify :: ((a → Identity b) → α → Identity β) → (a → b) → α → β
modify :: ((a -> Identity b) -> α -> Identity β) -> (a -> b) -> α -> β
modify l :: (a -> Identity b) -> α -> Identity β
l f :: a -> b
f = Identity β -> β
forall a. Identity a -> a
runIdentity (Identity β -> β) -> (α -> Identity β) -> α -> β
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ (a -> Identity b) -> α -> Identity β
l (b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> (a -> b) -> a -> Identity b
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ a -> b
f)

-- foldOf :: Monoid a => Getting a α β a b -> α -> a
-- foldOf = get

-- foldMapOf :: Getting c α β a b -> (a -> c) -> α -> c
-- foldMapOf = gets

toListOf :: Getting (Endo (->) [a]) α β a b -> α -> [a]
toListOf :: Getting (Endo (->) [a]) α β a b -> α -> [a]
toListOf l :: Getting (Endo (->) [a]) α β a b
l = Getting (Endo (->) [a]) α β a b
-> (a -> [a] -> [a]) -> [a] -> α -> [a]
forall k k c α (β :: k) a (b :: k).
Getting (Endo (->) c) α β a b -> (a -> c -> c) -> c -> α -> c
foldrOf Getting (Endo (->) [a]) α β a b
l (:) []

foldrOf :: Getting (Endo (->) c) α β a b -> (a -> c -> c) -> c -> α -> c
foldrOf :: Getting (Endo (->) c) α β a b -> (a -> c -> c) -> c -> α -> c
foldrOf l :: Getting (Endo (->) c) α β a b
l f :: a -> c -> c
f z₀ :: c
z₀ = (Endo (->) c -> c -> c) -> c -> Endo (->) c -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip Endo (->) c -> c -> c
forall k (s :: k -> k -> *) (a :: k). Endo s a -> s a a
endo c
z₀ (Endo (->) c -> c) -> (α -> Endo (->) c) -> α -> c
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ Getting (Endo (->) c) α β a b
-> (a -> Endo (->) c) -> α -> Endo (->) c
forall k k a c (b :: k) α (β :: k).
((a -> Const c b) -> α -> Const c β) -> (a -> c) -> α -> c
gets Getting (Endo (->) c) α β a b
l ((c -> c) -> Endo (->) c
forall k (s :: k -> k -> *) (a :: k). s a a -> Endo s a
Endo ((c -> c) -> Endo (->) c) -> (a -> c -> c) -> a -> Endo (->) c
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ a -> c -> c
f)

foldlOf :: Getting (Monoid.Dual (Endo (->) c)) α β a b -> (c -> a -> c) -> c -> α -> c
foldlOf :: Getting (Dual (Endo (->) c)) α β a b
-> (c -> a -> c) -> c -> α -> c
foldlOf l :: Getting (Dual (Endo (->) c)) α β a b
l f :: c -> a -> c
f z₀ :: c
z₀ = (Endo (->) c -> c -> c) -> c -> Endo (->) c -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip Endo (->) c -> c -> c
forall k (s :: k -> k -> *) (a :: k). Endo s a -> s a a
endo c
z₀ (Endo (->) c -> c) -> (α -> Endo (->) c) -> α -> c
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ Dual (Endo (->) c) -> Endo (->) c
forall a. Dual a -> a
Monoid.getDual (Dual (Endo (->) c) -> Endo (->) c)
-> (α -> Dual (Endo (->) c)) -> α -> Endo (->) c
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ Getting (Dual (Endo (->) c)) α β a b
-> (a -> Dual (Endo (->) c)) -> α -> Dual (Endo (->) c)
forall k k a c (b :: k) α (β :: k).
((a -> Const c b) -> α -> Const c β) -> (a -> c) -> α -> c
gets Getting (Dual (Endo (->) c)) α β a b
l (Endo (->) c -> Dual (Endo (->) c)
forall a. a -> Dual a
Monoid.Dual (Endo (->) c -> Dual (Endo (->) c))
-> (a -> Endo (->) c) -> a -> Dual (Endo (->) c)
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ (c -> c) -> Endo (->) c
forall k (s :: k -> k -> *) (a :: k). s a a -> Endo s a
Endo ((c -> c) -> Endo (->) c) -> (a -> c -> c) -> a -> Endo (->) c
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ (c -> a -> c) -> a -> c -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip c -> a -> c
f)

-- foldMapAccumOf :: Monoid c => ((a -> (c, b)) -> α -> (c, β)) -> (a -> (c, b)) -> α -> (c, β)
-- foldMapAccumOf = id

mapAccumROf :: ((a -> State c b) -> α -> State c β) -> (a -> c -> (c, b)) -> c -> α -> (c, β)
mapAccumROf :: ((a -> State c b) -> α -> State c β)
-> (a -> c -> (c, b)) -> c -> α -> (c, β)
mapAccumROf l :: (a -> State c b) -> α -> State c β
l f :: a -> c -> (c, b)
f z₀ :: c
z₀ = (β, c) -> (c, β)
forall a b. (a, b) -> (b, a)
swap ((β, c) -> (c, β)) -> (α -> (β, c)) -> α -> (c, β)
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ (State c β -> c -> (β, c)) -> c -> State c β -> (β, c)
forall a b c. (a -> b -> c) -> b -> a -> c
flip State c β -> c -> (β, c)
forall s a. State s a -> s -> (a, s)
runState c
z₀ (State c β -> (β, c)) -> (α -> State c β) -> α -> (β, c)
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ (a -> State c b) -> α -> State c β
l ((c -> (b, c)) -> State c b
forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state ((c -> (b, c)) -> State c b)
-> (a -> c -> (b, c)) -> a -> State c b
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ ((c, b) -> (b, c)
forall a b. (a, b) -> (b, a)
swap ((c, b) -> (b, c)) -> (c -> (c, b)) -> c -> (b, c)
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘) ((c -> (c, b)) -> c -> (b, c))
-> (a -> c -> (c, b)) -> a -> c -> (b, c)
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ a -> c -> (c, b)
f)

mapAccumLOf :: ((a -> Backwards (State c) b) -> α -> Backwards (State c) β) -> (c -> a -> (c, b)) -> c -> α -> (c, β)
mapAccumLOf :: ((a -> Backwards (State c) b) -> α -> Backwards (State c) β)
-> (c -> a -> (c, b)) -> c -> α -> (c, β)
mapAccumLOf l :: (a -> Backwards (State c) b) -> α -> Backwards (State c) β
l f :: c -> a -> (c, b)
f z₀ :: c
z₀ = (β, c) -> (c, β)
forall a b. (a, b) -> (b, a)
swap ((β, c) -> (c, β)) -> (α -> (β, c)) -> α -> (c, β)
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ (State c β -> c -> (β, c)) -> c -> State c β -> (β, c)
forall a b c. (a -> b -> c) -> b -> a -> c
flip State c β -> c -> (β, c)
forall s a. State s a -> s -> (a, s)
runState c
z₀ (State c β -> (β, c)) -> (α -> State c β) -> α -> (β, c)
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ Backwards (State c) β -> State c β
forall k (f :: k -> *) (a :: k). Backwards f a -> f a
forwards (Backwards (State c) β -> State c β)
-> (α -> Backwards (State c) β) -> α -> State c β
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ (a -> Backwards (State c) b) -> α -> Backwards (State c) β
l (StateT c Identity b -> Backwards (State c) b
forall k (f :: k -> *) (a :: k). f a -> Backwards f a
Backwards (StateT c Identity b -> Backwards (State c) b)
-> (a -> StateT c Identity b) -> a -> Backwards (State c) b
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ (c -> (b, c)) -> StateT c Identity b
forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state ((c -> (b, c)) -> StateT c Identity b)
-> (a -> c -> (b, c)) -> a -> StateT c Identity b
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ ((c, b) -> (b, c)
forall a b. (a, b) -> (b, a)
swap ((c, b) -> (b, c)) -> (c -> (c, b)) -> c -> (b, c)
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘) ((c -> (c, b)) -> c -> (b, c))
-> (a -> c -> (c, b)) -> a -> c -> (b, c)
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ (c -> a -> (c, b)) -> a -> c -> (c, b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip c -> a -> (c, b)
f)

type Getting r α β a b = (a -> Const r b) -> α -> Const r β

fstL :: Lens (->) (->) (a, c) (b, c) a b
fstL :: Refractor (->) (->) f (a, c) (b, c) a b
fstL = Refractor (->) (->) f (a, c) (b, c) (c, a) (c, b)
forall a b c d. Iso (->) (->) (->) (->) (a, b) (c, d) (b, a) (d, c)
swapL Refractor (->) (->) f (a, c) (b, c) (c, a) (c, b)
-> ((a -> f b) -> (c, a) -> f (c, b))
-> Refractor (->) (->) f (a, c) (b, c) a b
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ (a -> f b) -> (c, a) -> f (c, b)
forall a b c. Lens (->) (->) (a, b) (a, c) b c
sndL

sndL :: Lens (->) (->) (a, b) (a, c) b c
sndL :: Refractor (->) (->) f (a, b) (a, c) b c
sndL f :: b -> f c
f = a -> a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (a -> a) -> (b -> f c) -> (a, b) -> (a, f c)
forall (p :: * -> * -> *) a₁ b₁ a₂ b₂.
Strong (,) p =>
p a₁ b₁ -> p a₂ b₂ -> p (a₁, a₂) (b₁, b₂)
*** b -> f c
f ((a, b) -> (a, f c))
-> ((a, f c) -> f (a, c)) -> (a, b) -> f (a, c)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (a -> f c -> f (a, c)) -> (a, f c) -> f (a, c)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((c -> (a, c)) -> f c -> f (a, c)
forall α β (s :: α -> α -> *) (t :: β -> β -> *) (f :: α -> β)
       (a :: α) (b :: α).
Functor s t f =>
s a b -> t (f a) (f b)
map ((c -> (a, c)) -> f c -> f (a, c))
-> (a -> c -> (a, c)) -> a -> f c -> f (a, c)
forall (c :: * -> * -> *) β γ α.
Category c =>
c β γ -> c α β -> c α γ
∘ (,))

swapL :: Iso (->) (->) (->) (->) (a, b) (c, d) (b, a) (d, c)
swapL :: Refractor p p f (a, b) (c, d) (b, a) (d, c)
swapL = Proxy (->)
-> ((a, b) -> (b, a))
-> ((d, c) -> (c, d))
-> Iso (->) (->) (->) Any (a, b) (c, d) (b, a) (d, c)
forall k k k k (σ :: k -> k -> *) (τ :: k -> k -> *)
       (s :: k -> k -> *) (t :: k) (α :: k) (β :: k) (a :: k) (b :: k).
Proxy s -> σ α a -> τ b β -> Iso σ τ s t α β a b
iso (Proxy (->)
forall k (t :: k). Proxy t
Proxy :: Proxy (->)) (a, b) -> (b, a)
forall a b. (a, b) -> (b, a)
swap (d, c) -> (c, d)
forall a b. (a, b) -> (b, a)
swap

unitL :: Lens (->) (->) α α () ()
unitL :: Refractor (->) (->) f α α () ()
unitL = (α -> ()) -> (() -> α -> α) -> Lens (->) (->) α α () ()
forall α a b β. (α -> a) -> (b -> α -> β) -> Lens (->) (->) α β a b
lens (() -> α -> ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (\ () -> α -> α
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)

constL :: Iso (->) (->) (->) (->) (Const a α) (Const b β) a b
constL :: Refractor p p f (Const a α) (Const b β) a b
constL = Proxy (->)
-> (Const a α -> a)
-> (b -> Const b β)
-> Iso (->) (->) (->) Any (Const a α) (Const b β) a b
forall k k k k (σ :: k -> k -> *) (τ :: k -> k -> *)
       (s :: k -> k -> *) (t :: k) (α :: k) (β :: k) (a :: k) (b :: k).
Proxy s -> σ α a -> τ b β -> Iso σ τ s t α β a b
iso (Proxy (->)
forall k (t :: k). Proxy t
Proxy :: Proxy (->)) Const a α -> a
forall a k (b :: k). Const a b -> a
getConst b -> Const b β
forall k a (b :: k). a -> Const a b
Const