180 lines
4.5 KiB
Idris
180 lines
4.5 KiB
Idris
module Data.Profunctor.Costrong
|
|
|
|
import Data.Morphisms
|
|
import Data.Tensor
|
|
import Data.Profunctor.Functor
|
|
import Data.Profunctor.Types
|
|
|
|
%default total
|
|
|
|
public export
|
|
interface Profunctor p => GenCostrong (0 ten : Type -> Type -> Type) p where
|
|
costrongl : p (a `ten` c) (b `ten` c) -> p a b
|
|
costrongr : p (c `ten` a) (c `ten` b) -> p a b
|
|
|
|
|
|
public export
|
|
Costrong : (p : Type -> Type -> Type) -> Type
|
|
Costrong = GenCostrong Pair
|
|
|
|
public export
|
|
unfirst : Costrong p => p (a, c) (b, c) -> p a b
|
|
unfirst = costrongl {ten=Pair}
|
|
|
|
public export
|
|
unsecond : Costrong p => p (c, a) (c, b) -> p a b
|
|
unsecond = costrongr {ten=Pair}
|
|
|
|
public export
|
|
Cochoice : (p : Type -> Type -> Type) -> Type
|
|
Cochoice = GenCostrong Either
|
|
|
|
public export
|
|
unleft : Cochoice p => p (Either a c) (Either b c) -> p a b
|
|
unleft = costrongl {ten=Either}
|
|
|
|
public export
|
|
unright : Cochoice p => p (Either c a) (Either c b) -> p a b
|
|
unright = costrongr {ten=Either}
|
|
|
|
-- Implementations
|
|
|
|
export
|
|
GenCostrong Pair Tagged where
|
|
costrongl (Tag (x,_)) = Tag x
|
|
costrongr (Tag (_,x)) = Tag x
|
|
|
|
|
|
-- Tambara
|
|
|
|
public export
|
|
data GenCotambara : (ten, p : Type -> Type -> Type) -> Type -> Type -> Type where
|
|
MkCotambara : GenCostrong ten q => q :-> p -> q a b -> GenCotambara ten p a b
|
|
|
|
export
|
|
Profunctor (GenCotambara ten p) where
|
|
lmap f (MkCotambara n p) = MkCotambara n (lmap f p)
|
|
rmap f (MkCotambara n p) = MkCotambara n (rmap f p)
|
|
dimap f g (MkCotambara n p) = MkCotambara n (dimap f g p)
|
|
|
|
export
|
|
ProfunctorFunctor (GenCotambara ten) where
|
|
promap f (MkCotambara n p) = MkCotambara (f . n) p
|
|
|
|
export
|
|
GenCostrong ten (GenCotambara ten p) where
|
|
costrongl (MkCotambara @{costr} n p) = MkCotambara n (costrongl @{costr} p)
|
|
costrongr (MkCotambara @{costr} n p) = MkCotambara n (costrongr @{costr} p)
|
|
|
|
export
|
|
ProfunctorComonad (GenCotambara ten) where
|
|
proextract (MkCotambara n p) = n p
|
|
produplicate (MkCotambara n p) = MkCotambara id (MkCotambara n p)
|
|
|
|
export
|
|
Functor (GenCotambara ten p a) where
|
|
map = rmap
|
|
|
|
|
|
export
|
|
gencotambara : GenCostrong ten p => p :-> q -> p :-> GenCotambara ten q
|
|
gencotambara f = MkCotambara f
|
|
|
|
export
|
|
ungencotambara : Tensor ten i => Profunctor q => p :-> GenCotambara ten q -> p :-> q
|
|
ungencotambara f p = proextract (f p)
|
|
|
|
|
|
public export
|
|
Cotambara : (p : Type -> Type -> Type) -> Type -> Type -> Type
|
|
Cotambara = GenCotambara Pair
|
|
|
|
export
|
|
cotambara : Costrong p => p :-> q -> p :-> Cotambara q
|
|
cotambara = gencotambara
|
|
|
|
export
|
|
uncotambara : Profunctor q => p :-> Cotambara q -> p :-> q
|
|
uncotambara = ungencotambara
|
|
|
|
|
|
public export
|
|
CotambaraSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
|
|
CotambaraSum = GenCotambara Either
|
|
|
|
export
|
|
cotambaraSum : Cochoice p => p :-> q -> p :-> CotambaraSum q
|
|
cotambaraSum = gencotambara
|
|
|
|
export
|
|
uncotambaraSum : Profunctor q => p :-> CotambaraSum q -> p :-> q
|
|
uncotambaraSum = ungencotambara
|
|
|
|
|
|
-- Copastro
|
|
|
|
public export
|
|
record GenCopastro (ten, p : Type -> Type -> Type) a b where
|
|
constructor MkCopastro
|
|
runCopastro : forall q. GenCostrong ten q => p :-> q -> q a b
|
|
|
|
export
|
|
Profunctor (GenCopastro ten p) where
|
|
dimap f g (MkCopastro h) = MkCopastro $ \n => dimap f g (h n)
|
|
lmap f (MkCopastro h) = MkCopastro $ \n => lmap f (h n)
|
|
rmap f (MkCopastro h) = MkCopastro $ \n => rmap f (h n)
|
|
|
|
export
|
|
ProfunctorFunctor (GenCopastro ten) where
|
|
promap f (MkCopastro h) = MkCopastro $ \n => h (n . f)
|
|
|
|
export
|
|
ProfunctorMonad (GenCopastro ten) where
|
|
propure p = MkCopastro ($ p)
|
|
projoin p = MkCopastro $ \x => runCopastro p (\y => runCopastro y x)
|
|
|
|
export
|
|
GenCostrong ten (GenCopastro ten p) where
|
|
costrongl (MkCopastro h) = MkCopastro $ \n => costrongl {ten} (h n)
|
|
costrongr (MkCopastro h) = MkCopastro $ \n => costrongr {ten} (h n)
|
|
|
|
export
|
|
ProfunctorAdjunction (GenCopastro ten) (GenCotambara ten) where
|
|
prounit p = MkCotambara id (propure {t=GenCopastro ten} p)
|
|
procounit (MkCopastro h) = proextract (h id)
|
|
|
|
|
|
export
|
|
gencopastro : GenCostrong ten q => p :-> q -> GenCopastro ten p :-> q
|
|
gencopastro f (MkCopastro h) = h f
|
|
|
|
export
|
|
ungencopastro : Tensor ten i => GenCopastro ten p :-> q -> p :-> q
|
|
ungencopastro f x = f (MkCopastro ($ x))
|
|
|
|
|
|
public export
|
|
Copastro : (p : Type -> Type -> Type) -> Type -> Type -> Type
|
|
Copastro = GenCopastro Pair
|
|
|
|
export
|
|
copastro : Costrong q => p :-> q -> Copastro p :-> q
|
|
copastro = gencopastro
|
|
|
|
export
|
|
uncopastro : Copastro p :-> q -> p :-> q
|
|
uncopastro = ungencopastro
|
|
|
|
|
|
public export
|
|
CopastroSum : (p : Type -> Type -> Type) -> Type -> Type -> Type
|
|
CopastroSum = GenCopastro Either
|
|
|
|
export
|
|
copastroSum : Cochoice q => p :-> q -> CopastroSum p :-> q
|
|
copastroSum = gencopastro
|
|
|
|
export
|
|
uncopastroSum : CopastroSum p :-> q -> p :-> q
|
|
uncopastroSum = ungencopastro
|