{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE QuantifiedConstraints #-}

-- | van Laarhoven lenses for large records.
-- The type synonym
--
-- @
--   type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
-- @
-- Appears below, however it is not exported to avoid conflicts with other
-- libraries defining equivalent synonyms.
module Data.Record.Generic.Lens.VL (
    -- * Lenses for records
    SimpleRecordLens(..)
  , HKRecordLens(..)
  , RegularRecordLens(..)
  , lensesForSimpleRecord
  , lensesForHKRecord
  , lensesForRegularRecord
    -- * Regular records
  , RegularField(..)
  , IsRegularField(..)
    -- * Lenses into 'Rep'
  , RepLens(..)
  , repLenses
    -- * General purpose lenses
  , genericLens
  , normalForm1Lens
  , interpretedLens
  , standardInterpretationLens
  ) where

import Data.Kind

import Data.Record.Generic
import Data.Record.Generic.Transform

import qualified Data.Record.Generic.Rep as Rep

-- | The standard van Laarhoven representation for a monomorphic lens
type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s

{-------------------------------------------------------------------------------
  Simple records (in contrast to higher-kinded records, see below)
-------------------------------------------------------------------------------}

data SimpleRecordLens a b where
  SimpleRecordLens :: Lens' a b -> SimpleRecordLens a b

-- | Construct lenses for each field in the record
--
-- NOTE: This is of limited use since we cannot pattern match on the resulting
-- 'Rep' in any meaningful way. It is possible to go through the SOP adapter,
-- but if we do, we incur quadratic cost again.
--
-- We can do better for higher-kinded records, and better still for regular
-- higher-kinded records. See 'lensesForHKRecord' and 'lensesForRegularRecord'.
lensesForSimpleRecord :: forall a. Generic a => Rep (SimpleRecordLens a) a
lensesForSimpleRecord :: Rep (SimpleRecordLens a) a
lensesForSimpleRecord =
    (forall x. RepLens I a x -> SimpleRecordLens a x)
-> Rep (RepLens I a) a -> Rep (SimpleRecordLens a) a
forall a (f :: * -> *) (g :: * -> *).
Generic a =>
(forall x. f x -> g x) -> Rep f a -> Rep g a
Rep.map (\(RepLens l) -> Lens' a x -> SimpleRecordLens a x
forall a b. Lens' a b -> SimpleRecordLens a b
SimpleRecordLens (Lens' a x -> SimpleRecordLens a x)
-> Lens' a x -> SimpleRecordLens a x
forall a b. (a -> b) -> a -> b
$ \x -> f x
f -> Lens' (Rep I a) (I x) -> (x -> f x) -> a -> f a
forall x. Lens' (Rep I a) (I x) -> Lens' a x
aux Lens' (Rep I a) (I x)
l x -> f x
f) Rep (RepLens I a) a
forall a (f :: * -> *). Generic a => Rep (RepLens f a) a
repLenses
  where
    aux :: Lens' (Rep I a) (I x) -> Lens' a x
    aux :: Lens' (Rep I a) (I x) -> Lens' a x
aux Lens' (Rep I a) (I x)
l x -> f x
f a
a = Rep I a -> a
forall a. Generic a => Rep I a -> a
to (Rep I a -> a) -> f (Rep I a) -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (I x -> f (I x)) -> Rep I a -> f (Rep I a)
Lens' (Rep I a) (I x)
l (\(I x
x) -> x -> I x
forall a. a -> I a
I (x -> I x) -> f x -> f (I x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> x -> f x
f x
x) (a -> Rep I a
forall a. Generic a => a -> Rep I a
from a
a)

{-------------------------------------------------------------------------------
  Higher-kinded records (records with a functor parameter)
-------------------------------------------------------------------------------}

-- | Lens for higher-kinded record
--
-- See 'lensesForHKRecord' for details.
data HKRecordLens d (f :: Type -> Type) tbl x where
  HKRecordLens :: Lens' (tbl f) (Interpret (d f) x) -> HKRecordLens d f tbl x

-- | Lenses for higher-kinded records
--
-- NOTE: The lenses constructed by this function are primarily intended for
-- further processing, either by 'lensesForRegularRecord' or using application
-- specific logic. Details below.
--
-- Suppose we have a record @tbl f@ which is indexed by a functor @f@, and we
-- want to construct lenses from @tbl f@ to each field in the record. Using the
-- @Transform@ infrastructure, we can construct a lens
--
-- > tbl f ~~> Rep I (tbl f) ~~> Rep (Interpret (d f)) (tbl Uninterpreted)
--
-- Using 'repLenses' we can construct a lens of type
--
-- > Rep (Interpret (d f)) (tbl Uninterpreted) ~~> Interpret (d f) x
--
-- for every field of type @x@. Putting these two together gives us a lens
--
-- > tbl f ~~> Interpret (d f) x
--
-- for every field in @tbl Uninterpreted@. We cannot simplify this, because we
-- do not know anything about the shape of @x@; specifically, it might not be
-- equal to @Uninterpreted x'@ for some @x'@, and hence we cannot simplify the
-- target type of the lens. We can do better for records with regular fields;
-- see 'lensesForRegularRecord'.
lensesForHKRecord :: forall d tbl f.
     ( Generic (tbl f)
     , Generic (tbl Uninterpreted)
     , HasNormalForm (d f) (tbl f) (tbl Uninterpreted)
     )
  => Proxy d -> Rep (HKRecordLens d f tbl) (tbl Uninterpreted)
lensesForHKRecord :: Proxy d -> Rep (HKRecordLens d f tbl) (tbl Uninterpreted)
lensesForHKRecord Proxy d
d = (forall x.
 RepLens (Interpret (d f)) (tbl Uninterpreted) x
 -> HKRecordLens d f tbl x)
-> Rep
     (RepLens (Interpret (d f)) (tbl Uninterpreted)) (tbl Uninterpreted)
-> Rep (HKRecordLens d f tbl) (tbl Uninterpreted)
forall a (f :: * -> *) (g :: * -> *).
Generic a =>
(forall x. f x -> g x) -> Rep f a -> Rep g a
Rep.map forall x.
RepLens (Interpret (d f)) (tbl Uninterpreted) x
-> HKRecordLens d f tbl x
aux Rep
  (RepLens (Interpret (d f)) (tbl Uninterpreted)) (tbl Uninterpreted)
fromRepLenses
  where
    fromRepLenses :: Rep (RepLens (Interpret (d f)) (tbl Uninterpreted)) (tbl Uninterpreted)
    fromRepLenses :: Rep
  (RepLens (Interpret (d f)) (tbl Uninterpreted)) (tbl Uninterpreted)
fromRepLenses = Rep
  (RepLens (Interpret (d f)) (tbl Uninterpreted)) (tbl Uninterpreted)
forall a (f :: * -> *). Generic a => Rep (RepLens f a) a
repLenses

    aux :: forall x. RepLens (Interpret (d f)) (tbl Uninterpreted) x -> HKRecordLens d f tbl x
    aux :: RepLens (Interpret (d f)) (tbl Uninterpreted) x
-> HKRecordLens d f tbl x
aux (RepLens Lens'
  (Rep (Interpret (d f)) (tbl Uninterpreted)) (Interpret (d f) x)
l) = Lens' (tbl f) (Interpret (d f) x) -> HKRecordLens d f tbl x
forall (tbl :: (* -> *) -> *) (f :: * -> *) (d :: (* -> *) -> *) x.
Lens' (tbl f) (Interpret (d f) x) -> HKRecordLens d f tbl x
HKRecordLens (Lens' (tbl f) (Interpret (d f) x) -> HKRecordLens d f tbl x)
-> Lens' (tbl f) (Interpret (d f) x) -> HKRecordLens d f tbl x
forall a b. (a -> b) -> a -> b
$
          (Rep I (tbl f) -> f (Rep I (tbl f))) -> tbl f -> f (tbl f)
forall a. Generic a => Lens' a (Rep I a)
genericLens
        ((Rep I (tbl f) -> f (Rep I (tbl f))) -> tbl f -> f (tbl f))
-> ((Interpret (d f) x -> f (Interpret (d f) x))
    -> Rep I (tbl f) -> f (Rep I (tbl f)))
-> (Interpret (d f) x -> f (Interpret (d f) x))
-> tbl f
-> f (tbl f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy d
-> Lens'
     (Rep I (tbl f)) (Rep (Interpret (d f)) (tbl Uninterpreted))
forall (d :: (* -> *) -> *) (f :: * -> *) (x :: (* -> *) -> *).
HasNormalForm (d f) (x f) (x Uninterpreted) =>
Proxy d
-> Lens' (Rep I (x f)) (Rep (Interpret (d f)) (x Uninterpreted))
normalForm1Lens Proxy d
d
        ((Rep (Interpret (d f)) (tbl Uninterpreted)
  -> f (Rep (Interpret (d f)) (tbl Uninterpreted)))
 -> Rep I (tbl f) -> f (Rep I (tbl f)))
-> ((Interpret (d f) x -> f (Interpret (d f) x))
    -> Rep (Interpret (d f)) (tbl Uninterpreted)
    -> f (Rep (Interpret (d f)) (tbl Uninterpreted)))
-> (Interpret (d f) x -> f (Interpret (d f) x))
-> Rep I (tbl f)
-> f (Rep I (tbl f))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Interpret (d f) x -> f (Interpret (d f) x))
-> Rep (Interpret (d f)) (tbl Uninterpreted)
-> f (Rep (Interpret (d f)) (tbl Uninterpreted))
Lens'
  (Rep (Interpret (d f)) (tbl Uninterpreted)) (Interpret (d f) x)
l

{-------------------------------------------------------------------------------
  Regular records
-------------------------------------------------------------------------------}

-- | Proof that @x@ is a regular field
--
-- See 'IsRegularField'
data RegularField f x where
  RegularField :: RegularField f (f x)

-- | Regular record fields
--
-- For a higher-kinded record @tbl f@, parameterized over some functor @f@,
-- we say that the fields are /regular/ iff every field has the form @f x@
-- for some @x@.
class IsRegularField f x where
  isRegularField :: Proxy (f x) -> RegularField f x

instance IsRegularField f (f x) where
  isRegularField :: Proxy (f (f x)) -> RegularField f (f x)
isRegularField Proxy (f (f x))
_ = RegularField f (f x)
forall (f :: * -> *) x. RegularField f (f x)
RegularField

{-------------------------------------------------------------------------------
  Lenses into regular records
-------------------------------------------------------------------------------}

-- | Lens into a regular record
--
-- See 'lensesForRegularRecord'
data RegularRecordLens tbl f x where
  RegularRecordLens :: Lens' (tbl f) (f x) -> RegularRecordLens tbl f x

-- | Lenses into higher-kinded records with regular fields
--
-- We can use 'lensesForHKRecord' to construct a 'Rep' of lenses into a higher-kinded
-- record. If in addition the record is regular, we can use the record type
-- /itself/ to store all the lenses.
lensesForRegularRecord :: forall d tbl f.
     ( Generic (tbl (RegularRecordLens tbl f))
     , Generic (tbl Uninterpreted)
     , Generic (tbl f)
     , HasNormalForm (d (RegularRecordLens tbl f)) (tbl (RegularRecordLens tbl f)) (tbl Uninterpreted)
     , HasNormalForm (d f) (tbl f) (tbl Uninterpreted)
     , Constraints (tbl Uninterpreted) (IsRegularField Uninterpreted)
     , StandardInterpretation d (RegularRecordLens tbl f)
     , StandardInterpretation d f
     )
  => Proxy d -> tbl (RegularRecordLens tbl f)
lensesForRegularRecord :: Proxy d -> tbl (RegularRecordLens tbl f)
lensesForRegularRecord Proxy d
d = Rep I (tbl (RegularRecordLens tbl f))
-> tbl (RegularRecordLens tbl f)
forall a. Generic a => Rep I a -> a
to (Rep I (tbl (RegularRecordLens tbl f))
 -> tbl (RegularRecordLens tbl f))
-> (Rep
      (Interpret (d (RegularRecordLens tbl f))) (tbl Uninterpreted)
    -> Rep I (tbl (RegularRecordLens tbl f)))
-> Rep
     (Interpret (d (RegularRecordLens tbl f))) (tbl Uninterpreted)
-> tbl (RegularRecordLens tbl f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy d
-> Rep
     (Interpret (d (RegularRecordLens tbl f))) (tbl Uninterpreted)
-> Rep I (tbl (RegularRecordLens tbl f))
forall k dom (d :: (k -> *) -> dom) (f :: k -> *)
       (x :: (k -> *) -> *).
HasNormalForm (d f) (x f) (x Uninterpreted) =>
Proxy d -> Rep (Interpret (d f)) (x Uninterpreted) -> Rep I (x f)
denormalize1 Proxy d
d (Rep (Interpret (d (RegularRecordLens tbl f))) (tbl Uninterpreted)
 -> tbl (RegularRecordLens tbl f))
-> Rep
     (Interpret (d (RegularRecordLens tbl f))) (tbl Uninterpreted)
-> tbl (RegularRecordLens tbl f)
forall a b. (a -> b) -> a -> b
$
    Proxy (IsRegularField Uninterpreted)
-> (forall x.
    IsRegularField Uninterpreted x =>
    HKRecordLens d f tbl x
    -> Interpret (d (RegularRecordLens tbl f)) x)
-> Rep (HKRecordLens d f tbl) (tbl Uninterpreted)
-> Rep
     (Interpret (d (RegularRecordLens tbl f))) (tbl Uninterpreted)
forall a (c :: * -> Constraint) (f :: * -> *) (g :: * -> *).
(Generic a, Constraints a c) =>
Proxy c -> (forall x. c x => f x -> g x) -> Rep f a -> Rep g a
Rep.cmap
      (Proxy (IsRegularField Uninterpreted)
forall k (t :: k). Proxy t
Proxy @(IsRegularField Uninterpreted))
      forall x.
IsRegularField Uninterpreted x =>
HKRecordLens d f tbl x -> Interpret (d (RegularRecordLens tbl f)) x
aux
      (Proxy d -> Rep (HKRecordLens d f tbl) (tbl Uninterpreted)
forall (d :: (* -> *) -> *) (tbl :: (* -> *) -> *) (f :: * -> *).
(Generic (tbl f), Generic (tbl Uninterpreted),
 HasNormalForm (d f) (tbl f) (tbl Uninterpreted)) =>
Proxy d -> Rep (HKRecordLens d f tbl) (tbl Uninterpreted)
lensesForHKRecord Proxy d
d)
  where
    aux :: forall x.
         IsRegularField Uninterpreted x
      => HKRecordLens d f tbl x
      -> Interpret (d (RegularRecordLens tbl f)) x
    aux :: HKRecordLens d f tbl x -> Interpret (d (RegularRecordLens tbl f)) x
aux (HKRecordLens Lens' (tbl f) (Interpret (d f) x)
l) =
        case Proxy (Uninterpreted x) -> RegularField Uninterpreted x
forall (f :: * -> *) x.
IsRegularField f x =>
Proxy (f x) -> RegularField f x
isRegularField (Proxy (Uninterpreted x)
forall k (t :: k). Proxy t
Proxy @(Uninterpreted x)) of
          RegularField Uninterpreted x
RegularField -> Proxy d
-> RegularRecordLens tbl f x
-> Interpret (d (RegularRecordLens tbl f)) (Uninterpreted x)
forall k dom (d :: (k -> *) -> dom) (f :: k -> *) (x :: k).
StandardInterpretation d f =>
Proxy d -> f x -> Interpret (d f) (Uninterpreted x)
toStandardInterpretation Proxy d
d (RegularRecordLens tbl f x
 -> Interpret (d (RegularRecordLens tbl f)) (Uninterpreted x))
-> RegularRecordLens tbl f x
-> Interpret (d (RegularRecordLens tbl f)) (Uninterpreted x)
forall a b. (a -> b) -> a -> b
$ Lens' (tbl f) (f x) -> RegularRecordLens tbl f x
forall (tbl :: (* -> *) -> *) (f :: * -> *) x.
Lens' (tbl f) (f x) -> RegularRecordLens tbl f x
RegularRecordLens (Lens' (tbl f) (f x) -> RegularRecordLens tbl f x)
-> Lens' (tbl f) (f x) -> RegularRecordLens tbl f x
forall a b. (a -> b) -> a -> b
$
             (Interpret (d f) x -> f (Interpret (d f) x)) -> tbl f -> f (tbl f)
Lens' (tbl f) (Interpret (d f) x)
l ((Interpret (d f) x -> f (Interpret (d f) x))
 -> tbl f -> f (tbl f))
-> ((f x -> f (f x)) -> Interpret (d f) x -> f (Interpret (d f) x))
-> (f x -> f (f x))
-> tbl f
-> f (tbl f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy d -> Lens' (Interpret (d f) (Uninterpreted x)) (f x)
forall (d :: (* -> *) -> *) (f :: * -> *) x.
StandardInterpretation d f =>
Proxy d -> Lens' (Interpret (d f) (Uninterpreted x)) (f x)
standardInterpretationLens Proxy d
d

{-------------------------------------------------------------------------------
  Lenses into 'Rep'
-------------------------------------------------------------------------------}

data RepLens f a x where
  RepLens :: Lens' (Rep f a) (f x) -> RepLens f a x

repLenses :: Generic a => Rep (RepLens f a) a
repLenses :: Rep (RepLens f a) a
repLenses = (forall x. Index a x -> RepLens f a x)
-> Rep (Index a) a -> Rep (RepLens f a) a
forall a (f :: * -> *) (g :: * -> *).
Generic a =>
(forall x. f x -> g x) -> Rep f a -> Rep g a
Rep.map forall x. Index a x -> RepLens f a x
forall a x (f :: * -> *). Index a x -> RepLens f a x
aux Rep (Index a) a
forall a. Generic a => Rep (Index a) a
Rep.allIndices
  where
    aux :: Rep.Index a x -> RepLens f a x
    aux :: Index a x -> RepLens f a x
aux Index a x
ix = Lens' (Rep f a) (f x) -> RepLens f a x
forall (f :: * -> *) a x. Lens' (Rep f a) (f x) -> RepLens f a x
RepLens (Lens' (Rep f a) (f x) -> RepLens f a x)
-> Lens' (Rep f a) (f x) -> RepLens f a x
forall a b. (a -> b) -> a -> b
$ Index a x -> (f x -> f (f x)) -> Rep f a -> f (Rep f a)
forall (m :: * -> *) a x (f :: * -> *).
Functor m =>
Index a x -> (f x -> m (f x)) -> Rep f a -> m (Rep f a)
Rep.updateAtIndex Index a x
ix

{-------------------------------------------------------------------------------
  General purpose lenses
-------------------------------------------------------------------------------}

genericLens :: Generic a => Lens' a (Rep I a)
genericLens :: Lens' a (Rep I a)
genericLens Rep I a -> f (Rep I a)
f a
a = Rep I a -> a
forall a. Generic a => Rep I a -> a
to (Rep I a -> a) -> f (Rep I a) -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rep I a -> f (Rep I a)
f (a -> Rep I a
forall a. Generic a => a -> Rep I a
from a
a)

normalForm1Lens ::
     HasNormalForm (d f) (x f) (x Uninterpreted)
  => Proxy d
  -> Lens' (Rep I (x f)) (Rep (Interpret (d f)) (x Uninterpreted))
normalForm1Lens :: Proxy d
-> Lens' (Rep I (x f)) (Rep (Interpret (d f)) (x Uninterpreted))
normalForm1Lens Proxy d
p Rep (Interpret (d f)) (x Uninterpreted)
-> f (Rep (Interpret (d f)) (x Uninterpreted))
f Rep I (x f)
a = Proxy d -> Rep (Interpret (d f)) (x Uninterpreted) -> Rep I (x f)
forall k dom (d :: (k -> *) -> dom) (f :: k -> *)
       (x :: (k -> *) -> *).
HasNormalForm (d f) (x f) (x Uninterpreted) =>
Proxy d -> Rep (Interpret (d f)) (x Uninterpreted) -> Rep I (x f)
denormalize1 Proxy d
p (Rep (Interpret (d f)) (x Uninterpreted) -> Rep I (x f))
-> f (Rep (Interpret (d f)) (x Uninterpreted)) -> f (Rep I (x f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rep (Interpret (d f)) (x Uninterpreted)
-> f (Rep (Interpret (d f)) (x Uninterpreted))
f (Proxy d -> Rep I (x f) -> Rep (Interpret (d f)) (x Uninterpreted)
forall k dom (d :: (k -> *) -> dom) (f :: k -> *)
       (x :: (k -> *) -> *).
HasNormalForm (d f) (x f) (x Uninterpreted) =>
Proxy d -> Rep I (x f) -> Rep (Interpret (d f)) (x Uninterpreted)
normalize1 Proxy d
p Rep I (x f)
a)

interpretedLens :: Lens' (Interpret d x) (Interpreted d x)
interpretedLens :: (Interpreted d x -> f (Interpreted d x))
-> Interpret d x -> f (Interpret d x)
interpretedLens Interpreted d x -> f (Interpreted d x)
f (Interpret Interpreted d x
x) = Interpreted d x -> Interpret d x
forall dom (d :: dom) x. Interpreted d x -> Interpret d x
Interpret (Interpreted d x -> Interpret d x)
-> f (Interpreted d x) -> f (Interpret d x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Interpreted d x -> f (Interpreted d x)
f Interpreted d x
x

standardInterpretationLens :: forall d f x.
     StandardInterpretation d f
  => Proxy d
  -> Lens' (Interpret (d f) (Uninterpreted x)) (f x)
standardInterpretationLens :: Proxy d -> Lens' (Interpret (d f) (Uninterpreted x)) (f x)
standardInterpretationLens Proxy d
p f x -> f (f x)
f Interpret (d f) (Uninterpreted x)
x =
    Proxy d -> f x -> Interpret (d f) (Uninterpreted x)
forall k dom (d :: (k -> *) -> dom) (f :: k -> *) (x :: k).
StandardInterpretation d f =>
Proxy d -> f x -> Interpret (d f) (Uninterpreted x)
toStandardInterpretation Proxy d
p (f x -> Interpret (d f) (Uninterpreted x))
-> f (f x) -> f (Interpret (d f) (Uninterpreted x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      f x -> f (f x)
f (Proxy d -> Interpret (d f) (Uninterpreted x) -> f x
forall k dom (d :: (k -> *) -> dom) (f :: k -> *) (x :: k).
StandardInterpretation d f =>
Proxy d -> Interpret (d f) (Uninterpreted x) -> f x
fromStandardInterpretation Proxy d
p Interpret (d f) (Uninterpreted x)
x)