{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE RoleAnnotations #-}
module Control.Lens.Internal.Context
( IndexedFunctor(..)
, IndexedComonad(..)
, IndexedComonadStore(..)
, Sellable(..)
, Context(..), Context'
, Pretext(..), Pretext'
, PretextT(..), PretextT'
) where
import Prelude ()
import Control.Arrow
import qualified Control.Category as C
import Control.Comonad
import Control.Comonad.Store.Class
import Control.Lens.Internal.Indexed
import Control.Lens.Internal.Prelude
import Data.Kind
import Data.Profunctor.Rep
import Prelude hiding ((.),id)
class IndexedFunctor w where
ifmap :: (s -> t) -> w a b s -> w a b t
class IndexedFunctor w => IndexedComonad w where
{-# MINIMAL iextract, (iduplicate | iextend) #-}
:: w a a t -> t
iduplicate :: w a c t -> w a b (w b c t)
iduplicate = (w b c t -> w b c t) -> w a c t -> w a b (w b c t)
forall b c t r a. (w b c t -> r) -> w a c t -> w a b r
forall (w :: * -> * -> * -> *) b c t r a.
IndexedComonad w =>
(w b c t -> r) -> w a c t -> w a b r
iextend w b c t -> w b c t
forall a. a -> a
id
{-# INLINE iduplicate #-}
iextend :: (w b c t -> r) -> w a c t -> w a b r
iextend w b c t -> r
f = (w b c t -> r) -> w a b (w b c t) -> w a b r
forall s t a b. (s -> t) -> w a b s -> w a b t
forall (w :: * -> * -> * -> *) s t a b.
IndexedFunctor w =>
(s -> t) -> w a b s -> w a b t
ifmap w b c t -> r
f (w a b (w b c t) -> w a b r)
-> (w a c t -> w a b (w b c t)) -> w a c t -> w a b r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. w a c t -> w a b (w b c t)
forall a c t b. w a c t -> w a b (w b c t)
forall (w :: * -> * -> * -> *) a c t b.
IndexedComonad w =>
w a c t -> w a b (w b c t)
iduplicate
{-# INLINE iextend #-}
class IndexedComonad w => IndexedComonadStore w where
ipos :: w a c t -> a
ipeek :: c -> w a c t -> t
ipeek c
c = w c c t -> t
forall a t. w a a t -> t
forall (w :: * -> * -> * -> *) a t.
IndexedComonad w =>
w a a t -> t
iextract (w c c t -> t) -> (w a c t -> w c c t) -> w a c t -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> w a c t -> w c c t
forall b a c t. b -> w a c t -> w b c t
forall (w :: * -> * -> * -> *) b a c t.
IndexedComonadStore w =>
b -> w a c t -> w b c t
iseek c
c
{-# INLINE ipeek #-}
ipeeks :: (a -> c) -> w a c t -> t
ipeeks a -> c
f = w c c t -> t
forall a t. w a a t -> t
forall (w :: * -> * -> * -> *) a t.
IndexedComonad w =>
w a a t -> t
iextract (w c c t -> t) -> (w a c t -> w c c t) -> w a c t -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> c) -> w a c t -> w c c t
forall a b c t. (a -> b) -> w a c t -> w b c t
forall (w :: * -> * -> * -> *) a b c t.
IndexedComonadStore w =>
(a -> b) -> w a c t -> w b c t
iseeks a -> c
f
{-# INLINE ipeeks #-}
iseek :: b -> w a c t -> w b c t
iseeks :: (a -> b) -> w a c t -> w b c t
iexperiment :: Functor f => (b -> f c) -> w b c t -> f t
iexperiment b -> f c
bfc w b c t
wbct = (c -> w b c t -> t
forall c a t. c -> w a c t -> t
forall (w :: * -> * -> * -> *) c a t.
IndexedComonadStore w =>
c -> w a c t -> t
`ipeek` w b c t
wbct) (c -> t) -> f c -> f t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> f c
bfc (w b c t -> b
forall a c t. w a c t -> a
forall (w :: * -> * -> * -> *) a c t.
IndexedComonadStore w =>
w a c t -> a
ipos w b c t
wbct)
{-# INLINE iexperiment #-}
context :: w a b t -> Context a b t
context w a b t
wabt = (b -> t) -> a -> Context a b t
forall a b t. (b -> t) -> a -> Context a b t
Context (b -> w a b t -> t
forall c a t. c -> w a c t -> t
forall (w :: * -> * -> * -> *) c a t.
IndexedComonadStore w =>
c -> w a c t -> t
`ipeek` w a b t
wabt) (w a b t -> a
forall a c t. w a c t -> a
forall (w :: * -> * -> * -> *) a c t.
IndexedComonadStore w =>
w a c t -> a
ipos w a b t
wabt)
{-# INLINE context #-}
class Corepresentable p => Sellable p w | w -> p where
sell :: p a (w a b b)
data Context a b t = Context (b -> t) a
instance IndexedFunctor Context where
ifmap :: forall s t a b. (s -> t) -> Context a b s -> Context a b t
ifmap s -> t
f (Context b -> s
g a
t) = (b -> t) -> a -> Context a b t
forall a b t. (b -> t) -> a -> Context a b t
Context (s -> t
f (s -> t) -> (b -> s) -> b -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> s
g) a
t
{-# INLINE ifmap #-}
instance IndexedComonad Context where
iextract :: forall a t. Context a a t -> t
iextract (Context a -> t
f a
a) = a -> t
f a
a
{-# INLINE iextract #-}
iduplicate :: forall a c t b. Context a c t -> Context a b (Context b c t)
iduplicate (Context c -> t
f a
a) = (b -> Context b c t) -> a -> Context a b (Context b c t)
forall a b t. (b -> t) -> a -> Context a b t
Context ((c -> t) -> b -> Context b c t
forall a b t. (b -> t) -> a -> Context a b t
Context c -> t
f) a
a
{-# INLINE iduplicate #-}
iextend :: forall b c t r a.
(Context b c t -> r) -> Context a c t -> Context a b r
iextend Context b c t -> r
g (Context c -> t
f a
a) = (b -> r) -> a -> Context a b r
forall a b t. (b -> t) -> a -> Context a b t
Context (Context b c t -> r
g (Context b c t -> r) -> (b -> Context b c t) -> b -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c -> t) -> b -> Context b c t
forall a b t. (b -> t) -> a -> Context a b t
Context c -> t
f) a
a
{-# INLINE iextend #-}
instance IndexedComonadStore Context where
ipos :: forall a c t. Context a c t -> a
ipos (Context c -> t
_ a
a) = a
a
{-# INLINE ipos #-}
ipeek :: forall c a t. c -> Context a c t -> t
ipeek c
b (Context c -> t
g a
_) = c -> t
g c
b
{-# INLINE ipeek #-}
ipeeks :: forall a c t. (a -> c) -> Context a c t -> t
ipeeks a -> c
f (Context c -> t
g a
a) = c -> t
g (a -> c
f a
a)
{-# INLINE ipeeks #-}
iseek :: forall b a c t. b -> Context a c t -> Context b c t
iseek b
a (Context c -> t
g a
_) = (c -> t) -> b -> Context b c t
forall a b t. (b -> t) -> a -> Context a b t
Context c -> t
g b
a
{-# INLINE iseek #-}
iseeks :: forall a b c t. (a -> b) -> Context a c t -> Context b c t
iseeks a -> b
f (Context c -> t
g a
a) = (c -> t) -> b -> Context b c t
forall a b t. (b -> t) -> a -> Context a b t
Context c -> t
g (a -> b
f a
a)
{-# INLINE iseeks #-}
iexperiment :: forall (f :: * -> *) b c t.
Functor f =>
(b -> f c) -> Context b c t -> f t
iexperiment b -> f c
f (Context c -> t
g b
a) = c -> t
g (c -> t) -> f c -> f t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> f c
f b
a
{-# INLINE iexperiment #-}
context :: forall a b t. Context a b t -> Context a b t
context = Context a b t -> Context a b t
forall a. a -> a
id
{-# INLINE context #-}
instance Functor (Context a b) where
fmap :: forall a b. (a -> b) -> Context a b a -> Context a b b
fmap a -> b
f (Context b -> a
g a
t) = (b -> b) -> a -> Context a b b
forall a b t. (b -> t) -> a -> Context a b t
Context (a -> b
f (a -> b) -> (b -> a) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
g) a
t
{-# INLINE fmap #-}
instance a ~ b => Comonad (Context a b) where
extract :: forall a. Context a b a -> a
extract (Context b -> a
f a
a) = b -> a
f a
b
a
{-# INLINE extract #-}
duplicate :: forall a. Context a b a -> Context a b (Context a b a)
duplicate (Context b -> a
f a
a) = (b -> Context a b a) -> a -> Context a b (Context a b a)
forall a b t. (b -> t) -> a -> Context a b t
Context ((b -> a) -> b -> Context b b a
forall a b t. (b -> t) -> a -> Context a b t
Context b -> a
f) a
a
{-# INLINE duplicate #-}
extend :: forall a b. (Context a b a -> b) -> Context a b a -> Context a b b
extend Context a b a -> b
g (Context b -> a
f a
a) = (b -> b) -> a -> Context a b b
forall a b t. (b -> t) -> a -> Context a b t
Context (Context a b a -> b
g (Context a b a -> b) -> (b -> Context a b a) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> a) -> b -> Context b b a
forall a b t. (b -> t) -> a -> Context a b t
Context b -> a
f) a
a
{-# INLINE extend #-}
instance a ~ b => ComonadStore a (Context a b) where
pos :: forall a. Context a b a -> a
pos = Context a b a -> a
forall a c t. Context a c t -> a
forall (w :: * -> * -> * -> *) a c t.
IndexedComonadStore w =>
w a c t -> a
ipos
{-# INLINE pos #-}
peek :: forall a. a -> Context a b a -> a
peek = a -> Context a a a -> a
a -> Context a b a -> a
forall c a t. c -> Context a c t -> t
forall (w :: * -> * -> * -> *) c a t.
IndexedComonadStore w =>
c -> w a c t -> t
ipeek
{-# INLINE peek #-}
peeks :: forall a. (a -> a) -> Context a b a -> a
peeks = (a -> a) -> Context a a a -> a
(a -> a) -> Context a b a -> a
forall a c t. (a -> c) -> Context a c t -> t
forall (w :: * -> * -> * -> *) a c t.
IndexedComonadStore w =>
(a -> c) -> w a c t -> t
ipeeks
{-# INLINE peeks #-}
seek :: forall a. a -> Context a b a -> Context a b a
seek = a -> Context a b a -> Context a b a
forall b a c t. b -> Context a c t -> Context b c t
forall (w :: * -> * -> * -> *) b a c t.
IndexedComonadStore w =>
b -> w a c t -> w b c t
iseek
{-# INLINE seek #-}
seeks :: forall a. (a -> a) -> Context a b a -> Context a b a
seeks = (a -> a) -> Context a b a -> Context a b a
forall a b c t. (a -> b) -> Context a c t -> Context b c t
forall (w :: * -> * -> * -> *) a b c t.
IndexedComonadStore w =>
(a -> b) -> w a c t -> w b c t
iseeks
{-# INLINE seeks #-}
experiment :: forall (f :: * -> *) a.
Functor f =>
(a -> f a) -> Context a b a -> f a
experiment = (a -> f a) -> Context a a a -> f a
(a -> f a) -> Context a b a -> f a
forall (f :: * -> *) b c t.
Functor f =>
(b -> f c) -> Context b c t -> f t
forall (w :: * -> * -> * -> *) (f :: * -> *) b c t.
(IndexedComonadStore w, Functor f) =>
(b -> f c) -> w b c t -> f t
iexperiment
{-# INLINE experiment #-}
instance Sellable (->) Context where
sell :: forall a b. a -> Context a b b
sell = (b -> b) -> a -> Context a b b
forall a b t. (b -> t) -> a -> Context a b t
Context b -> b
forall a. a -> a
id
{-# INLINE sell #-}
type Context' a = Context a a
newtype Pretext p a b t = Pretext { forall (p :: * -> * -> *) a b t.
Pretext p a b t
-> forall (f :: * -> *). Functor f => p a (f b) -> f t
runPretext :: forall f. Functor f => p a (f b) -> f t }
type Pretext' p a = Pretext p a a
instance IndexedFunctor (Pretext p) where
ifmap :: forall s t a b. (s -> t) -> Pretext p a b s -> Pretext p a b t
ifmap s -> t
f (Pretext forall (f :: * -> *). Functor f => p a (f b) -> f s
k) = (forall (f :: * -> *). Functor f => p a (f b) -> f t)
-> Pretext p a b t
forall (p :: * -> * -> *) a b t.
(forall (f :: * -> *). Functor f => p a (f b) -> f t)
-> Pretext p a b t
Pretext ((s -> t) -> f s -> f t
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap s -> t
f (f s -> f t) -> (p a (f b) -> f s) -> p a (f b) -> f t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p a (f b) -> f s
forall (f :: * -> *). Functor f => p a (f b) -> f s
k)
{-# INLINE ifmap #-}
instance Functor (Pretext p a b) where
fmap :: forall a b. (a -> b) -> Pretext p a b a -> Pretext p a b b
fmap = (a -> b) -> Pretext p a b a -> Pretext p a b b
forall s t a b. (s -> t) -> Pretext p a b s -> Pretext p a b t
forall (w :: * -> * -> * -> *) s t a b.
IndexedFunctor w =>
(s -> t) -> w a b s -> w a b t
ifmap
{-# INLINE fmap #-}
instance Conjoined p => IndexedComonad (Pretext p) where
iextract :: forall a t. Pretext p a a t -> t
iextract (Pretext forall (f :: * -> *). Functor f => p a (f a) -> f t
m) = Identity t -> t
forall a. Identity a -> a
runIdentity (Identity t -> t) -> Identity t -> t
forall a b. (a -> b) -> a -> b
$ p a (Identity a) -> Identity t
forall (f :: * -> *). Functor f => p a (f a) -> f t
m ((a -> Identity a) -> p a (Identity a)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr a -> Identity a
forall a. a -> Identity a
Identity)
{-# INLINE iextract #-}
iduplicate :: forall a c t b. Pretext p a c t -> Pretext p a b (Pretext p b c t)
iduplicate (Pretext forall (f :: * -> *). Functor f => p a (f c) -> f t
m) = Compose (Pretext p a b) (Pretext p b c) t
-> Pretext p a b (Pretext p b c t)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose (Pretext p a b) (Pretext p b c) t
-> Pretext p a b (Pretext p b c t))
-> Compose (Pretext p a b) (Pretext p b c) t
-> Pretext p a b (Pretext p b c t)
forall a b. (a -> b) -> a -> b
$ p a (Compose (Pretext p a b) (Pretext p b c) c)
-> Compose (Pretext p a b) (Pretext p b c) t
forall (f :: * -> *). Functor f => p a (f c) -> f t
m (Pretext p a b (Pretext p b c c)
-> Compose (Pretext p a b) (Pretext p b c) c
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Pretext p a b (Pretext p b c c)
-> Compose (Pretext p a b) (Pretext p b c) c)
-> p a (Pretext p a b (Pretext p b c c))
-> p a (Compose (Pretext p a b) (Pretext p b c) c)
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> p a b -> p a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. p b (Pretext p b c c)
-> p (Pretext p a b b) (Pretext p a b (Pretext p b c c))
forall (f :: * -> *) a b. Functor f => p a b -> p (f a) (f b)
forall (p :: * -> * -> *) (f :: * -> *) a b.
(Conjoined p, Functor f) =>
p a b -> p (f a) (f b)
distrib p b (Pretext p b c c)
forall a b. p a (Pretext p a b b)
forall (p :: * -> * -> *) (w :: * -> * -> * -> *) a b.
Sellable p w =>
p a (w a b b)
sell p (Pretext p a b b) (Pretext p a b (Pretext p b c c))
-> p a (Pretext p a b b) -> p a (Pretext p a b (Pretext p b c c))
forall b c a. p b c -> p a b -> p a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
C.. p a (Pretext p a b b)
forall a b. p a (Pretext p a b b)
forall (p :: * -> * -> *) (w :: * -> * -> * -> *) a b.
Sellable p w =>
p a (w a b b)
sell)
{-# INLINE iduplicate #-}
instance (a ~ b, Conjoined p) => Comonad (Pretext p a b) where
extract :: forall a. Pretext p a b a -> a
extract = Pretext p a a a -> a
Pretext p a b a -> a
forall a t. Pretext p a a t -> t
forall (w :: * -> * -> * -> *) a t.
IndexedComonad w =>
w a a t -> t
iextract
{-# INLINE extract #-}
duplicate :: forall a. Pretext p a b a -> Pretext p a b (Pretext p a b a)
duplicate = Pretext p a b a -> Pretext p a b (Pretext p a b a)
Pretext p a b a -> Pretext p a b (Pretext p b b a)
forall a c t b. Pretext p a c t -> Pretext p a b (Pretext p b c t)
forall (w :: * -> * -> * -> *) a c t b.
IndexedComonad w =>
w a c t -> w a b (w b c t)
iduplicate
{-# INLINE duplicate #-}
instance Conjoined p => IndexedComonadStore (Pretext p) where
ipos :: forall a c t. Pretext p a c t -> a
ipos (Pretext forall (f :: * -> *). Functor f => p a (f c) -> f t
m) = Const a t -> a
forall {k} a (b :: k). Const a b -> a
getConst (Const a t -> a) -> Const a t -> a
forall a b. (a -> b) -> a -> b
$ (p a (Const a c) -> Const a t) -> p a (Const a c) -> Const a t
forall (q :: * -> * -> *) a b.
(Representable q, Comonad (Rep q)) =>
q a b -> a -> b
coarr p a (Const a c) -> Const a t
forall (f :: * -> *). Functor f => p a (f c) -> f t
m (p a (Const a c) -> Const a t) -> p a (Const a c) -> Const a t
forall a b. (a -> b) -> a -> b
$ (a -> Const a c) -> p a (Const a c)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr a -> Const a c
forall {k} a (b :: k). a -> Const a b
Const
{-# INLINE ipos #-}
ipeek :: forall c a t. c -> Pretext p a c t -> t
ipeek c
a (Pretext forall (f :: * -> *). Functor f => p a (f c) -> f t
m) = Identity t -> t
forall a. Identity a -> a
runIdentity (Identity t -> t) -> Identity t -> t
forall a b. (a -> b) -> a -> b
$ (p a (Identity c) -> Identity t) -> p a (Identity c) -> Identity t
forall (q :: * -> * -> *) a b.
(Representable q, Comonad (Rep q)) =>
q a b -> a -> b
coarr p a (Identity c) -> Identity t
forall (f :: * -> *). Functor f => p a (f c) -> f t
m (p a (Identity c) -> Identity t) -> p a (Identity c) -> Identity t
forall a b. (a -> b) -> a -> b
$ (a -> Identity c) -> p a (Identity c)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (\a
_ -> c -> Identity c
forall a. a -> Identity a
Identity c
a)
{-# INLINE ipeek #-}
ipeeks :: forall a c t. (a -> c) -> Pretext p a c t -> t
ipeeks a -> c
f (Pretext forall (f :: * -> *). Functor f => p a (f c) -> f t
m) = Identity t -> t
forall a. Identity a -> a
runIdentity (Identity t -> t) -> Identity t -> t
forall a b. (a -> b) -> a -> b
$ (p a (Identity c) -> Identity t) -> p a (Identity c) -> Identity t
forall (q :: * -> * -> *) a b.
(Representable q, Comonad (Rep q)) =>
q a b -> a -> b
coarr p a (Identity c) -> Identity t
forall (f :: * -> *). Functor f => p a (f c) -> f t
m (p a (Identity c) -> Identity t) -> p a (Identity c) -> Identity t
forall a b. (a -> b) -> a -> b
$ (a -> Identity c) -> p a (Identity c)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (c -> Identity c
forall a. a -> Identity a
Identity (c -> Identity c) -> (a -> c) -> a -> Identity c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> c
f)
{-# INLINE ipeeks #-}
iseek :: forall b a c t. b -> Pretext p a c t -> Pretext p b c t
iseek b
a (Pretext forall (f :: * -> *). Functor f => p a (f c) -> f t
m) = (forall (f :: * -> *). Functor f => p b (f c) -> f t)
-> Pretext p b c t
forall (p :: * -> * -> *) a b t.
(forall (f :: * -> *). Functor f => p a (f b) -> f t)
-> Pretext p a b t
Pretext ((p b (f c) -> p a (f c)) -> (p a (f c) -> f t) -> p b (f c) -> f t
forall a b c. (a -> b) -> (b -> c) -> a -> c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap ((a -> b) -> p b (f c) -> p a (f c)
forall a b c. (a -> b) -> p b c -> p a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap (b -> a -> b
forall a b. a -> b -> a
const b
a)) p a (f c) -> f t
forall (f :: * -> *). Functor f => p a (f c) -> f t
m)
{-# INLINE iseek #-}
iseeks :: forall a b c t. (a -> b) -> Pretext p a c t -> Pretext p b c t
iseeks a -> b
f (Pretext forall (f :: * -> *). Functor f => p a (f c) -> f t
m) = (forall (f :: * -> *). Functor f => p b (f c) -> f t)
-> Pretext p b c t
forall (p :: * -> * -> *) a b t.
(forall (f :: * -> *). Functor f => p a (f b) -> f t)
-> Pretext p a b t
Pretext ((p b (f c) -> p a (f c)) -> (p a (f c) -> f t) -> p b (f c) -> f t
forall a b c. (a -> b) -> (b -> c) -> a -> c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap ((a -> b) -> p b (f c) -> p a (f c)
forall a b c. (a -> b) -> p b c -> p a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
f) p a (f c) -> f t
forall (f :: * -> *). Functor f => p a (f c) -> f t
m)
{-# INLINE iseeks #-}
iexperiment :: forall (f :: * -> *) b c t.
Functor f =>
(b -> f c) -> Pretext p b c t -> f t
iexperiment b -> f c
f (Pretext forall (f :: * -> *). Functor f => p b (f c) -> f t
m) = (p b (f c) -> f t) -> p b (f c) -> f t
forall (q :: * -> * -> *) a b.
(Representable q, Comonad (Rep q)) =>
q a b -> a -> b
coarr p b (f c) -> f t
forall (f :: * -> *). Functor f => p b (f c) -> f t
m ((b -> f c) -> p b (f c)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> f c
f)
{-# INLINE iexperiment #-}
context :: forall a b t. Pretext p a b t -> Context a b t
context (Pretext forall (f :: * -> *). Functor f => p a (f b) -> f t
m) = (p a (Context a b b) -> Context a b t)
-> p a (Context a b b) -> Context a b t
forall (q :: * -> * -> *) a b.
(Representable q, Comonad (Rep q)) =>
q a b -> a -> b
coarr p a (Context a b b) -> Context a b t
forall (f :: * -> *). Functor f => p a (f b) -> f t
m ((a -> Context a b b) -> p a (Context a b b)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr a -> Context a b b
forall a b. a -> Context a b b
forall (p :: * -> * -> *) (w :: * -> * -> * -> *) a b.
Sellable p w =>
p a (w a b b)
sell)
{-# INLINE context #-}
instance (a ~ b, Conjoined p) => ComonadStore a (Pretext p a b) where
pos :: forall a. Pretext p a b a -> a
pos = Pretext p a b a -> a
forall a c t. Pretext p a c t -> a
forall (w :: * -> * -> * -> *) a c t.
IndexedComonadStore w =>
w a c t -> a
ipos
{-# INLINE pos #-}
peek :: forall a. a -> Pretext p a b a -> a
peek = a -> Pretext p a a a -> a
a -> Pretext p a b a -> a
forall c a t. c -> Pretext p a c t -> t
forall (w :: * -> * -> * -> *) c a t.
IndexedComonadStore w =>
c -> w a c t -> t
ipeek
{-# INLINE peek #-}
peeks :: forall a. (a -> a) -> Pretext p a b a -> a
peeks = (a -> a) -> Pretext p a a a -> a
(a -> a) -> Pretext p a b a -> a
forall a c t. (a -> c) -> Pretext p a c t -> t
forall (w :: * -> * -> * -> *) a c t.
IndexedComonadStore w =>
(a -> c) -> w a c t -> t
ipeeks
{-# INLINE peeks #-}
seek :: forall a. a -> Pretext p a b a -> Pretext p a b a
seek = a -> Pretext p a b a -> Pretext p a b a
forall b a c t. b -> Pretext p a c t -> Pretext p b c t
forall (w :: * -> * -> * -> *) b a c t.
IndexedComonadStore w =>
b -> w a c t -> w b c t
iseek
{-# INLINE seek #-}
seeks :: forall a. (a -> a) -> Pretext p a b a -> Pretext p a b a
seeks = (a -> a) -> Pretext p a b a -> Pretext p a b a
forall a b c t. (a -> b) -> Pretext p a c t -> Pretext p b c t
forall (w :: * -> * -> * -> *) a b c t.
IndexedComonadStore w =>
(a -> b) -> w a c t -> w b c t
iseeks
{-# INLINE seeks #-}
experiment :: forall (f :: * -> *) a.
Functor f =>
(a -> f a) -> Pretext p a b a -> f a
experiment = (a -> f a) -> Pretext p a a a -> f a
(a -> f a) -> Pretext p a b a -> f a
forall (f :: * -> *) b c t.
Functor f =>
(b -> f c) -> Pretext p b c t -> f t
forall (w :: * -> * -> * -> *) (f :: * -> *) b c t.
(IndexedComonadStore w, Functor f) =>
(b -> f c) -> w b c t -> f t
iexperiment
{-# INLINE experiment #-}
instance Corepresentable p => Sellable p (Pretext p) where
sell :: forall a b. p a (Pretext p a b b)
sell = (Corep p a -> Pretext p a b b) -> p a (Pretext p a b b)
forall d c. (Corep p d -> c) -> p d c
forall (p :: * -> * -> *) d c.
Corepresentable p =>
(Corep p d -> c) -> p d c
cotabulate ((Corep p a -> Pretext p a b b) -> p a (Pretext p a b b))
-> (Corep p a -> Pretext p a b b) -> p a (Pretext p a b b)
forall a b. (a -> b) -> a -> b
$ \ Corep p a
w -> (forall (f :: * -> *). Functor f => p a (f b) -> f b)
-> Pretext p a b b
forall (p :: * -> * -> *) a b t.
(forall (f :: * -> *). Functor f => p a (f b) -> f t)
-> Pretext p a b t
Pretext (p a (f b) -> Corep p a -> f b
forall a b. p a b -> Corep p a -> b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Cosieve p f =>
p a b -> f a -> b
`cosieve` Corep p a
w)
{-# INLINE sell #-}
newtype PretextT p (g :: Type -> Type) a b t = PretextT { forall (p :: * -> * -> *) (g :: * -> *) a b t.
PretextT p g a b t
-> forall (f :: * -> *). Functor f => p a (f b) -> f t
runPretextT :: forall f. Functor f => p a (f b) -> f t }
type role PretextT representational nominal nominal nominal nominal
type PretextT' p g a = PretextT p g a a
instance IndexedFunctor (PretextT p g) where
ifmap :: forall s t a b.
(s -> t) -> PretextT p g a b s -> PretextT p g a b t
ifmap s -> t
f (PretextT forall (f :: * -> *). Functor f => p a (f b) -> f s
k) = (forall (f :: * -> *). Functor f => p a (f b) -> f t)
-> PretextT p g a b t
forall (p :: * -> * -> *) (g :: * -> *) a b t.
(forall (f :: * -> *). Functor f => p a (f b) -> f t)
-> PretextT p g a b t
PretextT ((s -> t) -> f s -> f t
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap s -> t
f (f s -> f t) -> (p a (f b) -> f s) -> p a (f b) -> f t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p a (f b) -> f s
forall (f :: * -> *). Functor f => p a (f b) -> f s
k)
{-# INLINE ifmap #-}
instance Functor (PretextT p g a b) where
fmap :: forall a b. (a -> b) -> PretextT p g a b a -> PretextT p g a b b
fmap = (a -> b) -> PretextT p g a b a -> PretextT p g a b b
forall s t a b.
(s -> t) -> PretextT p g a b s -> PretextT p g a b t
forall (w :: * -> * -> * -> *) s t a b.
IndexedFunctor w =>
(s -> t) -> w a b s -> w a b t
ifmap
{-# INLINE fmap #-}
instance Conjoined p => IndexedComonad (PretextT p g) where
iextract :: forall a t. PretextT p g a a t -> t
iextract (PretextT forall (f :: * -> *). Functor f => p a (f a) -> f t
m) = Identity t -> t
forall a. Identity a -> a
runIdentity (Identity t -> t) -> Identity t -> t
forall a b. (a -> b) -> a -> b
$ p a (Identity a) -> Identity t
forall (f :: * -> *). Functor f => p a (f a) -> f t
m ((a -> Identity a) -> p a (Identity a)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr a -> Identity a
forall a. a -> Identity a
Identity)
{-# INLINE iextract #-}
iduplicate :: forall a c t b.
PretextT p g a c t -> PretextT p g a b (PretextT p g b c t)
iduplicate (PretextT forall (f :: * -> *). Functor f => p a (f c) -> f t
m) = Compose (PretextT p g a b) (PretextT p g b c) t
-> PretextT p g a b (PretextT p g b c t)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose (PretextT p g a b) (PretextT p g b c) t
-> PretextT p g a b (PretextT p g b c t))
-> Compose (PretextT p g a b) (PretextT p g b c) t
-> PretextT p g a b (PretextT p g b c t)
forall a b. (a -> b) -> a -> b
$ p a (Compose (PretextT p g a b) (PretextT p g b c) c)
-> Compose (PretextT p g a b) (PretextT p g b c) t
forall (f :: * -> *). Functor f => p a (f c) -> f t
m (PretextT p g a b (PretextT p g b c c)
-> Compose (PretextT p g a b) (PretextT p g b c) c
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (PretextT p g a b (PretextT p g b c c)
-> Compose (PretextT p g a b) (PretextT p g b c) c)
-> p a (PretextT p g a b (PretextT p g b c c))
-> p a (Compose (PretextT p g a b) (PretextT p g b c) c)
forall a b c (q :: * -> * -> *).
Coercible c b =>
q b c -> p a b -> p a c
forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
(Profunctor p, Coercible c b) =>
q b c -> p a b -> p a c
#. p b (PretextT p g b c c)
-> p (PretextT p g a b b) (PretextT p g a b (PretextT p g b c c))
forall (f :: * -> *) a b. Functor f => p a b -> p (f a) (f b)
forall (p :: * -> * -> *) (f :: * -> *) a b.
(Conjoined p, Functor f) =>
p a b -> p (f a) (f b)
distrib p b (PretextT p g b c c)
forall a b. p a (PretextT p g a b b)
forall (p :: * -> * -> *) (w :: * -> * -> * -> *) a b.
Sellable p w =>
p a (w a b b)
sell p (PretextT p g a b b) (PretextT p g a b (PretextT p g b c c))
-> p a (PretextT p g a b b)
-> p a (PretextT p g a b (PretextT p g b c c))
forall b c a. p b c -> p a b -> p a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
C.. p a (PretextT p g a b b)
forall a b. p a (PretextT p g a b b)
forall (p :: * -> * -> *) (w :: * -> * -> * -> *) a b.
Sellable p w =>
p a (w a b b)
sell)
{-# INLINE iduplicate #-}
instance (a ~ b, Conjoined p) => Comonad (PretextT p g a b) where
extract :: forall a. PretextT p g a b a -> a
extract = PretextT p g a a a -> a
PretextT p g a b a -> a
forall a t. PretextT p g a a t -> t
forall (w :: * -> * -> * -> *) a t.
IndexedComonad w =>
w a a t -> t
iextract
{-# INLINE extract #-}
duplicate :: forall a.
PretextT p g a b a -> PretextT p g a b (PretextT p g a b a)
duplicate = PretextT p g a b a -> PretextT p g a b (PretextT p g a b a)
PretextT p g a b a -> PretextT p g a b (PretextT p g b b a)
forall a c t b.
PretextT p g a c t -> PretextT p g a b (PretextT p g b c t)
forall (w :: * -> * -> * -> *) a c t b.
IndexedComonad w =>
w a c t -> w a b (w b c t)
iduplicate
{-# INLINE duplicate #-}
instance Conjoined p => IndexedComonadStore (PretextT p g) where
ipos :: forall a c t. PretextT p g a c t -> a
ipos (PretextT forall (f :: * -> *). Functor f => p a (f c) -> f t
m) = Const a t -> a
forall {k} a (b :: k). Const a b -> a
getConst (Const a t -> a) -> Const a t -> a
forall a b. (a -> b) -> a -> b
$ (p a (Const a c) -> Const a t) -> p a (Const a c) -> Const a t
forall (q :: * -> * -> *) a b.
(Representable q, Comonad (Rep q)) =>
q a b -> a -> b
coarr p a (Const a c) -> Const a t
forall (f :: * -> *). Functor f => p a (f c) -> f t
m (p a (Const a c) -> Const a t) -> p a (Const a c) -> Const a t
forall a b. (a -> b) -> a -> b
$ (a -> Const a c) -> p a (Const a c)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr a -> Const a c
forall {k} a (b :: k). a -> Const a b
Const
{-# INLINE ipos #-}
ipeek :: forall c a t. c -> PretextT p g a c t -> t
ipeek c
a (PretextT forall (f :: * -> *). Functor f => p a (f c) -> f t
m) = Identity t -> t
forall a. Identity a -> a
runIdentity (Identity t -> t) -> Identity t -> t
forall a b. (a -> b) -> a -> b
$ (p a (Identity c) -> Identity t) -> p a (Identity c) -> Identity t
forall (q :: * -> * -> *) a b.
(Representable q, Comonad (Rep q)) =>
q a b -> a -> b
coarr p a (Identity c) -> Identity t
forall (f :: * -> *). Functor f => p a (f c) -> f t
m (p a (Identity c) -> Identity t) -> p a (Identity c) -> Identity t
forall a b. (a -> b) -> a -> b
$ (a -> Identity c) -> p a (Identity c)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (\a
_ -> c -> Identity c
forall a. a -> Identity a
Identity c
a)
{-# INLINE ipeek #-}
ipeeks :: forall a c t. (a -> c) -> PretextT p g a c t -> t
ipeeks a -> c
f (PretextT forall (f :: * -> *). Functor f => p a (f c) -> f t
m) = Identity t -> t
forall a. Identity a -> a
runIdentity (Identity t -> t) -> Identity t -> t
forall a b. (a -> b) -> a -> b
$ (p a (Identity c) -> Identity t) -> p a (Identity c) -> Identity t
forall (q :: * -> * -> *) a b.
(Representable q, Comonad (Rep q)) =>
q a b -> a -> b
coarr p a (Identity c) -> Identity t
forall (f :: * -> *). Functor f => p a (f c) -> f t
m (p a (Identity c) -> Identity t) -> p a (Identity c) -> Identity t
forall a b. (a -> b) -> a -> b
$ (a -> Identity c) -> p a (Identity c)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (c -> Identity c
forall a. a -> Identity a
Identity (c -> Identity c) -> (a -> c) -> a -> Identity c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> c
f)
{-# INLINE ipeeks #-}
iseek :: forall b a c t. b -> PretextT p g a c t -> PretextT p g b c t
iseek b
a (PretextT forall (f :: * -> *). Functor f => p a (f c) -> f t
m) = (forall (f :: * -> *). Functor f => p b (f c) -> f t)
-> PretextT p g b c t
forall (p :: * -> * -> *) (g :: * -> *) a b t.
(forall (f :: * -> *). Functor f => p a (f b) -> f t)
-> PretextT p g a b t
PretextT ((p b (f c) -> p a (f c)) -> (p a (f c) -> f t) -> p b (f c) -> f t
forall a b c. (a -> b) -> (b -> c) -> a -> c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap ((a -> b) -> p b (f c) -> p a (f c)
forall a b c. (a -> b) -> p b c -> p a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap (b -> a -> b
forall a b. a -> b -> a
const b
a)) p a (f c) -> f t
forall (f :: * -> *). Functor f => p a (f c) -> f t
m)
{-# INLINE iseek #-}
iseeks :: forall a b c t.
(a -> b) -> PretextT p g a c t -> PretextT p g b c t
iseeks a -> b
f (PretextT forall (f :: * -> *). Functor f => p a (f c) -> f t
m) = (forall (f :: * -> *). Functor f => p b (f c) -> f t)
-> PretextT p g b c t
forall (p :: * -> * -> *) (g :: * -> *) a b t.
(forall (f :: * -> *). Functor f => p a (f b) -> f t)
-> PretextT p g a b t
PretextT ((p b (f c) -> p a (f c)) -> (p a (f c) -> f t) -> p b (f c) -> f t
forall a b c. (a -> b) -> (b -> c) -> a -> c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap ((a -> b) -> p b (f c) -> p a (f c)
forall a b c. (a -> b) -> p b c -> p a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap a -> b
f) p a (f c) -> f t
forall (f :: * -> *). Functor f => p a (f c) -> f t
m)
{-# INLINE iseeks #-}
iexperiment :: forall (f :: * -> *) b c t.
Functor f =>
(b -> f c) -> PretextT p g b c t -> f t
iexperiment b -> f c
f (PretextT forall (f :: * -> *). Functor f => p b (f c) -> f t
m) = (p b (f c) -> f t) -> p b (f c) -> f t
forall (q :: * -> * -> *) a b.
(Representable q, Comonad (Rep q)) =>
q a b -> a -> b
coarr p b (f c) -> f t
forall (f :: * -> *). Functor f => p b (f c) -> f t
m ((b -> f c) -> p b (f c)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> f c
f)
{-# INLINE iexperiment #-}
context :: forall a b t. PretextT p g a b t -> Context a b t
context (PretextT forall (f :: * -> *). Functor f => p a (f b) -> f t
m) = (p a (Context a b b) -> Context a b t)
-> p a (Context a b b) -> Context a b t
forall (q :: * -> * -> *) a b.
(Representable q, Comonad (Rep q)) =>
q a b -> a -> b
coarr p a (Context a b b) -> Context a b t
forall (f :: * -> *). Functor f => p a (f b) -> f t
m ((a -> Context a b b) -> p a (Context a b b)
forall b c. (b -> c) -> p b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr a -> Context a b b
forall a b. a -> Context a b b
forall (p :: * -> * -> *) (w :: * -> * -> * -> *) a b.
Sellable p w =>
p a (w a b b)
sell)
{-# INLINE context #-}
instance (a ~ b, Conjoined p) => ComonadStore a (PretextT p g a b) where
pos :: forall a. PretextT p g a b a -> a
pos = PretextT p g a b a -> a
forall a c t. PretextT p g a c t -> a
forall (w :: * -> * -> * -> *) a c t.
IndexedComonadStore w =>
w a c t -> a
ipos
{-# INLINE pos #-}
peek :: forall a. a -> PretextT p g a b a -> a
peek = a -> PretextT p g a a a -> a
a -> PretextT p g a b a -> a
forall c a t. c -> PretextT p g a c t -> t
forall (w :: * -> * -> * -> *) c a t.
IndexedComonadStore w =>
c -> w a c t -> t
ipeek
{-# INLINE peek #-}
peeks :: forall a. (a -> a) -> PretextT p g a b a -> a
peeks = (a -> a) -> PretextT p g a a a -> a
(a -> a) -> PretextT p g a b a -> a
forall a c t. (a -> c) -> PretextT p g a c t -> t
forall (w :: * -> * -> * -> *) a c t.
IndexedComonadStore w =>
(a -> c) -> w a c t -> t
ipeeks
{-# INLINE peeks #-}
seek :: forall a. a -> PretextT p g a b a -> PretextT p g a b a
seek = a -> PretextT p g a b a -> PretextT p g a b a
forall b a c t. b -> PretextT p g a c t -> PretextT p g b c t
forall (w :: * -> * -> * -> *) b a c t.
IndexedComonadStore w =>
b -> w a c t -> w b c t
iseek
{-# INLINE seek #-}
seeks :: forall a. (a -> a) -> PretextT p g a b a -> PretextT p g a b a
seeks = (a -> a) -> PretextT p g a b a -> PretextT p g a b a
forall a b c t.
(a -> b) -> PretextT p g a c t -> PretextT p g b c t
forall (w :: * -> * -> * -> *) a b c t.
IndexedComonadStore w =>
(a -> b) -> w a c t -> w b c t
iseeks
{-# INLINE seeks #-}
experiment :: forall (f :: * -> *) a.
Functor f =>
(a -> f a) -> PretextT p g a b a -> f a
experiment = (a -> f a) -> PretextT p g a a a -> f a
(a -> f a) -> PretextT p g a b a -> f a
forall (f :: * -> *) b c t.
Functor f =>
(b -> f c) -> PretextT p g b c t -> f t
forall (w :: * -> * -> * -> *) (f :: * -> *) b c t.
(IndexedComonadStore w, Functor f) =>
(b -> f c) -> w b c t -> f t
iexperiment
{-# INLINE experiment #-}
instance Corepresentable p => Sellable p (PretextT p g) where
sell :: forall a b. p a (PretextT p g a b b)
sell = (Corep p a -> PretextT p g a b b) -> p a (PretextT p g a b b)
forall d c. (Corep p d -> c) -> p d c
forall (p :: * -> * -> *) d c.
Corepresentable p =>
(Corep p d -> c) -> p d c
cotabulate ((Corep p a -> PretextT p g a b b) -> p a (PretextT p g a b b))
-> (Corep p a -> PretextT p g a b b) -> p a (PretextT p g a b b)
forall a b. (a -> b) -> a -> b
$ \ Corep p a
w -> (forall (f :: * -> *). Functor f => p a (f b) -> f b)
-> PretextT p g a b b
forall (p :: * -> * -> *) (g :: * -> *) a b t.
(forall (f :: * -> *). Functor f => p a (f b) -> f t)
-> PretextT p g a b t
PretextT (p a (f b) -> Corep p a -> f b
forall a b. p a b -> Corep p a -> b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Cosieve p f =>
p a b -> f a -> b
`cosieve` Corep p a
w)
{-# INLINE sell #-}
instance (Profunctor p, Contravariant g) => Contravariant (PretextT p g a b) where
contramap :: forall a' a. (a' -> a) -> PretextT p g a b a -> PretextT p g a b a'
contramap a' -> a
_ = a' -> PretextT p g a b a -> PretextT p g a b a'
forall a b. a -> PretextT p g a b b -> PretextT p g a b a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) ([Char] -> a'
forall a. HasCallStack => [Char] -> a
error [Char]
"contramap: PretextT")
{-# INLINE contramap #-}
coarr :: (Representable q, Comonad (Rep q)) => q a b -> a -> b
coarr :: forall (q :: * -> * -> *) a b.
(Representable q, Comonad (Rep q)) =>
q a b -> a -> b
coarr q a b
qab = Rep q b -> b
forall a. Rep q a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract (Rep q b -> b) -> (a -> Rep q b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. q a b -> a -> Rep q b
forall a b. q a b -> a -> Rep q b
forall (p :: * -> * -> *) (f :: * -> *) a b.
Sieve p f =>
p a b -> a -> f b
sieve q a b
qab
{-# INLINE coarr #-}