{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstrainedClassMethods #-}
module Data.Profunctor.Composition.List where
import Data.Profunctor
import Data.Profunctor.Composition
import Data.Type.List
data PList (ps :: [* -> * -> *]) (a :: *) (b :: *) where
Hom :: { forall a b. PList '[] a b -> a -> b
unHom :: a -> b } -> PList '[] a b
P :: { forall (p :: * -> * -> *) a b. PList '[p] a b -> p a b
unP :: p a b } -> PList '[p] a b
PComp :: p a x -> PList (q ': qs) x b -> PList (p ': q ': qs) a b
instance Profunctor (PList '[]) where
dimap :: forall a b c d.
(a -> b) -> (c -> d) -> PList '[] b c -> PList '[] a d
dimap a -> b
l c -> d
r (Hom b -> c
f) = forall a b. (a -> b) -> PList '[] a b
Hom (c -> d
r forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> c
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
l)
instance Profunctor p => Profunctor (PList '[p]) where
dimap :: forall a b c d.
(a -> b) -> (c -> d) -> PList '[p] b c -> PList '[p] a d
dimap a -> b
l c -> d
r (P p b c
p) = forall (p :: * -> * -> *) a b. p a b -> PList '[p] a b
P (forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> b
l c -> d
r p b c
p)
instance (Profunctor p, Profunctor (PList (q ': qs))) => Profunctor (PList (p ': q ': qs)) where
dimap :: forall a b c d.
(a -> b)
-> (c -> d) -> PList (p : q : qs) b c -> PList (p : q : qs) a d
dimap a -> b
l c -> d
r (PComp p b x
p PList (q : qs) x c
ps) = forall (p :: * -> * -> *) a x (q :: * -> * -> *)
(qs :: [* -> * -> *]) b.
p a x -> PList (q : qs) x b -> PList (p : q : qs) a b
PComp (forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
l p b x
p) (forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap c -> d
r PList (q : qs) x c
ps)
type family PlainP (ps :: [* -> * -> *]) :: * -> * -> *
type instance PlainP '[] = (->)
type instance PlainP '[p] = p
type instance PlainP (p ': q ': qs) = Procompose (PlainP (q ': qs)) p
class IsPList ps where
pappend :: (Profunctor (PList ps), Profunctor (PList qs)) => Procompose (PList qs) (PList ps) :-> PList (ps ++ qs)
punappend :: PList (ps ++ qs) :-> Procompose (PList qs) (PList ps)
toPlainP :: PList ps :-> PlainP ps
fromPlainP :: PlainP ps :-> PList ps
instance IsPList '[] where
pappend :: forall (qs :: [* -> * -> *]).
(Profunctor (PList '[]), Profunctor (PList qs)) =>
Procompose (PList qs) (PList '[]) :-> PList ('[] ++ qs)
pappend (Procompose PList qs x b
q (Hom a -> x
f)) = forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> x
f PList qs x b
q
punappend :: forall (qs :: [* -> * -> *]).
PList ('[] ++ qs) :-> Procompose (PList qs) (PList '[])
punappend PList ('[] ++ qs) a b
q = forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
(q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
Procompose PList ('[] ++ qs) a b
q (forall a b. (a -> b) -> PList '[] a b
Hom forall a. a -> a
id)
toPlainP :: PList '[] :-> PlainP '[]
toPlainP (Hom a -> b
f) = a -> b
f
fromPlainP :: PlainP '[] :-> PList '[]
fromPlainP PlainP '[] a b
f = forall a b. (a -> b) -> PList '[] a b
Hom PlainP '[] a b
f
instance IsPList '[p] where
pappend :: forall (qs :: [* -> * -> *]).
(Profunctor (PList '[p]), Profunctor (PList qs)) =>
Procompose (PList qs) (PList '[p]) :-> PList ('[p] ++ qs)
pappend (Procompose (Hom x -> b
f) PList '[p] a x
p) = forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap x -> b
f PList '[p] a x
p
pappend (Procompose q :: PList qs x b
q@P{} (P p a x
p)) = forall (p :: * -> * -> *) a x (q :: * -> * -> *)
(qs :: [* -> * -> *]) b.
p a x -> PList (q : qs) x b -> PList (p : q : qs) a b
PComp p a x
p PList qs x b
q
pappend (Procompose q :: PList qs x b
q@PComp{} (P p a x
p)) = forall (p :: * -> * -> *) a x (q :: * -> * -> *)
(qs :: [* -> * -> *]) b.
p a x -> PList (q : qs) x b -> PList (p : q : qs) a b
PComp p a x
p PList qs x b
q
punappend :: forall (qs :: [* -> * -> *]).
PList ('[p] ++ qs) :-> Procompose (PList qs) (PList '[p])
punappend p :: PList ('[p] ++ qs) a b
p@P{} = forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
(q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
Procompose (forall a b. (a -> b) -> PList '[] a b
Hom forall a. a -> a
id) PList ('[p] ++ qs) a b
p
punappend (PComp p a x
p PList (q : qs) x b
qs) = forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
(q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
Procompose PList (q : qs) x b
qs (forall (p :: * -> * -> *) a b. p a b -> PList '[p] a b
P p a x
p)
toPlainP :: PList '[p] :-> PlainP '[p]
toPlainP (P p a b
p) = p a b
p
fromPlainP :: PlainP '[p] :-> PList '[p]
fromPlainP PlainP '[p] a b
p = forall (p :: * -> * -> *) a b. p a b -> PList '[p] a b
P PlainP '[p] a b
p
instance (Profunctor (PList (q ': qs)), IsPList (q ': qs)) => IsPList (p ': q ': qs) where
pappend :: forall (qs :: [* -> * -> *]).
(Profunctor (PList (p : q : qs)), Profunctor (PList qs)) =>
Procompose (PList qs) (PList (p : q : qs))
:-> PList ((p : q : qs) ++ qs)
pappend (Procompose PList qs x b
q (PComp p a x
p PList (q : qs) x x
ps)) = forall (p :: * -> * -> *) a x (q :: * -> * -> *)
(qs :: [* -> * -> *]) b.
p a x -> PList (q : qs) x b -> PList (p : q : qs) a b
PComp p a x
p (forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]).
(IsPList ps, Profunctor (PList ps), Profunctor (PList qs)) =>
Procompose (PList qs) (PList ps) :-> PList (ps ++ qs)
pappend (forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
(q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
Procompose PList qs x b
q PList (q : qs) x x
ps))
punappend :: forall (qs :: [* -> * -> *]).
PList ((p : q : qs) ++ qs)
:-> Procompose (PList qs) (PList (p : q : qs))
punappend (PComp p a x
p PList (q : qs) x b
pq) = case forall (ps :: [* -> * -> *]) (qs :: [* -> * -> *]).
IsPList ps =>
PList (ps ++ qs) :-> Procompose (PList qs) (PList ps)
punappend PList (q : qs) x b
pq of Procompose PList qs x b
q PList (q : qs) x x
ps -> forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
(q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
Procompose PList qs x b
q (forall (p :: * -> * -> *) a x (q :: * -> * -> *)
(qs :: [* -> * -> *]) b.
p a x -> PList (q : qs) x b -> PList (p : q : qs) a b
PComp p a x
p PList (q : qs) x x
ps)
toPlainP :: PList (p : q : qs) :-> PlainP (p : q : qs)
toPlainP (PComp p a x
p PList (q : qs) x b
pq) = forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
(q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
Procompose (forall (ps :: [* -> * -> *]). IsPList ps => PList ps :-> PlainP ps
toPlainP PList (q : qs) x b
pq) p a x
p
fromPlainP :: PlainP (p : q : qs) :-> PList (p : q : qs)
fromPlainP (Procompose PlainP (q : qs) x b
pq p a x
p) = forall (p :: * -> * -> *) a x (q :: * -> * -> *)
(qs :: [* -> * -> *]) b.
p a x -> PList (q : qs) x b -> PList (p : q : qs) a b
PComp p a x
p (forall (ps :: [* -> * -> *]). IsPList ps => PlainP ps :-> PList ps
fromPlainP PlainP (q : qs) x b
pq)