gen_poly_lens.hs

{-# LANGUAGE RankNTypes, TypeInType, TypeOperators, GADTs, TypeFamilies,
    ConstraintKinds, FlexibleInstances, MultiParamTypeClasses, FlexibleContexts,
    UndecidableInstances, ScopedTypeVariables, DeriveGeneric #-}

-- base
import Data.Kind
import Data.Proxy

import GHC.Generics
import GHC.TypeLits

newtype Constr (sym :: Symbol) xs = C xs
    deriving (Eq, Show, Ord)

data HList xs where
    Z :: HList '[]
    S :: a -> HList xs -> HList (a ': xs)

type family (++) (xs :: [k]) (ys :: [k]) :: [k] where
    '[] ++ xs       = xs
    (x ': xs) ++ ys = x ': (xs ++ ys)

happend :: HList xs -> HList ys -> HList (xs ++ ys)
happend xs ys = case xs of
    Z       -> ys
    S x xs' -> S x (happend xs' ys)

data Opt cxt s t a b = O (forall f. cxt f => (a -> f b) -> s -> f t)
type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t

class GenLens (cxt :: (Type -> Type) -> Constraint) (a :: Type -> Type) (b :: Type -> Type) where
    type GenLensArr cxt s t a b:: [Type]

    genLens
        :: Proxy (a x, b x)
        -> Proxy (s, t)
        -> Proxy cxt
        -> (forall f. cxt f => (a x -> f (b x)) -> s -> f t)
        -> HList (GenLensArr cxt s t a b)

instance GenLens cxt U1 U1 where
    type GenLensArr cxt s t U1 U1 = '[]

    genLens _ _ _ _ = Z

instance GenLens Functor a b => GenLens Functor (D1 m a) (D1 m b) where
    type GenLensArr Functor s t (D1 m a) (D1 m b) = GenLensArr Functor s t a b

    genLens _ st cxt l = genLens (Proxy :: Proxy (a x, b x)) st cxt (l . m1L)

instance GenLens Functor (S1 m (Rec0 a)) (S1 m (Rec0 b)) where
    type GenLensArr Functor s t (S1 m (Rec0 a)) (S1 m (Rec0 b)) = '[Opt Functor s t a b]

    genLens _ _ _ l = S (O (l . m1L . k1L)) Z

instance GenLens Functor a b => GenLens Functor (C1 ('MetaCons sym f t) a) (C1 ('MetaCons sym f t) b) where
    type GenLensArr Functor s t' (C1 ('MetaCons sym f t) a) (C1 ('MetaCons sym f t) b) =
            '[Constr sym (HList (GenLensArr Functor s t' a b))]

    genLens _ st cxt l = S (C (genLens (Proxy :: Proxy (a x, b x)) st cxt (l . m1L))) Z

-- instance (GenLens Functor a b, GenLens Functor a1 b1) => GenLens Functor (a :*: a1) (b :*: b1) where
--     type GenLensArr Functor s t (a :*: a1) (b :*: b1) = GenLensArr Functor s t a b ++ GenLensArr Functor s t a1 b1

--     genLens _ st cxt l = genLens (Proxy :: Proxy (a x, b x)) st cxt (l . p1L) `happend` genLens (Proxy :: Proxy (a1 x, b1 x)) st cxt (l . p2L)


genPolyLens
    :: forall s t. (GenLens Functor (Rep s) (Rep t), Generic s, Generic t)
    => Proxy (s, t)
    -> HList (GenLensArr Functor s t (Rep s) (Rep t))
genPolyLens p =
    genLens
        (Proxy :: Proxy (Rep s x, Rep t x))
        (Proxy :: Proxy (s, t))
        (Proxy :: Proxy Functor)
        ftL

genMonoLens
    :: forall s. (GenLens Functor (Rep s) (Rep s), Generic s)
    => Proxy s
    -> HList (GenLensArr Functor s s (Rep s) (Rep s))
genMonoLens p = genPolyLens (Proxy :: Proxy (s, s))

data T a = T a deriving Generic

S (C (S opt Z)) Z = genPolyLens (Proxy :: Proxy (T x, T y))

ftL :: (Generic s, Generic t) => Lens s t (Rep s x) (Rep t x)
ftL f v = to <$> f (from v)

m1L :: Lens (M1 i c f p) (M1 i d g r) (f p) (g r)
m1L f (M1 v) = M1 <$> f v

k1L :: Lens (K1 i a p) (K1 i b r) a b
k1L f (K1 v) = K1 <$> f v

p1L :: Lens ((a :*: p) x) ((b :*: p) x) (a x) (b x)
p1L f (l :*: r) = (:*: r) <$> f l

p2L :: Lens ((p :*: a) x) ((p :*: b) x) (a x) (b x)
p2L f (l :*: r) = (l :*:) <$> f r