gen_lens.hs

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

-- base
import Data.Kind
import Data.Proxy
import Data.Type.Bool
import Data.Type.Equality

import GHC.Generics
import GHC.TypeLits

-- mtl
import Control.Monad.State

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 GenMonoLens (cxt :: (Type -> Type) -> Constraint) (r :: Type -> Type) where
    type MonoLensArr cxt r s :: [Type]

    genMonoLens :: Proxy (r x) -> Proxy s -> Proxy cxt -> (forall f. cxt f => (r x -> f (r x)) -> s -> f s) -> HList (MonoLensArr cxt r s)



instance GenMonoLens cxt U1 where
    type MonoLensArr cxt U1 s = '[]

    genMonoLens _ _ _ _ = Z



instance GenMonoLens Functor c => GenMonoLens Functor (D1 m c) where
    type MonoLensArr Functor (D1 m c) s = MonoLensArr Functor c s

    genMonoLens _ s cxt l = genMonoLens (Proxy :: Proxy (c x)) s cxt (l . m1L)

instance GenMonoLens Functor (S1 m (Rec0 v)) where
    type MonoLensArr Functor (S1 m (Rec0 v)) s = '[Opt Functor s s v v]

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

instance GenMonoLens Applicative (S1 m (Rec0 v)) where
    type MonoLensArr Applicative (S1 m (Rec0 v)) s = '[Opt Applicative s s v v]

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

instance GenMonoLens Functor c => GenMonoLens Functor (C1 ('MetaCons sym f t) c) where
    type MonoLensArr Functor (C1 ('MetaCons sym f t) c) s = '[Constr sym (HList (MonoLensArr Functor c s))]

    genMonoLens r s cxt l = S (C (genMonoLens (Proxy :: Proxy (c x)) s cxt (l . m1L))) Z

instance GenMonoLens Applicative c => GenMonoLens Applicative (C1 ('MetaCons sym f t) c) where
    type MonoLensArr Applicative (C1 ('MetaCons sym f t) c) s = '[Constr sym (HList (MonoLensArr Applicative c s))]

    genMonoLens r s cxt l = S (C (genMonoLens (Proxy :: Proxy (c x)) s cxt (l . m1L))) Z



instance (GenMonoLens Functor f, GenMonoLens Functor g) => GenMonoLens Functor (f :*: g) where
    type MonoLensArr Functor (f :*: g) s = MonoLensArr Functor f s ++ MonoLensArr Functor g s

    genMonoLens r s cxt l = genMonoLens (Proxy :: Proxy (f x)) s cxt (l . p1L) `happend` genMonoLens (Proxy :: Proxy (g x)) s cxt (l . p2L)

instance (GenMonoLens Applicative f, GenMonoLens Applicative g) => GenMonoLens Applicative (f :*: g) where
    type MonoLensArr Applicative (f :*: g) s = MonoLensArr Applicative f s ++ MonoLensArr Applicative g s

    genMonoLens r s cxt l = genMonoLens (Proxy :: Proxy (f x)) s cxt (l . p1L) `happend` genMonoLens (Proxy :: Proxy (g x)) s cxt (l . p2L)



instance (GenMonoLens Applicative f, GenMonoLens Applicative g) => GenMonoLens Functor (f :+: g) where
    type MonoLensArr Functor (f :+: g) s = MonoLensArr Applicative f s ++ MonoLensArr Applicative g s

    genMonoLens r s cxt l = happend
        (genMonoLens (Proxy :: Proxy (f x)) s (Proxy :: Proxy Applicative) (l . l1L))
        (genMonoLens (Proxy :: Proxy (g x)) s (Proxy :: Proxy Applicative) (l . r1L))




genericMonoLens
    :: (Generic t, GenMonoLens Functor (Rep t))
    => Proxy t -> HList (MonoLensArr Functor (Rep t) t)
genericMonoLens p = genMonoLens Proxy p (Proxy :: Proxy Functor) ftL


S (C (S fstOpt (S sndOpt Z))) Z = genericMonoLens (Proxy :: Proxy (x, 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

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

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

l1L :: Traversal ((f :+: g) x) ((f1 :+: g) x) (f x) (f1 x)
l1L f v = case v of
    L1 v' -> L1 <$> f v'
    R1 v' -> pure (R1 v')

r1L :: Traversal ((f :+: g) x) ((f :+: g1) x) (g x) (g1 x)
r1L f v = case v of
    R1 v' -> R1 <$> f v'
    L1 v' -> pure (L1 v')