Define new profunctors Forget and Coforget

This commit is contained in:
Kiana Sheibani 2023-03-08 15:05:07 -05:00
parent 99ff1476aa
commit 7ff2746ab4
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
6 changed files with 127 additions and 0 deletions

View file

@ -89,6 +89,16 @@ GenCostrong Pair Tagged where
costrongl (Tag (x,_)) = Tag x
costrongr (Tag (_,x)) = Tag x
export
GenCostrong Either (Forget r) where
costrongl (MkForget k) = MkForget (k . Left)
costrongr (MkForget k) = MkForget (k . Right)
export
GenCostrong Pair (Coforget r) where
costrongl (MkCoforget k) = MkCoforget (fst . k)
costrongr (MkCoforget k) = MkCoforget (snd . k)
------------------------------------------------------------------------------
-- Cotambara

View file

@ -1,5 +1,6 @@
module Data.Profunctor.Representable
import Control.Applicative.Const
import Control.Monad.Identity
import Data.Morphisms
import Data.Profunctor
@ -61,6 +62,10 @@ export
Functor f => Representable (Star f) f where
tabulate = MkStar
export
Representable (Forget r) (Const r) where
tabulate = MkForget . (runConst .)
export
Corepresentable Morphism Identity where
cotabulate f = Mor (f . Id)
@ -75,3 +80,7 @@ namespace Corepresentable
export
Functor f => Corepresentable (Costar f) f where
cotabulate = MkCostar
export
Corepresentable (Coforget r) (Const r) where
cotabulate = MkCoforget . (. MkConst)

View file

@ -1,5 +1,6 @@
module Data.Profunctor.Sieve
import Control.Applicative.Const
import Control.Monad.Identity
import Data.Morphisms
import Data.Profunctor
@ -47,6 +48,10 @@ export
Functor f => Sieve (Star f) f where
sieve = applyStar
export
Sieve (Forget r) (Const r) where
sieve (MkForget k) = MkConst . k
export
Cosieve Morphism Identity where
@ -62,3 +67,7 @@ namespace Cosieve
export
Functor f => Cosieve (Costar f) f where
cosieve = applyCostar
export
Cosieve (Coforget r) (Const r) where
cosieve (MkCoforget k) = k . runConst

View file

@ -132,6 +132,21 @@ GenStrong Either Tagged where
strongl (Tag x) = Tag (Left x)
strongr (Tag x) = Tag (Right x)
export
GenStrong Pair (Forget r) where
strongl (MkForget k) = MkForget (k . fst)
strongr (MkForget k) = MkForget (k . snd)
export
Monoid r => GenStrong Either (Forget r) where
strongl (MkForget k) = MkForget (either k (const neutral))
strongr (MkForget k) = MkForget (either (const neutral) k)
export
GenStrong Either (Coforget r) where
strongl (MkCoforget k) = MkCoforget (Left . k)
strongr (MkCoforget k) = MkCoforget (Right . k)
------------------------------------------------------------------------------
-- Tambara

View file

@ -1,5 +1,6 @@
module Data.Profunctor.Traversing
import Control.Applicative.Const
import Control.Monad.Identity
import Data.Morphisms
import Data.Tensor
@ -106,6 +107,11 @@ Applicative f => Traversing (Star f) where
traverse' (MkStar p) = MkStar (traverse p)
wander f (MkStar p) = MkStar (f p)
export
Monoid r => Traversing (Forget r) where
traverse' (MkForget k) = MkForget (foldMap k)
wander f (MkForget k) = MkForget (runConst . f (MkConst . k))
------------------------------------------------------------------------------
-- CofreeTraversing

View file

@ -192,3 +192,81 @@ Profunctor Tagged where
dimap _ f (Tag x) = Tag (f x)
lmap = const retag
rmap f (Tag x) = Tag (f x)
||| `Forget r` is equivalent to `Star (Const r)`.
public export
record Forget {0 k : Type} r a (b : k) where
constructor MkForget
runForget : a -> r
public export
reforget : Forget r a b -> Forget r a c
reforget (MkForget k) = MkForget k
export
Functor (Forget r a) where
map _ = reforget
export
Contravariant (Forget {k=Type} r a) where
contramap _ = reforget
export
Monoid r => Applicative (Forget r a) where
pure _ = MkForget (const neutral)
MkForget f <*> MkForget g = MkForget (f <+> g)
export
Monoid r => Monad (Forget {k=Type} r a) where
join = reforget
(>>=) = reforget .: const
export
Foldable (Forget r a) where
foldr _ x _ = x
foldl _ x _ = x
null = const True
foldlM _ x _ = pure x
toList _ = []
foldMap _ _ = neutral
export
Traversable (Forget r a) where
traverse _ = pure . reforget
export
Profunctor (Forget r) where
dimap f _ (MkForget k) = MkForget (k . f)
lmap f (MkForget k) = MkForget (k . f)
rmap = map
||| `Coforget r` is equivalent to `Costar (Const r)`.
public export
record Coforget {0 k : Type} r (a : k) b where
constructor MkCoforget
runCoforget : r -> b
public export
recoforget : Coforget r a c -> Coforget r b c
recoforget (MkCoforget k) = MkCoforget k
export
Functor (Coforget r a) where
map f (MkCoforget k) = MkCoforget (f . k)
export
Applicative (Coforget r a) where
pure = MkCoforget . const
MkCoforget f <*> MkCoforget g = MkCoforget (\r => f r (g r))
export
Monad (Coforget r a) where
MkCoforget k >>= f = MkCoforget (\r => runCoforget (f $ k r) r)
export
Profunctor (Coforget f) where
dimap _ f (MkCoforget k) = MkCoforget (f . k)
lmap _ = recoforget
rmap = map