{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
module Data.Profunctor.Composition.List where
import Data.Profunctor
import Data.Profunctor.Composition
import Data.Type.List
data PList (ps :: [* -> * -> *]) (a :: *) (b :: *) where
Hom :: { unHom :: a -> b } -> PList '[] a b
P :: { 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 l r (Hom f) = Hom (r . f . l)
instance Profunctor p => Profunctor (PList '[p]) where
dimap l r (P p) = P (dimap l r p)
instance (Profunctor p, Profunctor (PList (q ': qs))) => Profunctor (PList (p ': q ': qs)) where
dimap l r (PComp p ps) = PComp (lmap l p) (rmap r 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 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 (Procompose q (Hom f)) = lmap f q
punappend q = Procompose q (Hom id)
toPlainP (Hom f) = f
fromPlainP f = Hom f
instance Profunctor p => IsPList '[p] where
pappend (Procompose (Hom f) (P p)) = P (rmap f p)
pappend (Procompose q@P{} (P p)) = PComp p q
pappend (Procompose q@PComp{} (P p)) = PComp p q
punappend p@P{} = Procompose (Hom id) p
punappend (PComp p qs) = Procompose qs (P p)
toPlainP (P p) = p
fromPlainP p = P p
instance IsPList (q ': qs) => IsPList (p ': q ': qs) where
pappend (Procompose q (PComp p ps)) = PComp p (pappend (Procompose q ps))
punappend (PComp p pq) = case punappend pq of Procompose q ps -> Procompose q (PComp p ps)
toPlainP (PComp p pq) = Procompose (toPlainP pq) p
fromPlainP (Procompose pq p) = PComp p (fromPlainP pq)