module Hask.Core
( Hom, type (~>), type (^)
, Dom, Cod, Cod2, Arr, Enriched, Internal, External, Natural
, Nat(Nat, runNat), nat2, nat3, nat4, runNat2, runNat3, runNat4
, Functor(fmap), first
, Contravariant(contramap), lmap
, Composed(..), type (ยท), composed, associateCompose
, whiskerComposeL
, whiskerComposeR
, lambdaCompose
, rhoCompose
, Post
, fmap1, contramap1
, fmap2
, Bifunctor, bimap
, Profunctor, dimap
, Phantom
, Cocomplete(..)
, Constant(..)
, Complete(..)
, Iso, Iso'
, (-|)(..)
, unitAdj, counitAdj, zipR, absurdL, cozipL
, Curried(..), curried, ccc
, Cocurried(..), cocurried
, Lifted(..)
, (:-)(Sub), Dict(Dict), (\\), type (&), (|-)(implies), _Sub, _Implies, Class(..), (:=>)(..)
, Get(..), _Get, get
, Beget(..), _Beget, beget, (#)
, Un(..), _Un, un
, Via(..), via, mapping, lmapping, swapping, mapping1, firstly, post, pre
, Self(..), _Self
, Semitensor(..)
, I
, Tensor(..)
, Symmetric(..)
, Closed(..)
, Terminal(..)
, Initial(..)
, Copower, type (*)
, Precartesian(..)
, Cartesian
, Precocartesian(..)
, Cocartesian
, Distributive(..)
, CCC
, Semimonoidal(..), ap, ap2Applicative
, Monoidal(..), return
, Cosemimonoidal(..)
, Comonoidal(..)
, Semimonad(..)
, Monad
, Cosemimonad(..)
, Comonad(..)
, Semigroup(..), multM
, Monoid(..), oneM, mappend
, Cosemigroup(..), zeroOp
, Comonoid(..), comultOp
, Strength(..)
, Costrength(..)
, Identity(..)
, HasRan(..)
, HasLan(..)
, Prod(..), runProd, runFst, runSnd, diagProdAdj, sumDiagAdj
, Unit(..)
, Empty(..), No
, Semicategory
, Compose1(..), Compose2(..), ComposeC
, Lim1(..), Lim2(..), Lim3(..), LimC(..)
, Const1(..), Const2(..), ConstC
, Colim1(..), Colim2(..)
, Id0(..), Id1(..), IdC
, Lift1(..), Lift2(..), LiftC, LiftC2
, Copower1(..), Copower2(..), Copower2_1(..)
, Ran1(..), Lan1(..), Lan2(..)
, Constraint
, undefined, ($)
, Either(..), Maybe(..)
, Tagged(..), Proxy(..), Category(..), Void, absurd
) where
import qualified Control.Applicative as Base
import qualified Control.Arrow as Arrow
import Control.Category (Category(..))
import qualified Data.Constraint as Constraint
import Data.Constraint ((:-)(Sub), (\\), Dict(Dict), Class(..), (:=>)(..))
import qualified Data.Functor as Base
import Data.Proxy
import Data.Tagged
import qualified Data.Traversable as Base
import Data.Void
import qualified Prelude
import Prelude (Either(..), ($), either, Bool, undefined, Maybe(..))
import GHC.Exts (Constraint, Any)
import Unsafe.Coerce (unsafeCoerce)
infixr 0 ~>, `Nat`, `Hom`
type family Hom :: i -> i -> k
type instance Hom = (->)
type instance Hom = Nat
type instance Hom = (:-)
type instance Hom = Unit
type instance Hom = Empty
type instance Hom = Prod
type instance Hom = Lift Hom
type instance Hom = (|-)
type (~>) = (Hom :: i -> i -> *)
type Dom (f :: i -> j) = (Hom :: i -> i -> *)
type Dom1 (f :: i -> j -> k) = (Hom :: j -> j -> *)
type Cod (f :: i -> j) = (Hom :: j -> j -> *)
type Cod2 (f :: i -> j -> k) = (Hom :: k -> k -> *)
type Arr (a :: i) = (Hom :: i -> i -> *)
type Enriched (k :: i -> i -> *) = (Hom :: i -> i -> j)
type Internal (k :: i -> i -> *) = (Hom :: i -> i -> i)
type External (k :: i -> i -> j) = (Hom :: i -> i -> *)
type Natural (k :: j -> j -> *) = (Hom :: (i -> j) -> (i -> j) -> *)
infixr 8 ^
type a ^ b = Internal Hom b a
newtype Nat f g = Nat { runNat :: forall a. f a ~> g a }
nat2 :: (forall a b. f a b ~> g a b) -> f ~> g
nat2 f = Nat (Nat f)
nat3 :: (forall a b c. f a b c ~> g a b c) -> f ~> g
nat3 f = Nat (Nat (Nat f))
nat4 :: (forall a b c d. f a b c d ~> g a b c d) -> f ~> g
nat4 f = Nat (Nat (Nat (Nat f)))
runNat2 = runNat . runNat
runNat3 = runNat . runNat . runNat
runNat4 = runNat . runNat . runNat . runNat
instance Category ((~>) :: j -> j -> *) => Category (Nat :: (i -> j) -> (i -> j) -> *) where
id = Nat id
Nat f . Nat g = Nat (f . g)
class Functor (f :: x -> y) where
fmap :: (a ~> b) -> f a ~> f b
instance Functor [] where fmap = Base.fmap
instance Functor Maybe where fmap = Base.fmap
first :: Functor f => (a ~> b) -> f a c ~> f b c
first = runNat . fmap
class Contravariant f where
contramap :: (b ~> a) -> f a ~> f b
lmap :: Contravariant f => (a ~> b) -> f b c ~> f a c
lmap = runNat . contramap
class LimC (p :: i -> Constraint) where
limDict :: Dict (p a)
instance p Any => LimC (p :: i -> Constraint) where
limDict = case unsafeCoerce (id :: p Any :- p Any) :: p Any :- p a of
Sub d -> d
instance Functor LimC where
fmap f = dimap (Sub limDict) (Sub Dict) (runAny f) where
runAny :: (p ~> q) -> p Any ~> q Any
runAny = runNat
class (hom ~ Hom) => Composed (hom :: k -> k -> *) | k -> hom where
type Compose :: (j -> k) -> (i -> j) -> i -> k
compose :: f (g a) `hom` Compose f g a
decompose :: Compose f g a `hom` f (g a)
infixr 9 ยท
type (ยท) = Compose
class f (g a) => ComposeC f g a
instance f (g a) => ComposeC f g a
instance Class (f (g a)) (ComposeC f g a) where cls = Sub Dict
instance f (g a) :=> ComposeC f g a where ins = Sub Dict
instance Composed (:-) where
type Compose = ComposeC
compose = Sub Dict
decompose = Sub Dict
class LimC (f ยท p) => Post f p
instance LimC (f ยท p) => Post f p
fmap1 :: forall p a b c. Post Functor p => (a ~> b) -> p c a ~> p c b
fmap1 f = case limDict :: Dict (Compose Functor p c) of Dict -> fmap f
fmap2 :: forall p a b c d. Post (Post Functor) p => (a ~> b) -> p c d a ~> p c d b
fmap2 f = case limDict :: Dict (Compose (Post Functor) p c) of
Dict -> case limDict :: Dict (Compose Functor (p c) d) of
Dict -> fmap f
contramap1 :: forall p a b c. Post Contravariant p => (a ~> b) -> p c b ~> p c a
contramap1 f = case limDict :: Dict (Compose Contravariant p c) of Dict -> contramap f
class (Functor p, Post Functor p) => Bifunctor p
instance (Functor p, Post Functor p) => Bifunctor p
bimap :: (Bifunctor p, Category (Cod2 p)) => (a ~> b) -> (c ~> d) -> p a c ~> p b d
bimap f g = first f . fmap1 g
class (Contravariant p, Post Functor p) => Profunctor p
instance (Contravariant p, Post Functor p) => Profunctor p
dimap :: (Profunctor p, Category (Cod2 p)) => (a ~> b) -> (c ~> d) -> p b c ~> p a d
dimap f g = lmap f . fmap1 g
type Iso s t a b = forall p. Profunctor p => p a b -> p s t
type Iso' s a = Iso s s a a
infixr 0 -|
class (Functor f, Functor u) => f -| u | f -> u, u -> f where
adj :: Iso (f a ~> b) (f a' ~> b') (a ~> u b) (a' ~> u b')
unitAdj :: (f -| u, Category (Dom u)) => a ~> u (f a)
unitAdj = get adj id
counitAdj :: (f -| u, Category (Dom f)) => f (u b) ~> b
counitAdj = beget adj id
zipR :: (f -| u, Cartesian (Dom u), Cartesian (Cod u))
=> Iso (u a * u b) (u a' * u b') (u (a * b)) (u (a' * b'))
zipR = dimap (get adj (beget adj fst &&& beget adj snd))
(fmap fst &&& fmap snd)
absurdL :: (f -| u, Initial z) => Iso z z (f z) (f z)
absurdL = dimap initial (beget adj initial)
cozipL :: (f -| u, Cocartesian (Cod u), Cocartesian (Cod f))
=> Iso (f (a + b)) (f (a' + b')) (f a + f b) (f a' + f b')
cozipL = dimap
(beget adj (get adj inl ||| get adj inr))
(fmap inl ||| fmap inr)
instance Category ((~>) :: j -> j -> *) => Functor (Nat f :: (i -> j) -> *) where
fmap = (.)
instance Functor ((:-) f) where
fmap = fmap1
class Const ~ k => Constant (k :: j -> i -> j) | j i -> k where
type Const :: j -> i -> j
_Const :: Iso (k b a) (k b' a') b b'
newtype Const1 b a = Const { getConst :: b }
instance Constant Const1 where
type Const = Const1
_Const = dimap getConst Const
instance Functor Const1 where
fmap f = Nat (_Const f)
instance Functor (Const1 b) where
fmap _ = _Const id
instance Contravariant (Const1 b) where
contramap _ = _Const id
instance (Semigroup b, Precartesian ((~>) :: i -> i -> *)) => Semimonoidal (Const1 b :: i -> *) where
ap2 = beget _Const . mult . bimap (get _Const) (get _Const)
instance (Monoid b, Cartesian ((~>) :: i -> i -> *)) => Monoidal (Const1 b :: i -> *) where
ap0 = beget _Const . one
instance Semigroup b => Semigroup (Const1 b a) where
mult = beget _Const . mult . bimap (get _Const) (get _Const)
instance Monoid b => Monoid (Const1 b a) where
one = beget _Const . one
instance (Cosemigroup b, Precocartesian ((~>) :: i -> i -> *)) => Cosemimonoidal (Const1 b :: i -> *) where
op2 = bimap (beget _Const) (beget _Const) . comult . get _Const
instance (Comonoid b, Cocartesian ((~>) :: i -> i -> *)) => Comonoidal (Const1 b :: i -> *) where
op0 = zero . get _Const
instance Cosemigroup b => Cosemigroup (Const1 b a) where
comult = bimap (beget _Const) (beget _Const) . comult . get _Const
instance Comonoid b => Comonoid (Const1 b a) where
zero = zero . get _Const
newtype Const2 (f :: j -> *) (a :: i) (c :: j) = Const2 { getConst2 :: f c }
instance Constant Const2 where
type Const = Const2
_Const = dimap (Nat getConst2) (Nat Const2)
instance Functor Const2 where
fmap f = Nat (_Const f)
instance Functor (Const2 f) where
fmap _ = Nat $ Const2 . getConst2
instance Functor f => Functor (Const2 f a) where
fmap f = Const2 . fmap f . getConst2
instance (Semigroup b, Precartesian ((~>) :: i -> i -> *)) => Semimonoidal (Const2 b :: i -> j -> *) where
ap2 = beget _Const . mult . bimap (get _Const) (get _Const)
instance (Monoid b, Cartesian ((~>) :: i -> i -> *)) => Monoidal (Const2 b :: i -> j -> *) where
ap0 = beget _Const . one
instance Semigroup b => Semigroup (Const2 b a) where
mult = beget _Const . mult . bimap (get _Const) (get _Const)
instance Monoid b => Monoid (Const2 b a) where
one = beget _Const . one
instance (Cosemigroup b, Precocartesian ((~>) :: i -> i -> *)) => Cosemimonoidal (Const2 b :: i -> j -> *) where
op2 = bimap (beget _Const) (beget _Const) . comult . get _Const
instance (Comonoid b, Cocartesian ((~>) :: i -> i -> *)) => Comonoidal (Const2 b :: i -> j -> *) where
op0 = zero . get _Const
instance Cosemigroup b => Cosemigroup (Const2 b a) where
comult = bimap (beget _Const) (beget _Const) . comult . get _Const
instance Comonoid b => Comonoid (Const2 b a) where
zero = zero . get _Const
class b => ConstC b a
instance b => ConstC b a
instance Constant ConstC where
type Const = ConstC
_Const = dimap (Sub Dict) (Sub Dict)
instance Functor ConstC where
fmap f = Nat (_Const f)
instance Functor (ConstC b) where
fmap _ = Sub Dict
instance (Semigroup b, Precartesian ((~>) :: i -> i -> *)) => Semimonoidal (ConstC b :: i -> Constraint) where
ap2 = beget _Const . mult . bimap (get _Const) (get _Const)
instance (Monoid b, Cartesian ((~>) :: i -> i -> *)) => Monoidal (ConstC b :: i -> Constraint) where
ap0 = beget _Const . one
instance Monoid b => Monoid (ConstC b a) where
one = beget _Const . one
instance (Cosemigroup b, Precocartesian ((~>) :: i -> i -> *)) => Cosemimonoidal (ConstC b :: i -> Constraint) where
op2 = bimap (beget _Const) (beget _Const) . comult . get _Const
instance (Comonoid b, Cocartesian ((~>) :: i -> i -> *)) => Comonoidal (ConstC b :: i -> Constraint) where
op0 = zero . get _Const
instance Cosemigroup b => Cosemigroup (ConstC b a) where
comult = bimap (beget _Const) (beget _Const) . comult . get _Const
instance Comonoid b => Comonoid (ConstC b a) where
zero = zero . get _Const
class f c => ConstC2 f a c
instance f c => ConstC2 f a c
instance Class (f c) (ConstC2 f a c) where cls = Sub Dict
instance f c :=> ConstC2 f a c where ins = Sub Dict
instance Constant ConstC2 where
type Const = ConstC2
_Const = dimap (Nat (Sub Dict)) (Nat (Sub Dict))
instance Functor ConstC2 where
fmap f = Nat (_Const f)
instance Functor (ConstC2 f) where
fmap _ = Nat $ ins . cls
instance Functor f => Functor (ConstC2 f a) where
fmap f = ins . fmap f . cls
instance (Semigroup b, Precartesian ((~>) :: i -> i -> *)) => Semimonoidal (ConstC2 b :: i -> j -> Constraint) where
ap2 = beget _Const . mult . bimap (get _Const) (get _Const)
instance (Monoid b, Cartesian ((~>) :: i -> i -> *)) => Monoidal (ConstC2 b :: i -> j -> Constraint) where
ap0 = beget _Const . one
instance Semigroup b => Semigroup (ConstC2 b a) where
mult = beget _Const . mult . bimap (get _Const) (get _Const)
instance Monoid b => Monoid (ConstC2 b a) where
one = beget _Const . one
instance (Cosemigroup b, Precocartesian ((~>) :: i -> i -> *)) => Cosemimonoidal (ConstC2 b :: i -> j -> Constraint) where
op2 = bimap (beget _Const) (beget _Const) . comult . get _Const
instance (Comonoid b, Cocartesian ((~>) :: i -> i -> *)) => Comonoidal (ConstC2 b :: i -> j -> Constraint) where
op0 = zero . get _Const
instance Cosemigroup b => Cosemigroup (ConstC2 b a) where
comult = bimap (beget _Const) (beget _Const) . comult . get _Const
instance Comonoid b => Comonoid (ConstC2 b a) where
zero = zero . get _Const
newtype Lim1 (f :: i -> *) = Lim { getLim :: forall x. f x }
instance Functor Lim1 where
fmap (Nat f) (Lim g) = Lim (f g)
instance Semimonoidal Lim1 where
ap2 (Lim f, Lim g) = Lim (Lift (f, g))
instance Monoidal Lim1 where
ap0 () = Lim $ Const ()
instance Semigroup m => Semigroup (Lim1 m) where
mult = multM
instance Monoid m => Monoid (Lim1 m) where
one = oneM
instance Const1 -| Lim1 where
adj = dimap (\f a -> Lim (runNat f (Const a))) $ \h -> Nat $ getLim . h . getConst
newtype Lim2 (f :: i -> j -> *) (y :: j) = Lim2 { getLim2 :: forall x. f x y }
newtype Lim3 (f :: i -> j -> k -> *) (y :: j) (z :: k) = Lim3 { getLim3 :: forall x. f x y z }
instance Functor Lim2 where
fmap f = Nat $ \(Lim2 g) -> Lim2 (runNat (runNat f) g)
instance Const2 -| Lim2 where
adj = dimap (\(Nat f) -> Nat $ \ a -> Lim2 (runNat f (Const2 a))) $ \(Nat h) -> nat2 $ getLim2 . h . getConst2
instance Semimonoidal LimC where
ap2 = get zipR
instance Monoidal LimC where
ap0 = Sub Dict
instance Monoid m => Monoid (LimC m) where
one = oneM
instance ConstC -| LimC where
adj = dimap (hither . runNat) (\b -> Nat $ dimap (Sub Dict) (Sub limDict) b) where
hither :: (ConstC a Any :- f Any) -> a :- LimC f
hither = dimap (Sub Dict) (Sub Dict)
class hom ~ Hom => Complete (hom :: j -> j -> *) | j -> hom where
type Lim :: (i -> j) -> j
elim :: hom (Lim g) (g a)
complete :: Dict (Const -| (Lim :: (i -> j) -> j))
default complete :: (Const -| (Lim :: (i -> j) -> j)) => Dict (Const -| (Lim :: (i-> j) -> j))
complete = Dict
instance Complete (->) where
type Lim = Lim1
elim = getLim
complete = Dict
instance Complete (Nat :: (i -> *) -> (i -> *) -> *) where
type Lim = Lim2
elim = Nat getLim2
complete = Dict
instance Complete ((:-) :: Constraint -> Constraint -> *) where
type Lim = LimC
elim = Sub limDict
complete = Dict
instance Functor Tagged where
fmap _ = Nat (_Tagged id)
instance Functor (Tagged e) where
fmap = Prelude.fmap
_Tagged :: Iso (Tagged s a) (Tagged t b) a b
_Tagged = dimap unTagged Tagged
instance Functor Proxy where
fmap _ Proxy = Proxy
instance Contravariant Proxy where
contramap _ Proxy = Proxy
instance Functor Dict where
fmap p Dict = Dict \\ p
class hom ~ Hom => Lifted (hom :: l -> l -> *) where
type Lift :: (j -> k -> l) -> (i -> j) -> (i -> k) -> (i -> l)
_Lift :: forall (q :: j -> k -> l) (r :: j -> k -> l) (f :: i -> j) (h :: i -> j) (g :: i -> k) (e :: i -> k) (a :: i) (b :: i).
Iso (Lift q f g a) (Lift r h e b) (q (f a) (g a)) (r (h b) (e b))
newtype Lift1 p f g a = Lift { lower :: p (f a) (g a) }
instance Lifted (->) where
type Lift = Lift1
_Lift = dimap lower Lift
instance Functor Lift1 where
fmap f = nat3 $ _Lift $ runNat2 f
instance Functor p => Functor (Lift1 p) where
fmap f = nat2 $ _Lift $ first $ runNat f
instance Contravariant p => Contravariant (Lift1 p) where
contramap f = nat2 $ _Lift $ lmap $ runNat f
instance Post Contravariant p => Contravariant (Lift1 p f) where
contramap (Nat f) = Nat $ _Lift (contramap1 f)
instance Post Functor p => Functor (Lift1 p f) where
fmap (Nat f) = Nat (_Lift $ fmap1 f)
instance (Functor p, Post Functor p, Functor f, Functor g) => Functor (Lift1 p f g) where
fmap f = _Lift (bimap (fmap f) (fmap f))
class r (p a) (q a) => LiftC r p q a
instance r (p a) (q a) => LiftC r p q a
instance Functor p => Functor (LiftC p) where
fmap f = nat2 $ _Lift $ first $ runNat f
instance Contravariant p => Contravariant (LiftC p) where
contramap f = nat2 $ _Lift $ lmap $ runNat f
instance Post Functor p => Functor (LiftC p e) where
fmap (Nat f) = Nat (_Lift $ fmap1 f)
instance Post Contravariant p => Contravariant (LiftC p e) where
contramap (Nat f) = Nat (_Lift $ contramap1 f)
instance Lifted (:-) where
type Lift = LiftC
_Lift = dimap (Sub Dict) (Sub Dict)
class r (f a) (g a) b => LiftC2 r f g a b
instance r (f a) (g a) b => LiftC2 r f g a b
instance Functor LiftC2 where
fmap f = nat3 $ _Lift $ runNat2 f
instance Functor p => Functor (LiftC2 p) where
fmap f = nat2 $ _Lift $ first $ runNat f
instance Contravariant p => Contravariant (LiftC2 p) where
contramap f = nat2 $ _Lift $ lmap $ runNat f
instance Post Functor p => Functor (LiftC2 p f) where
fmap (Nat f) = Nat (_Lift $ fmap1 f)
instance Post Contravariant p => Contravariant (LiftC2 p f) where
contramap = contramap1
instance Lifted (Nat :: (i -> Constraint) -> (i -> Constraint) -> *) where
type Lift = LiftC2
_Lift = dimap (Nat (Sub Dict)) (Nat (Sub Dict))
newtype Lift2 p f g a b = Lift2 { lower2 :: p (f a) (g a) b }
instance Lifted (Nat :: (i -> *) -> (i -> *) -> *) where
type Lift = Lift2
_Lift = dimap (Nat lower2) (Nat Lift2)
instance Functor Lift2 where
fmap f = nat3 $ _Lift $ runNat2 f
instance Functor p => Functor (Lift2 p) where
fmap f = nat2 $ _Lift $ first $ runNat f
instance Contravariant p => Contravariant (Lift2 p) where
contramap f = nat2 $ _Lift $ lmap $ runNat f
instance Post Functor p => Functor (Lift2 p f) where
fmap (Nat f) = Nat (_Lift $ fmap1 f)
instance Post Contravariant p => Contravariant (Lift2 p f) where
contramap = contramap1
instance Functor (,) where
fmap f = Nat (Arrow.first f)
instance Functor ((,) a) where
fmap = Arrow.second
infixr 2 &
class (p, q) => p & q
instance (p, q) => p & q
instance Functor (&) where
fmap f = Nat $ Sub $ Dict \\ f
instance Functor ((&) p) where
fmap p = Sub $ Dict \\ p
instance Functor Either where
fmap f = Nat (Arrow.left f)
instance Functor ((->) e) where
fmap = (.)
instance Contravariant (:-) where
contramap f = Nat $ dimap Self runSelf (lmap f)
instance Functor (Either e) where
fmap = Arrow.right
data Via (a :: x) (b :: x) (s :: x) (t :: x) where
Via :: (s ~> a) -> (b ~> t) -> Via a b s t
instance Post Functor ((~>) :: x -> x -> *) => Functor (Via :: x -> x -> x -> x -> *) where
fmap f = nat3 $ \(Via sa bt) -> Via (fmap1 f sa) bt
instance Post Contravariant ((~>) :: x -> x -> *) => Contravariant (Via :: x -> x -> x -> x -> *) where
contramap f = nat3 $ \(Via sa bt) -> Via (contramap1 f sa) bt
instance Functor ((~>) :: x -> x -> *) => Functor (Via a :: x -> x -> x -> *) where
fmap f = nat2 $ \(Via sa bt) -> Via sa (first f bt)
instance Contravariant ((~>) :: x -> x -> *) => Contravariant (Via a :: x -> x -> x -> *) where
contramap f = nat2 $ \(Via sa bt) -> Via sa (lmap f bt)
instance Functor ((~>) :: x -> x -> *) => Functor (Via a b :: x -> x -> *) where
fmap f = Nat $ \(Via sa bt) -> Via (first f sa) bt
instance Contravariant ((~>) :: x -> x -> *) => Contravariant (Via a b :: x -> x -> *) where
contramap f = Nat $ \(Via sa bt) -> Via (lmap f sa) bt
instance Post Functor ((~>) :: x -> x -> *) => Functor (Via a b s :: x -> *) where
fmap f (Via sa bt) = Via sa (fmap1 f bt)
instance Post Contravariant ((~>) :: x -> x -> *) => Contravariant (Via a b s :: x -> *) where
contramap f (Via sa bt) = Via sa (contramap1 f bt)
via :: forall (a :: *) (b :: *) (r :: *) (p :: x -> x -> *) (c :: x) (t :: *) (u :: *).
Category p => (Via a b a b -> Via r (p c c) u t) -> (t -> u) -> r
via l m = case l (Via id id) of
Via csa dbt -> csa $ m (dbt id)
mapping :: (Functor f, Functor f', Category (Dom f)) => (Via a b a b -> Via a b s t) -> Iso (f s) (f' t) (f a) (f' b)
mapping l = case l (Via id id) of
Via csa dbt -> dimap (fmap csa) (fmap dbt)
mapping1 :: (Post Functor f, Post Functor f', Category (Dom1 f)) => (Via a b a b -> Via a b s t) -> Iso (f i s) (f' j t) (f i a) (f' j b)
mapping1 l = case l (Via id id) of
Via csa dbt -> dimap (fmap1 csa) (fmap1 dbt)
firstly :: (Functor f, Functor f', Category (Dom f)) => (Via a b a b -> Via a b s t) -> Iso (f s x) (f' t y) (f a x) (f' b y)
firstly l = case l (Via id id) of
Via csa dbt -> dimap (first csa) (first dbt)
lmapping :: (Contravariant f, Contravariant f', Category (Dom f)) => (Via s t s t -> Via s t a b) -> Iso (f s x) (f' t y) (f a x) (f' b y)
lmapping l = case l (Via id id) of
Via csa dbt -> dimap (lmap csa) (lmap dbt)
swapping :: (Profunctor f, Profunctor f', Category (Dom f), Category (Cod2 f), Category (Cod2 f'))
=> (Via a b a b -> Via a b s t) -> Iso (f a s) (f' b t) (f s a) (f' t b)
swapping l = case l (Via id id) of
Via csa dbt -> dimap (dimap csa csa) (dimap dbt dbt)
post :: Category (Arr i) => (Via a b a b -> Via a b s t) -> Iso (i ~> s) (j ~> t) (i ~> a) (j ~> b)
post l = case l (Via id id) of
Via csa dbt -> dimap (csa .) (dbt .)
pre :: Category (Arr i) => (Via a b a b -> Via a b s t) -> Iso (a ~> i) (b ~> j) (s ~> i) (t ~> j)
pre l = case l (Via id id) of
Via csa dbt -> dimap (. csa) (. dbt)
newtype Self a b = Self { runSelf :: a ~> b }
_Self = dimap runSelf Self
instance Category ((~>) :: x -> x -> *) => Contravariant (Self :: x -> x -> *) where
contramap f = Nat (_Self (.f))
instance Category (Arr a) => Functor (Self a) where
fmap g (Self h) = Self (g . h)
instance Precartesian (Arr a) => Semimonoidal (Self a :: x -> *) where
ap2 (ea, eb) = Self (runSelf ea &&& runSelf eb)
instance Cartesian (Arr a) => Monoidal (Self a :: x -> *) where
ap0 () = Self terminal
instance (Precartesian (Arr a), Semigroup b) => Semigroup (Self a b) where
mult = multM
instance (Cartesian (Arr a), Monoid b) => Monoid (Self a b) where
one = oneM
instance Contravariant (->) where
contramap f = Nat (. f)
instance Contravariant ((~>)::j->j-> *) => Contravariant (Nat::(i->j)->(i->j)-> *) where
contramap (Nat f) = Nat $ \g -> Nat $ lmap f $ runNat g
instance Contravariant Tagged where
contramap _ = Nat (_Tagged id)
instance Contravariant (Const2 k) where
contramap _ = _Const id
newtype Get r a b = Get { runGet :: a ~> r }
_Get = dimap runGet Get
instance Category ((~>) :: i -> i -> *) => Functor (Get :: i -> i -> k -> *) where
fmap f = nat2 $ _Get (f .)
instance Category (Arr r) => Contravariant (Get r) where
contramap f = Nat (_Get (. f))
instance Contravariant (Get r a) where
contramap _ = _Get id
instance Functor (Get r a) where
fmap _ = _Get id
get :: (Category c, c ~ (~>)) => (Get a a a -> Get a s s) -> c s a
get l = runGet $ l (Get id)
newtype Beget r a b = Beget { runBeget :: r ~> b }
_Beget = dimap runBeget Beget
instance Category ((~>) :: i -> i -> *) => Contravariant (Beget :: i -> k -> i -> *) where
contramap f = nat2 $ _Beget (. f)
instance Functor (Beget r) where
fmap _ = Nat $ _Beget id
instance Contravariant (Beget r) where
contramap _ = Nat $ _Beget id
instance Category ((~>) :: i -> i -> *) => Functor (Beget (r :: i) (a :: k)) where
fmap f = _Beget (f .)
beget :: (Category c, c ~ (~>)) => (Beget b b b -> Beget b t t) -> c b t
beget l = runBeget $ l (Beget id)
(#) :: (Beget b b b -> Beget b t t) -> b -> t
(#) = beget
newtype Un (p::i->i->j) (a::i) (b::i) (s::i) (t::i) = Un { runUn :: p t s ~> p b a }
_Un = dimap runUn Un
instance (Category ((~>)::j->j-> *), Post Functor p) => Contravariant (Un (p::i->i->j) a b) where
contramap f = Nat $ _Un $ dimap Self runSelf $ lmap (fmap1 f)
instance (Category ((~>)::j->j-> *), Post Contravariant p) => Functor (Un (p::i->i->j) a b) where
fmap f = Nat $ _Un $ dimap Self runSelf $ lmap (contramap1 f)
instance (Category ((~>)::j->j-> *), Contravariant p) => Functor (Un (p::i->i->j) a b s) where
fmap g = _Un $ dimap Self runSelf $ lmap (lmap g)
instance (Category ((~>)::j->j-> *), Functor p) => Contravariant (Un (p::i->i->j) a b s) where
contramap f = _Un $ dimap Self runSelf $ lmap (first f)
un :: (Un p a b a b -> Un p a b s t) -> p t s -> p b a
un l = runUn $ l (Un id)
class (Contravariant p, Functor p) => Phantom p
instance (Contravariant p, Functor p) => Phantom p
class (Functor p, Profunctor (Cod2 p), Category (Cod2 p)) => Semitensor (p :: x -> x -> x) where
type Tensorable (p :: x -> x -> x) :: x -> Constraint
type Tensorable p = Const (() :: Constraint)
second :: (Tensorable p c) => (a ~> b) -> p c a ~> p c b
associate :: (Tensorable p a, Tensorable p b, Tensorable p c, Tensorable p a', Tensorable p b', Tensorable p c')
=> Iso (p (p a b) c) (p (p a' b') c') (p a (p b c)) (p a' (p b' c'))
second1 :: forall p a b c x. (Semitensor p, Post (Tensorable p) c) => (a ~> b) -> p (c x) a ~> p (c x) b
second1 = case limDict :: Dict (Compose (Tensorable p) c x) of
Dict -> second
associate1 :: forall a b c a' b' c' p x. (Semitensor p, Post (Tensorable p) a, Post (Tensorable p) b, Post (Tensorable p) c,
Post (Tensorable p) a', Post (Tensorable p) b', Post (Tensorable p) c')
=> Iso (p (p (a x) (b x)) (c x)) (p (p (a' x) (b' x)) (c' x)) (p (a x) (p (b x) (c x))) (p (a' x) (p (b' x) (c' x)))
associate1 = case limDict :: Dict (Compose (Tensorable p) a x) of
Dict -> case limDict :: Dict (Compose (Tensorable p) b x) of
Dict -> case limDict :: Dict (Compose (Tensorable p) c x) of
Dict -> case limDict :: Dict (Compose (Tensorable p) a' x) of
Dict -> case limDict :: Dict (Compose (Tensorable p) b' x) of
Dict -> case limDict :: Dict (Compose (Tensorable p) c' x) of
Dict -> associate
instance Semitensor (,) where
second = fmap1
associate = dimap (\((a,b),c) -> (a,(b,c)))
(\(a,(b,c)) -> ((a,b),c))
instance Semitensor Either where
second = fmap1
associate = dimap hither yon where
hither (Left (Left a)) = Left a
hither (Left (Right b)) = Right (Left b)
hither (Right c) = Right (Right c)
yon (Left a) = Left (Left a)
yon (Right (Left b)) = Left (Right b)
yon (Right (Right c)) = Right c
instance Semitensor (&) where
second = fmap1
associate = dimap (Sub Dict) (Sub Dict)
type family I (p :: x -> x -> x) :: x
class Semitensor p => Tensor p where
lambda :: (Tensorable p a, Tensorable p a') => Iso (p (I p) a) (p (I p) a') a a'
rho :: (Tensorable p a, Tensorable p a') => Iso (p a (I p)) (p a' (I p)) a a'
lambda1 :: forall a a' p x. (Tensor p, Post (Tensorable p) a, Post (Tensorable p) a') => Iso (p (I p) (a x)) (p (I p) (a' x)) (a x) (a' x)
lambda1 = case limDict :: Dict (Compose (Tensorable p) a x) of
Dict -> case limDict :: Dict (Compose (Tensorable p) a' x) of
Dict -> lambda
rho1 :: forall a a' p x. (Tensor p, Post (Tensorable p) a, Post (Tensorable p) a') => Iso (p (a x) (I p)) (p (a' x) (I p)) (a x) (a' x)
rho1 = case limDict :: Dict (Compose (Tensorable p) a x) of
Dict -> case limDict :: Dict (Compose (Tensorable p) a' x) of
Dict -> rho
type instance I (,) = ()
instance Tensor (,) where
lambda = dimap (\((), a) -> a) ((,) ())
rho = dimap (\(a, ()) -> a) (\a -> (a, ()))
type instance I Either = Void
instance Tensor Either where
lambda = dimap (\(Right a) -> a) Right
rho = dimap (\(Left a) -> a) Left
type instance I (&) = (() :: Constraint)
instance Tensor (&) where
lambda = dimap (Sub Dict) (Sub Dict)
rho = dimap (Sub Dict) (Sub Dict)
instance Semitensor p => Semitensor (Lift1 p) where
type Tensorable (Lift1 p) = Post (Tensorable p)
second f = Nat $ _Lift $ second1 $ runNat f
associate = dimap
(Nat $ _Lift $ second1 Lift . get associate1 . first (get _Lift))
(Nat $ _Lift $ first Lift . beget associate1 . second1 (get _Lift))
type instance I (Lift1 p) = Const1 (I p)
instance Tensor p => Tensor (Lift1 p) where
lambda = dimap (Nat $ lmap (first (get _Const) . get _Lift) (get lambda1))
(Nat $ fmap1 (beget _Lift . first (beget _Const)) (beget lambda1))
rho = dimap (Nat $ lmap (second1 (get _Const) . get _Lift) (get rho1))
(Nat $ fmap1 (beget _Lift . second1 (beget _Const)) (beget rho1))
instance Semitensor p => Semitensor (Lift2 (p :: (i -> *) -> (i -> *) -> i -> *)) where
type Tensorable (Lift2 p) = Post (Tensorable p)
second f = Nat $ _Lift $ second1 $ runNat f
associate = dimap
(Nat $ _Lift $ second1 (beget _Lift) . get associate1 . first (get _Lift))
(Nat $ _Lift $ first (beget _Lift) . beget associate1 . second1 (get _Lift))
type instance I (Lift2 p) = Const2 (I p)
instance Tensor p => Tensor (Lift2 p) where
lambda = dimap
(Nat $ lmap (first (get _Const) . get _Lift) (get lambda1))
(Nat $ fmap1 (beget _Lift . first (beget _Const)) (beget lambda1))
rho = dimap (Nat $ lmap (second1 (get _Const) . get _Lift) (get rho1))
(Nat $ fmap1 (beget _Lift . second1 (beget _Const)) (beget rho1))
instance Semitensor p => Semitensor (LiftC p) where
type Tensorable (LiftC p) = Post (Tensorable p)
second f = Nat $ _Lift $ second1 $ runNat f
associate = dimap
(Nat $ _Lift $ second1 (beget _Lift) . get associate1 . first (get _Lift))
(Nat $ _Lift $ first (beget _Lift) . beget associate1 . second1 (get _Lift))
type instance I (LiftC p) = ConstC (I p)
instance Tensor p => Tensor (LiftC p) where
lambda = dimap
(Nat $ lmap (first (get _Const) . get _Lift) (get lambda1))
(Nat $ fmap1 (beget _Lift . first (beget _Const)) (beget lambda1))
rho = dimap (Nat $ lmap (second1 (get _Const) . get _Lift) (get rho1))
(Nat $ fmap1 (beget _Lift . second1 (beget _Const)) (beget rho1))
instance Semitensor p => Semitensor (LiftC2 p) where
type Tensorable (LiftC2 p) = Post (Tensorable p)
second f = Nat $ _Lift $ second1 $ runNat f
associate = dimap
(Nat $ _Lift $ second1 (beget _Lift) . get associate1 . first (get _Lift))
(Nat $ _Lift $ first (beget _Lift) . beget associate1 . second1 (get _Lift))
type instance I (LiftC2 p) = ConstC2 (I p)
instance Tensor p => Tensor (LiftC2 p) where
lambda = dimap
(Nat $ lmap (first (get _Const) . get _Lift) (get lambda1))
(Nat $ fmap1 (beget _Lift . first (beget _Const)) (beget lambda1))
rho = dimap (Nat $ lmap (second1 (get _Const) . get _Lift) (get rho1))
(Nat $ fmap1 (beget _Lift . second1 (beget _Const)) (beget rho1))
class (Profunctor (Internal k), Category k, k ~ Hom) => Closed (k :: i -> i -> *) where
iota :: Iso (Internal k (I (Internal k)) a) (Internal k (I (Internal k)) b) a b
default iota :: (CCC k, Curryable (*) b, Tensorable (*) b, Tensorable (*) (Internal k (I (*)) a))
=> Iso (Internal k (I (Internal k)) a) (Internal k (I (Internal k)) b) a b
iota = dimap (apply . beget rho) (curry (get rho))
jot :: I (Internal k) ~> Internal k a a
default jot :: (CCC k, Tensorable (*) a) => I (Internal k) ~> Internal k a a
jot = curry (get lambda)
type instance I (->) = ()
type instance I (|-) = (() :: Constraint)
instance Closed (->)
instance Closed (:-)
instance Closed (Nat :: (i -> *) -> (i -> *) -> *)
instance Closed (Nat :: (i -> Constraint) -> (i -> Constraint) -> *)
class Bifunctor p => Symmetric p where
swap :: p a b ~> p b a
instance Symmetric (,) where
swap (a,b) = (b, a)
instance Symmetric (&) where
swap = Sub Dict
instance Symmetric Either where
swap = either Right Left
instance Symmetric p => Symmetric (Lift1 p) where
swap = Nat $ _Lift swap
instance Symmetric p => Symmetric (Lift2 p) where
swap = Nat $ _Lift swap
instance Symmetric p => Symmetric (LiftC p) where
swap = Nat $ _Lift swap
instance Symmetric p => Symmetric (LiftC2 p) where
swap = Nat $ _Lift swap
class One ~ t => Terminal (t :: i) | i -> t where
type One :: i
terminal :: a ~> t
instance Terminal () where
type One = ()
terminal _ = ()
instance Terminal t => Terminal (Const1 t) where
type One = Const1 One
terminal = Nat (beget _Const . terminal)
instance Terminal t => Terminal (Const2 t) where
type One = Const2 One
terminal = Nat (beget _Const . terminal)
instance Terminal (() :: Constraint) where
type One = (() :: Constraint)
terminal = Constraint.top
instance Terminal (ConstC ()) where
type One = ConstC ()
terminal = Nat (beget _Const . terminal)
instance Terminal t => Terminal (ConstC2 t) where
type One = ConstC2 One
terminal = Nat (beget _Const . terminal)
class Zero ~ t => Initial (t :: i) | i -> t where
type Zero :: i
initial :: t ~> a
instance Initial Void where
type Zero = Void
initial = absurd
instance Initial i => Initial (Const1 i) where
type Zero = Const1 Zero
initial = Nat $ initial . get _Const
instance Initial i => Initial (Const2 i) where
type Zero = Const2 Zero
initial = Nat $ initial . get _Const
instance Initial (() ~ Bool) where
type Zero = () ~ Bool
initial = Constraint.bottom
instance Initial i => Initial (ConstC i) where
type Zero = ConstC Zero
initial = Nat $ initial . get _Const
infixl 7 *
type family Copower :: i -> j -> j
type (*) = (Copower :: i -> i -> i)
class (h ~ (~>), Symmetric ((*)::i->i->i), Semitensor ((*)::i->i->i)) => Precartesian (h :: i -> i -> *) | i -> h where
fst :: forall (a::i) (b::i). a * b ~> a
snd :: forall (a::i) (b::i). a * b ~> b
(&&&) :: forall (a::i) (b::i) (c::i). (a ~> b) -> (a ~> c) -> a ~> b * c
class (h ~ (~>), Tensor ((*)::i->i->i), Terminal (I ((*)::i->i->i)), Precartesian h) => Cartesian (h ::i->i-> *) | i -> h
instance (h ~ (~>), Tensor ((*)::i->i->i), Terminal (I ((*)::i->i->i)), Precartesian h) => Cartesian (h ::i->i-> *)
type instance Copower = (,)
instance Precartesian (->) where
fst = Prelude.fst
snd = Prelude.snd
(&&&) = (Arrow.&&&)
type instance Copower = (&)
instance Precartesian (:-) where
fst = Sub Dict
snd = Sub Dict
p &&& q = Sub $ Dict \\ p \\ q
type instance Copower = Lift (,)
instance Precartesian (Nat :: (i -> *) -> (i -> *) -> *) where
fst = Nat $ fst . get _Lift
snd = Nat $ snd . get _Lift
Nat f &&& Nat g = Nat $ Lift . (f &&& g)
type instance Copower = Lift2 (*)
instance Precartesian (Nat :: (i -> j -> *) -> (i -> j -> *) -> *) where
fst = Nat $ fst . get _Lift
snd = Nat $ snd . get _Lift
Nat f &&& Nat g = Nat $ beget _Lift . (f &&& g)
type instance Copower = LiftC (&)
instance Precartesian (Nat :: (i -> Constraint) -> (i -> Constraint) -> *) where
fst = Nat $ fst . get _Lift
snd = Nat $ snd . get _Lift
Nat f &&& Nat g = Nat $ beget _Lift . (f &&& g)
type instance Copower = LiftC2 (*)
instance Precartesian (Nat :: (i -> j -> Constraint) -> (i -> j -> Constraint) -> *) where
fst = Nat $ fst . get _Lift
snd = Nat $ snd . get _Lift
Nat f &&& Nat g = Nat $ beget _Lift . (f &&& g)
infixl 6 +
class (h ~ (~>), Symmetric ((+)::i->i->i), Semitensor ((+)::i->i->i)) => Precocartesian (h :: i -> i -> *) | i -> h where
type (+) :: i -> i -> i
inl :: forall (a :: i) (b :: i). a ~> a + b
inr :: forall (a :: i) (b :: i). b ~> a + b
(|||) :: forall (a :: i) (b :: i) (c :: i). (a ~> c) -> (b ~> c) -> a + b ~> c
class (h ~ (~>), Tensor ((+)::i->i->i), Initial (I ((+)::i->i->i)), Precocartesian h) => Cocartesian (h ::i->i-> *) | i -> h
instance (h ~ (~>), Tensor ((+)::i->i->i), Initial (I ((+)::i->i->i)), Precocartesian h) => Cocartesian (h ::i->i-> *)
instance Precocartesian (->) where
type (+) = Either
inl = Left
inr = Right
(|||) = either
instance Precocartesian (Nat :: (i -> *) -> (i -> *) -> *) where
type (+) = Lift1 (+)
inl = Nat (beget _Lift . inl)
inr = Nat (beget _Lift . inr)
Nat f ||| Nat g = Nat $ (f ||| g) . get _Lift
instance Precocartesian (Nat :: (i -> j -> *) -> (i -> j -> *) -> *) where
type (+) = Lift2 (+)
inl = Nat (beget _Lift . inl)
inr = Nat (beget _Lift . inr)
Nat f ||| Nat g = Nat $ (f ||| g) . get _Lift
class (((a |- r) & (b |- r)) |- r) => CoproductCHelper a b r
instance (((a |- r) & (b |- r)) |- r) => CoproductCHelper a b r
instance Class (((a |- r) & (b |- r)) |- r) (CoproductCHelper a b r) where cls = Sub Dict
instance (((a |- r) & (b |- r)) |- r) :=> CoproductCHelper a b r where ins = Sub Dict
class LimC (CoproductCHelper a b) => CoproductC a b
instance LimC (CoproductCHelper a b) => CoproductC a b
instance Class (LimC (CoproductCHelper a b)) (CoproductC a b) where cls = Sub Dict
instance LimC (CoproductCHelper a b) :=> CoproductC a b where ins = Sub Dict
instance Functor CoproductC where
fmap f = Nat $ (inl . f) ||| inr
instance Functor (CoproductC a) where
fmap f = inl ||| (inr . f)
instance Symmetric CoproductC where
swap = inr ||| inl
instance Semitensor CoproductC where
second = fmap
associate = dimap ((inl ||| (inr . inl)) ||| (inr . inr)) ((inl . inl) ||| ((inl . inr) ||| inr))
instance Precocartesian (:-) where
type (+) = CoproductC
inl = inlC
where
inlC :: forall a b. a :- CoproductC a b
inlC = Sub $ Dict \\ ((ins . l) :: a :- CoproductCHelper a b Any)
l :: forall a b r. a :- (((a |- r) & (b |- r)) |- r)
l = Sub $ get _Implies $ Sub $ Dict \\ (implies :: a :- r)
inr = inrC
where
inrC :: forall a b. b :- CoproductC a b
inrC = Sub $ Dict \\ ((ins . r) :: b :- CoproductCHelper a b Any)
r :: forall a b r. b :- (((a |- r) & (b |- r)) |- r)
r = Sub $ get _Implies $ Sub $ Dict \\ (implies :: b :- r)
(|||) = eitherC
where
eitherC :: forall a b c. (a :- c) -> (b :- c) -> (CoproductC a b :- c)
eitherC = undefined
factor :: (Post Functor (f :: j -> i -> i), Precocartesian (Cod2 f)) => f e b + f e c ~> f e (b + c)
factor = fmap1 inl ||| fmap1 inr
class (Cartesian k, Cocartesian k) => Distributive (k :: i -> i -> *) | i -> k where
distribute :: forall (a :: i) (b :: i) (c :: i) (a' :: i) (b' :: i) (c' :: i).
Iso ((a * b) + (a * c)) ((a' * b') + (a' * c'))
(a * (b + c)) (a' * (b' + c'))
instance Distributive (->) where
distribute = dimap factor $ \case
(a, Left b) -> Left (a, b)
(a, Right c) -> Right (a, c)
instance Distributive (Nat :: (i -> *) -> (i -> *) -> *) where
distribute = dimap factor $ Nat $ \case
Lift (a, Lift (Left b)) -> Lift (Left (Lift (a, b)))
Lift (a, Lift (Right b)) -> Lift (Right (Lift (a, b)))
instance Distributive (Nat :: (i -> j -> *) -> (i -> j -> *) -> *) where
distribute = dimap factor $ Nat $ Nat $ \case
Lift2 (Lift (a, Lift2 (Lift (Left b)))) -> Lift2 (Lift (Left (Lift2 (Lift (a, b)))))
Lift2 (Lift (a, Lift2 (Lift (Right b)))) -> Lift2 (Lift (Right (Lift2 (Lift (a, b)))))
class Curried (p :: k -> i -> j) (e :: i -> j -> k) | p -> e, e -> p where
type Curryable (p :: k -> i -> j) :: k -> Constraint
type Curryable p = Const (() :: Constraint)
curry :: Curryable p a => (p a b ~> c) -> a ~> e b c
default curry :: (Post Functor e, Category (Cod2 e), Category (Cod2 p), Curryable p a) => (p a b ~> c) -> a ~> e b c
curry q = fmap1 q . unapply
uncurry :: (a ~> e b c) -> p a b ~> c
default uncurry :: (Functor p, Category (Cod2 e), Category (Cod2 p)) => (a ~> e b c) -> p a b ~> c
uncurry p = apply . first p
apply :: p (e a b) a ~> b
default apply :: Category (Cod2 e) => p (e a b) a ~> b
apply = uncurry id
unapply :: Curryable p a => a ~> e b (p a b)
default unapply :: (Category (Cod2 p), Curryable p a) => a ~> e b (p a b)
unapply = curry id
curried :: (Curried p e, Curryable p a) => Iso (p a b ~> c) (p a' b' ~> c') (a ~> e b c) (a' ~> e b' c')
curried = dimap curry uncurry
ccc :: (Category (Cod2 p), Symmetric p, Curried p e, Curryable p a) => Iso (p i a ~> b) (p i' a' ~> b') (a ~> e i b) (a' ~> e i' b')
ccc = dimap (. swap) (. swap) . curried
curry1 :: forall a b c p q x. (Curried p q, Post (Curryable p) a) => (p (a x) (b x) ~> c x) -> a x ~> q (b x) (c x)
curry1 = case limDict :: Dict (Compose (Curryable p) a x) of Dict -> curry
instance Curried p q => Curried (Lift1 p) (Lift1 q) where
type Curryable (Lift1 p) = Post (Curryable p)
curry f = Nat $ beget _Lift . curry1 (runNat f . beget _Lift)
uncurry g = Nat $ uncurry (get _Lift . runNat g) . get _Lift
instance Curried p q => Curried (Lift2 p) (Lift2 q) where
type Curryable (Lift2 p) = Post (Curryable p)
curry f = Nat $ beget _Lift . curry1 (runNat f . beget _Lift)
uncurry g = Nat $ uncurry (get _Lift . runNat g) . get _Lift
instance Curried p q => Curried (LiftC p) (LiftC q) where
type Curryable (LiftC p) = Post (Curryable p)
curry f = Nat $ beget _Lift . curry1 (runNat f . beget _Lift)
uncurry g = Nat $ uncurry (get _Lift . runNat g) . get _Lift
instance Curried p q => Curried (LiftC2 p) (LiftC2 q) where
type Curryable (LiftC2 p) = Post (Curryable p)
curry f = Nat $ beget _Lift . curry1 (runNat f . beget _Lift)
uncurry g = Nat $ uncurry (get _Lift . runNat g) . get _Lift
class Cocurried (f :: i -> j -> k) (u :: k -> i -> j) | f -> u , u -> f where
type Cocurryable (u :: k -> i -> j) :: k -> Constraint
type Cocurryable p = Const (() :: Constraint)
cocurry :: (f a b ~> c) -> b ~> u c a
uncocurry :: Cocurryable u c => (b ~> u c a) -> f a b ~> c
cocurried :: (Cocurried f u, Cocurryable u c') => Iso (f a b ~> c) (f a' b' ~> c') (b ~> u c a) (b' ~> u c' a')
cocurried = dimap cocurry uncocurry
class
( Cartesian k
, Closed k
, Curried (*) (Internal k)
, I (Internal k) ~ I (*)
, Curryable (*) (I (Internal k))
) => CCC (k :: x -> x -> *) | x -> k
instance
( Cartesian k
, Closed k
, Curried (*) (Internal k)
, I (Internal k) ~ I (*)
, Curryable (*) (I (Internal k))
) => CCC (k :: x -> x -> *)
instance Curried (,) (->) where
curry = Prelude.curry
uncurry = Prelude.uncurry
instance (,) e -| (->) e where
adj = ccc
class (Precartesian ((~>) :: x -> x -> *), Precartesian ((~>) :: y -> y -> *), Functor f) => Semimonoidal (f :: x -> y) where
ap2 :: f a * f b ~> f (a * b)
class (Cartesian ((~>) :: x -> x -> *), Cartesian ((~>) :: y -> y -> *), Semimonoidal f) => Monoidal (f :: x -> y) where
ap0 :: One ~> f One
instance Semimonoidal Dict where
ap2 (Dict, Dict) = Dict
instance Monoidal Dict where
ap0 () = Dict
instance Semigroup (Dict m) where
mult (Dict, Dict) = Dict
instance Monoid m => Monoid (Dict m) where
one = oneM
ap2Applicative :: Base.Applicative f => f a * f b -> f (a * b)
ap2Applicative = uncurry $ Base.liftA2 (,)
instance Semimonoidal ((:-) f) where
ap2 = uncurry (&&&)
instance Monoidal ((:-) f) where
ap0 () = terminal
instance Semigroup (f :- m) where
mult = multM
instance Monoid m => Monoid (f :- m) where
one = oneM
instance Semimonoidal ((|-) f) where
ap2 = get zipR
instance Monoidal ((|-) f) where
ap0 = curry fst
instance Monoid m => Monoid (f |- m) where
one = oneM
instance Semimonoidal (Nat f :: (i -> *) -> *) where
ap2 = uncurry (&&&)
instance Monoidal (Nat f :: (i -> *) -> *) where
ap0 () = terminal
instance Semimonoidal (Nat f :: (i -> Constraint) -> *) where
ap2 = uncurry (&&&)
instance Monoidal (Nat f :: (i -> Constraint) -> *) where
ap0 () = terminal
instance (Semimonoidal (Nat f), Semigroup m) => Semigroup (Nat f m) where
mult = multM
instance (Monoidal (Nat f), Monoid m) => Monoid (Nat f m) where
one = oneM
instance Semimonoidal (Tagged s) where
ap2 = Tagged . bimap unTagged unTagged
instance Monoidal (Tagged s) where
ap0 = Tagged
instance Semigroup m => Semigroup (Tagged s m) where
mult = Tagged . mult . bimap unTagged unTagged
instance Monoid m => Monoid (Tagged s m) where
one = Tagged . one
instance Precartesian ((~>) :: i -> i -> *) => Semimonoidal (Proxy :: i -> *) where
ap2 (Proxy, Proxy) = Proxy
instance Cartesian ((~>) :: i -> i -> *) => Monoidal (Proxy :: i -> *) where
ap0 () = Proxy
class Semimonoidal (m :: x -> x) => Semimonad (m :: x -> x) where
join :: m (m a) ~> m a
join = bind id
bind :: Semimonad m => (a ~> m b) ~> m a ~> m b
bind f = join . fmap f
class (Monoidal m, Semimonad m) => Monad m
instance (Monoidal m, Semimonad m) => Monad m
class (Precocartesian ((~>) :: x -> x -> *), Precocartesian ((~>) :: y -> y -> *), Functor f) => Cosemimonoidal (f :: x -> y) where
op2 :: f (a + b) ~> f a + f b
class (Cocartesian ((~>) :: x -> x -> *), Cocartesian ((~>) :: y -> y -> *), Cosemimonoidal f) => Comonoidal (f :: x -> y) where
op0 :: f Zero ~> Zero
instance Cosemimonoidal ((,) e) where
op2 (e,ab) = bimap ((,) e) ((,) e) ab
instance Comonoidal ((,) e) where
op0 = snd
instance Cosemigroup m => Cosemigroup (e, m) where
comult = comultOp
instance Comonoid m => Comonoid (e, m) where
zero = zeroOp
instance Cosemimonoidal Id0 where
op2 = bimap Id Id . runId
instance Comonoidal Id0 where
op0 = runId
instance Cosemigroup m => Cosemigroup (Id0 m) where
comult = comultOp
instance Comonoid m => Comonoid (Id0 m) where
zero = zeroOp
instance Cosemimonoidal (Lift1 (,) e) where
op2 = Nat $ Lift . bimap Lift Lift . op2 . fmap lower . lower
instance Comonoidal (Lift1 (,) e) where
op0 = snd
instance Cosemigroup m => Cosemigroup (Lift1 (,) e m) where
comult = comultOp
instance Comonoid m => Comonoid (Lift1 (,) e m) where
zero = zeroOp
instance Cosemimonoidal (Tagged s) where
op2 = bimap Tagged Tagged . unTagged
instance Comonoidal (Tagged s) where
op0 = unTagged
instance Cosemigroup m => Cosemigroup (Tagged s m) where
comult = comultOp
instance Comonoid m => Comonoid (Tagged s m) where
zero = zeroOp
class (f -| f, Id ~ f) => Identity (f :: i -> i) | i -> f where
type Id :: i -> i
_Id :: Iso (f a) (f a') a a'
newtype Id0 a = Id { runId :: a }
instance Identity Id0 where
type Id = Id0
_Id = dimap runId Id
instance Functor Id0 where
fmap = _Id
instance Id0 -| Id0 where
adj = un (mapping _Id . lmapping _Id)
newtype Id1 (f :: i -> *) (a :: i) = Id1 { runId1 :: f a }
_Id1 = dimap runId1 Id1
instance Identity Id1 where
type Id = Id1
_Id = dimap (Nat runId1) (Nat Id1)
instance Functor f => Functor (Id1 f) where
fmap = _Id1 . fmap
instance Cosemimonad Id1 where
duplicate = Nat Id1
instance Comonad Id1 where
extract = Nat runId1
instance Semimonoidal Id1 where
ap2 = Nat $ \(Lift (Id1 x, Id1 y)) -> Id1 (Lift (x, y))
instance Monoidal Id1 where
ap0 = Nat Id1
instance Semigroup m => Semigroup (Id1 m) where
mult = multM
instance Monoid m => Monoid (Id1 m) where
one = oneM
instance Semimonad Id1 where
join = Nat runId1
instance Monad Id1
instance Cosemimonoidal Id1 where
op2 = Nat $ \(Id1 (Lift ea)) -> Lift (bimap Id1 Id1 ea)
instance Comonoidal Id1 where
op0 = Nat runId1
instance Cosemigroup m => Cosemigroup (Id1 m) where
comult = comultOp
instance Comonoid m => Comonoid (Id1 m) where
zero = zeroOp
instance Id1 -| Id1 where
adj = un (mapping _Id . lmapping _Id)
instance Contravariant f => Contravariant (Id1 f) where
contramap = _Id1 . contramap
instance Functor Id1 where
fmap = _Id
instance Semimonoidal f => Semimonoidal (Id1 f) where
ap2 = Id1 . ap2 . bimap runId1 runId1
instance Monoidal f => Monoidal (Id1 f) where
ap0 = Id1 . ap0
instance Cosemimonoidal f => Cosemimonoidal (Id1 f) where
op2 = bimap Id1 Id1 . op2 . runId1
instance Comonoidal f => Comonoidal (Id1 f) where
op0 = op0 . runId1
instance (Cosemimonoidal f, Cosemigroup m) => Cosemigroup (Id1 f m) where
comult = comultOp
instance (Comonoidal f, Comonoid m) => Comonoid (Id1 f m) where
zero = zeroOp
class c => IdC c
instance c => IdC c
instance Identity IdC where
type Id = IdC
_Id = dimap (Sub Dict) (Sub Dict)
instance Functor IdC where
fmap = _Id
instance IdC -| IdC where
adj = un (mapping _Id . lmapping _Id)
class Precartesian (Arr m) => Semigroup m where
mult :: m * m ~> m
class (Semigroup m, Cartesian (Arr m)) => Monoid m where
one :: One ~> m
oneM :: (Monoidal u, Monoid m) => One ~> u m
oneM = fmap one . ap0
multM :: (Semimonoidal u, Semigroup m) => u m * u m ~> u m
multM = fmap mult . ap2
instance Semigroup (Const1 ()) where
mult = get lambda
instance Monoid (Const1 ()) where
one = id
instance Semigroup (p :: Constraint) where
mult = Sub Dict
instance Monoid (() :: Constraint) where
one = id
mappend :: (Semigroup m, CCC (Arr m), Curryable (*) m) => m ~> m^m
mappend = curry mult
class Precocartesian (Arr m) => Cosemigroup m where
comult :: m ~> m + m
class (Cosemigroup m, Cocartesian (Arr m)) => Comonoid m where
zero :: m ~> Zero
zeroOp :: (Comonoidal f, Comonoid m) => f m ~> Zero
zeroOp = op0 . fmap zero
comultOp :: (Cosemimonoidal f, Cosemigroup m) => f m ~> f m + f m
comultOp = op2 . fmap comult
instance Cosemigroup Void where
comult = initial
instance Comonoid Void where
zero = id
instance Semigroup Void where
mult = fst
instance Cosemigroup (Const1 Void) where
comult = Nat $ absurd . getConst
instance Comonoid (Const1 Void) where
zero = id
instance Semigroup (Const1 Void) where
mult = fst
class Functor f => Strength f where
strength :: a * f b ~> f (a * b)
instance Functor f => Strength (f :: * -> *) where
strength (a,fb) = fmap ((,) a) fb
class Functor f => Costrength (f :: x -> x) where
costrength :: f (a + b) ~> a + f b
instance (Functor f, Base.Traversable f) => Costrength f where
costrength = Base.sequence
ap :: (Semimonoidal f, CCC (Dom f), CCC (Cod f), Curryable (*) (f (b ^ a))) => f (b ^ a) ~> f b ^ f a
ap = curry (fmap apply . ap2)
return :: (Monoidal f, Strength f, CCC (Dom f), Tensorable (*) a) => a ~> f a
return = fmap (get lambda . swap) . strength . fmap1 ap0 . beget rho
class (Functor f, Category (Dom f)) => Cosemimonad f where
duplicate :: f a ~> f (f a)
default duplicate :: Category (Dom f) => f a ~> f (f a)
duplicate = extend id
extend :: (f a ~> b) -> f a ~> f b
extend f = fmap f . duplicate
class Cosemimonad f => Comonad f where
extract :: f a ~> a
data Prod :: (i,j) -> (i,j) -> * where
Want :: Prod a a
Have :: (a ~> b) -> (c ~> d) -> Prod '(a,c) '(b,d)
instance (Category ((~>) :: i -> i -> *), Category ((~>) :: j -> j -> *)) => Category (Prod :: (i,j) -> (i,j) -> *) where
id = Want
Want . f = f
f . Want = f
Have f f' . Have g g' = Have (f . g) (f' . g')
instance (Functor ((~>) a :: i -> *), Functor ((~>) b :: j -> *), ab ~ '(a,b)) => Functor (Prod ab :: (i, j) -> *) where
fmap Want f = f
fmap f Want = f
fmap (Have f g) (Have f' g') = Have (fmap f f') (fmap g g')
instance (Contravariant ((~>) :: i -> i -> *), Contravariant ((~>) :: j -> j -> *)) => Contravariant (Prod :: (i, j) -> (i, j) -> *) where
contramap Want = id
contramap (Have f g) = Nat $ \case
Want -> Have f g
Have f' g' -> Have (lmap f f') (lmap g g')
runProd :: forall (a :: i) (b :: i) (c :: j) (d :: j).
(Category ((~>) :: i -> i -> *), Category ((~>) :: j -> j -> *))
=> Prod '(a,c) '(b,d) -> (a ~> b, c ~> d)
runProd Want = (id,id)
runProd (Have f g) = (f,g)
runFst
:: forall (a :: i) (b :: i) (c :: j) (d :: j).
Category ((~>) :: i -> i -> *)
=> Prod '(a,c) '(b,d) -> a ~> b
runFst Want = id
runFst (Have f _) = f
runSnd
:: forall (a :: i) (b :: i) (c :: j) (d :: j).
Category ((~>) :: j -> j -> *)
=> Prod '(a,c) '(b,d) -> c ~> d
runSnd Want = id
runSnd (Have _ g) = g
diagProdAdj :: forall (a :: i) (b :: i) (c :: i) (a' :: i) (b' :: i) (c' :: i).
Cartesian ((~>) :: i -> i -> *) =>
Iso ('(a,a) ~> '(b,c)) ('(a',a') ~> '(b',c')) (a ~> b * c) (a' ~> b' * c')
diagProdAdj = dimap (uncurry (&&&) . runProd) $ \f -> Have (fst . f) (snd . f)
sumDiagAdj :: forall (a :: i) (b :: i) (c :: i) (a' :: i) (b' :: i) (c' :: i).
Cocartesian ((~>) :: i -> i -> *) =>
Iso (b + c ~> a) (b' + c' ~> a') ('(b,c) ~> '(a,a)) ('(b',c') ~> '(a',a'))
sumDiagAdj = dimap (\f -> Have (f . inl) (f . inr)) (uncurry (|||) . runProd)
infixr 9 |-
class p |- q where
implies :: p :- q
_Sub :: Iso (p :- q) (p' :- q') (Dict p -> Dict q) (Dict p' -> Dict q')
_Sub = dimap (\pq Dict -> case pq of Sub q -> q) (\f -> Sub $ f Dict)
newtype Magic p q r = Magic ((p |- q) => r)
_Implies :: Iso (p :- q) (p' :- q') (Dict (p |- q)) (Dict (p' |- q'))
_Implies = dimap (reify Dict) (\Dict -> implies) where
reify :: forall p q r. ((p |- q) => r) -> (p :- q) -> r
reify k = unsafeCoerce (Magic k :: Magic p q r)
instance Contravariant (|-) where
contramap f = Nat $ beget _Sub $ un _Implies (. f)
instance Functor ((|-) p) where
fmap f = beget _Sub $ un _Implies (f .)
instance (&) p -| (|-) p where
adj = ccc
instance Curried (&) (|-) where
apply = applyConstraint where
applyConstraint :: forall p q. (p |- q & p) :- q
applyConstraint = Sub $ Dict \\ (implies :: p :- q)
unapply = unapplyConstraint where
unapplyConstraint :: p :- q |- (p & q)
unapplyConstraint = Sub $ get _Implies (Sub Dict)
data Unit (a :: ()) (b :: ()) = Unit
instance Category Unit where
id = Unit
Unit . Unit = Unit
instance Contravariant Unit where
contramap f = Nat (. f)
instance Functor (Unit a) where
fmap = (.)
instance Terminal '() where
type One = '()
terminal = Unit
instance Initial '() where
type Zero = '()
initial = Unit
instance Functor Unit where
fmap = contramap . swap
instance Contravariant (Unit a) where
contramap = fmap . swap
instance Symmetric Unit where
swap Unit = Unit
newtype Empty (a :: Void) (b :: Void) = Empty (Empty a b)
instance Category Empty where
id = Empty id
(.) (!f0) = spin f0 where
spin (Empty f) = spin f
instance Symmetric Empty where
swap (Empty f) = Empty (swap f)
instance Contravariant Empty where
contramap f = Nat (. f)
instance Functor Empty where
fmap = contramap . swap
instance Functor (Empty a) where
fmap = (.)
instance Contravariant (Empty a) where
contramap = fmap . swap
data No (a :: Void)
instance Functor No where
fmap !_ = Prelude.undefined
composed = dimap decompose compose
associateCompose = dimap (Nat (compose . fmap compose . decompose . decompose))
(Nat (compose . compose . fmap decompose . decompose))
whiskerComposeL k = Nat $ composed $ runNat k
whiskerComposeR k = Nat $ composed $ fmap (runNat k)
lambdaCompose = dimap (Nat (get _Id . decompose)) (Nat (compose . beget _Id))
rhoCompose = dimap (Nat (fmap (get _Id) . decompose)) (Nat (compose . fmap (beget _Id)))
newtype Compose1 f g a = Compose { getCompose :: f (g a) }
instance Composed (->) where
type Compose = Compose1
compose = Compose
decompose = getCompose
instance Semitensor Compose1 where
type Tensorable Compose1 = Functor
second f = Nat $ composed $ fmap (runNat f)
associate = dimap (Nat (compose . fmap compose . decompose . decompose))
(Nat (compose . compose . fmap decompose . decompose))
type instance I Compose1 = Id
instance Tensor Compose1 where
lambda = dimap (Nat (get _Id . decompose)) (Nat (compose . beget _Id))
rho = dimap (Nat (fmap (get _Id) . decompose)) (Nat (compose . fmap (beget _Id)))
newtype Compose2 f g a b = Compose2 { getCompose2 :: f (g a) b }
instance Semitensor Compose2 where
type Tensorable Compose2 = Functor
second f = Nat $ composed $ fmap (runNat f)
associate = dimap (Nat (compose . fmap compose . decompose . decompose))
(Nat (compose . compose . fmap decompose . decompose))
type instance I Compose2 = Id
instance Tensor Compose2 where
lambda = dimap (Nat (get _Id . decompose)) (Nat (compose . beget _Id))
rho = dimap (Nat (fmap (get _Id) . decompose)) (Nat (compose . fmap (beget _Id)))
instance Semitensor ComposeC where
type Tensorable ComposeC = Functor
second f = Nat $ composed $ fmap (runNat f)
associate = dimap (Nat (compose . fmap compose . decompose . decompose))
(Nat (compose . compose . fmap decompose . decompose))
type instance I ComposeC = Id
instance Tensor ComposeC where
lambda = dimap (Nat (get _Id . decompose)) (Nat (compose . beget _Id))
rho = dimap (Nat (fmap (get _Id) . decompose)) (Nat (compose . fmap (beget _Id)))
instance Composed (Nat :: (k -> *) -> (k -> *) -> *) where
type Compose = Compose2
compose = Nat Compose2
decompose = Nat getCompose2
instance Functor Compose1 where
fmap f = nat2 $ composed $ runNat f
instance Functor Compose2 where
fmap f = nat2 $ composed $ runNat f
instance Functor ComposeC where
fmap f = nat2 $ composed $ runNat f
instance Functor f => Functor (Compose1 f) where
fmap f = Nat $ composed $ fmap $ runNat f
instance Functor f => Functor (Compose2 f) where
fmap f = Nat $ composed $ fmap $ runNat f
instance Functor f => Functor (ComposeC f) where
fmap f = Nat $ composed $ fmap $ runNat f
instance Contravariant f => Contravariant (Compose1 f) where
contramap f = Nat $ composed $ contramap $ runNat f
instance Contravariant f => Contravariant (Compose2 f) where
contramap f = Nat $ composed $ contramap $ runNat f
instance Contravariant f => Contravariant (ComposeC f) where
contramap f = Nat $ composed $ contramap $ runNat f
instance (Functor f, Functor g) => Functor (Compose1 f g) where
fmap = composed . fmap . fmap
instance (Functor f, Functor g) => Functor (Compose2 f g) where
fmap = composed . fmap . fmap
instance (Functor f, Functor g) => Functor (ComposeC f g) where
fmap = composed . fmap . fmap
instance (Semimonoidal f, Semimonoidal g) => Semimonoidal (Compose1 f g) where
ap2 = compose . fmap ap2 . ap2 . bimap decompose decompose
instance (Semimonoidal f, Semimonoidal g) => Semimonoidal (Compose2 f g) where
ap2 = compose . fmap ap2 . ap2 . bimap decompose decompose
instance (Semimonoidal f, Semimonoidal g) => Semimonoidal (ComposeC f g) where
ap2 = compose . fmap ap2 . ap2 . bimap decompose decompose
instance (Monoidal f, Monoidal g) => Monoidal (Compose1 f g) where
ap0 = compose . fmap ap0 . ap0
instance (Monoidal f, Monoidal g) => Monoidal (Compose2 f g) where
ap0 = compose . fmap ap0 . ap0
instance (Monoidal f, Monoidal g) => Monoidal (ComposeC f g) where
ap0 = compose . fmap ap0 . ap0
instance (Cosemimonoidal f, Cosemimonoidal g) => Cosemimonoidal (Compose1 f g) where
op2 = bimap compose compose . op2 . fmap op2 . decompose
instance (Cosemimonoidal f, Cosemimonoidal g) => Cosemimonoidal (Compose2 f g) where
op2 = bimap compose compose . op2 . fmap op2 . decompose
instance (Cosemimonoidal f, Cosemimonoidal g) => Cosemimonoidal (ComposeC f g) where
op2 = bimap compose compose . op2 . fmap op2 . decompose
instance (Comonoidal f, Comonoidal g) => Comonoidal (Compose1 f g) where
op0 = op0 . fmap op0 . decompose
instance (Comonoidal f, Comonoidal g) => Comonoidal (Compose2 f g) where
op0 = op0 . fmap op0 . decompose
instance (Comonoidal f, Comonoidal g) => Comonoidal (ComposeC f g) where
op0 = op0 . fmap op0 . decompose
instance (Semimonoidal f, Semimonoidal g, Semigroup m) => Semigroup (Compose1 f g m) where
mult = compose . fmap (fmap mult . ap2) . ap2 . bimap decompose decompose
instance (Semimonoidal f, Semimonoidal g, Semigroup m) => Semigroup (Compose2 f g m) where
mult = compose . fmap (fmap mult . ap2) . ap2 . bimap decompose decompose
instance (Monoidal f, Monoidal g, Monoid m) => Monoid (Compose1 f g m) where
one = compose . fmap (fmap one . ap0) . ap0
instance (Monoidal f, Monoidal g, Monoid m) => Monoid (Compose2 f g m) where
one = compose . fmap (fmap one . ap0) . ap0
instance (Monoidal f, Monoidal g, Monoid m) => Monoid (ComposeC f g m) where
one = compose . fmap (fmap one . ap0) . ap0
instance (Cosemimonoidal f, Cosemimonoidal g, Cosemigroup m) => Cosemigroup (Compose1 f g m) where
comult = bimap compose compose . op2 . fmap (op2 . fmap comult) . decompose
instance (Cosemimonoidal f, Cosemimonoidal g, Cosemigroup m) => Cosemigroup (Compose2 f g m) where
comult = bimap compose compose . op2 . fmap (op2 . fmap comult) . decompose
instance (Cosemimonoidal f, Cosemimonoidal g, Cosemigroup m) => Cosemigroup (ComposeC f g m) where
comult = bimap compose compose . op2 . fmap (op2 . fmap comult) . decompose
instance (Comonoidal f, Comonoidal g, Comonoid m) => Comonoid (Compose1 f g m) where
zero = op0 . fmap (op0 . fmap zero) . decompose
instance (Comonoidal f, Comonoidal g, Comonoid m) => Comonoid (Compose2 f g m) where
zero = op0 . fmap (op0 . fmap zero) . decompose
instance (Comonoidal f, Comonoidal g, Comonoid m) => Comonoid (ComposeC f g m) where
zero = op0 . fmap (op0 . fmap zero) . decompose
instance (f -| g, f' -| g', Category (Dom f), Category (Cod f)) => Compose1 f' f -| Compose1 g g' where
adj = dimap (fmap1 compose . get adj . get adj . lmap compose)
(lmap decompose . beget adj . beget adj . fmap1 decompose)
instance (f -| g, f' -| g', Category (Dom f), Category (Cod f)) => Compose1 f' f -| Compose2 g g' where
adj = dimap (fmap1 compose . get adj . get adj . lmap compose)
(lmap decompose . beget adj . beget adj . fmap1 decompose)
instance (f -| g, f' -| g', Category (Dom f), Category (Cod f)) => Compose1 f' f -| ComposeC g g' where
adj = dimap (fmap1 compose . get adj . get adj . lmap compose)
(lmap decompose . beget adj . beget adj . fmap1 decompose)
class (Profunctor p, p ~ (~>)) => Semicategory p
instance (Profunctor p, p ~ (~>)) => Semicategory p
data Copower1 x f a = Copower x (f a)
type instance Copower = Copower1
instance Functor Copower1 where
fmap f = nat2 $ \(Copower x fa) -> Copower (f x) fa
instance Functor (Copower1 x) where
fmap f = Nat $ \(Copower x fa) -> Copower x (runNat f fa)
instance Functor f => Functor (Copower1 x f) where
fmap f (Copower x fa) = Copower x (fmap f fa)
instance Contravariant f => Contravariant (Copower1 x f) where
contramap f (Copower x fa) = Copower x (contramap f fa)
instance Curried Copower1 Nat where
curry f a = Nat $ \e -> runNat f (Copower a e)
uncurry f = Nat $ \(Copower a e) -> runNat (f a) e
data Copower2 x f a b = Copower2 x (f a b)
type instance Copower = Copower2
instance Functor Copower2 where
fmap f = nat3 $ \(Copower2 x fab) -> Copower2 (f x) fab
instance Functor (Copower2 x) where
fmap f = nat2 $ \(Copower2 x fab) -> Copower2 x (runNat2 f fab)
instance Functor f => Functor (Copower2 x f) where
fmap f = Nat $ \(Copower2 x fab) -> Copower2 x (first f fab)
instance Post Functor f => Functor (Copower2 x f a) where
fmap f (Copower2 x fab) = Copower2 x (fmap1 f fab)
instance Contravariant f => Contravariant (Copower2 x f) where
contramap f = Nat $ \(Copower2 x fab) -> Copower2 x (lmap f fab)
instance Post Contravariant f => Contravariant (Copower2 x f a) where
contramap f (Copower2 x fab) = Copower2 x (contramap1 f fab)
instance Curried Copower2 Nat where
curry f a = nat2 $ \b -> runNat2 f (Copower2 a b)
uncurry f = nat2 $ \(Copower2 a b) -> runNat2 (f a) b
data Copower2_1 x f a b = Copower2_1 (x a) (f a b)
type instance Copower = Copower2_1
instance Functor Copower2_1 where
fmap f = nat3 $ \(Copower2_1 xa fab) -> Copower2_1 (runNat f xa) fab
instance Functor (Copower2_1 x) where
fmap f = nat2 $ \(Copower2_1 xa fab) -> Copower2_1 xa (runNat2 f fab)
instance (Functor x, Functor f) => Functor (Copower2_1 x f) where
fmap f = Nat $ \(Copower2_1 xa fab) -> Copower2_1 (fmap f xa) (first f fab)
instance (Contravariant x, Contravariant f) => Contravariant (Copower2_1 x f) where
contramap f = Nat $ \(Copower2_1 xa fab) -> Copower2_1 (contramap f xa) (lmap f fab)
instance Post Functor f => Functor (Copower2_1 x f a) where
fmap f (Copower2_1 xa fab) = Copower2_1 xa (fmap1 f fab)
instance Post Contravariant f => Contravariant (Copower2_1 x f a) where
contramap f (Copower2_1 xa fab) = Copower2_1 xa (contramap1 f fab)
instance Curried Copower2_1 (Lift1 Nat) where
curry f = Nat $ \a -> Lift $ Nat $ \b -> runNat2 f $ Copower2_1 a b
uncurry f = nat2 $ \(Copower2_1 a b) -> runNat (lower (runNat f a)) b
class (k ~ (~>)) => Cocomplete (k :: j -> j -> *) where
type Colim :: (i -> j) -> j
colim :: k (f a) (Colim f)
cocomplete :: Dict ((Colim :: (i -> j) -> j) -| Const)
default cocomplete :: ((Colim :: (i -> j) -> j) -| Const) => Dict ((Colim :: (i -> j) -> j) -| Const)
cocomplete = Dict
data Colim1 (f :: i -> *) where
Colim :: f x -> Colim1 f
instance Functor Colim1 where
fmap (Nat f) (Colim g)= Colim (f g)
instance Cosemimonoidal Colim1 where
op2 (Colim (Lift ab)) = bimap Colim Colim ab
instance Comonoidal Colim1 where
op0 (Colim (Const a)) = a
instance Cosemigroup m => Cosemigroup (Colim1 m) where
comult = comultOp
instance Comonoid m => Comonoid (Colim1 m) where
zero = zeroOp
instance Colim1 -| Const1 where
adj = dimap (\f -> Nat $ Const . f . Colim) $ \(Nat g2cb) (Colim g) -> getConst (g2cb g)
instance Cocomplete (->) where
type Colim = Colim1
colim = Colim
data Colim2 (f :: i -> j -> *) (x :: j) where
Colim2 :: f y x -> Colim2 f x
instance Functor Colim2 where
fmap f = Nat $ \(Colim2 g) -> Colim2 (runNat (runNat f) g)
instance Colim2 -| Const2 where
adj = dimap (\(Nat f) -> nat2 $ Const2 . f . Colim2) $
\ f -> Nat $ \ xs -> case xs of
Colim2 fyx -> getConst2 $ runNat2 f fyx
instance Cocomplete (Nat :: (i -> *) -> (i -> *) -> *) where
type Colim = Colim2
colim = Nat Colim2
class (c ~ Hom) => HasRan (c :: k -> k -> *) | k -> c where
type Ran :: (i -> j) -> (i -> k) -> j -> k
ranCurried :: Dict (Curried Compose (Ran :: (i -> j) -> (i -> k) -> j -> k))
default ranCurried :: Curried Compose (Ran :: (i -> j) -> (i -> k) -> j -> k) => Dict (Curried Compose (Ran :: (i -> j) -> (i -> k) -> j -> k))
ranCurried = Dict
ranProfunctor :: Category (Hom :: j -> j -> *) => Dict (Profunctor (Ran :: (i -> j) -> (i -> k) -> j -> k))
default ranProfunctor :: Profunctor (Ran :: (i -> j) -> (i -> k) -> j -> k) => Dict (Profunctor (Ran :: (i -> j) -> (i -> k) -> j -> k))
ranProfunctor = Dict
ranFunctor :: Dict (Functor (Ran f g :: j -> k))
default ranFunctor :: Functor (Ran f g :: j -> k) => Dict (Functor (Ran f g :: j -> k))
ranFunctor = Dict
iotaRan :: forall (f :: i -> k) (g :: i -> k) id. (Category (Cod f), Category (Dom f), Functor g, Identity id) => Iso (Ran id f) (Ran id g) f g
jotRan :: forall (f :: i -> k). Id ~> Ran f f
data Ran1 f g a = forall z. Functor z => Ran (Compose z f ~> g) (z a)
instance Curried Compose1 Ran1 where
type Curryable Compose1 = Functor
curry l = Nat (Ran l)
uncurry l = Nat $ \ (Compose ab) -> case runNat l ab of
Ran czfg za -> runNat czfg (Compose za)
instance HasRan (->) where
type Ran = Ran1
iotaRan = dimap (apply . beget rhoCompose) (curry (get rhoCompose))
jotRan = curry (get lambdaCompose)
instance Contravariant Ran1 where
contramap f = nat2 $ \(Ran k z) -> Ran (k . Nat (compose . fmap (runNat f) . decompose)) z
instance Category (Hom :: j -> j -> *) => Functor (Ran1 f :: (i -> *) -> (j -> *)) where
fmap f = Nat $ \(Ran k z) -> Ran (f . k) z
instance Functor (Ran1 f g) where
fmap f (Ran k z) = Ran k (fmap f z)
class (c ~ Hom) => HasLan (c :: k -> k -> *) | k -> c where
type Lan :: (i -> j) -> (i -> k) -> j -> k
lanCocurried :: Dict (Cocurried (Lan :: (i -> j) -> (i -> k) -> j -> k) Compose)
default lanCocurried :: Cocurried (Lan :: (i -> j) -> (i -> k) -> j -> k) Compose => Dict (Cocurried (Lan :: (i -> j) -> (i -> k) -> j -> k) Compose)
lanCocurried = Dict
lanProfunctor :: Category (Hom :: j -> j -> *) => Dict (Profunctor (Lan :: (i -> j) -> (i -> k) -> j -> k))
default lanProfunctor :: Profunctor (Lan :: (i -> j) -> (i -> k) -> j -> k) => Dict (Profunctor (Lan :: (i -> j) -> (i -> k) -> j -> k))
lanProfunctor = Dict
lanFunctor :: Dict (Functor (Lan f g :: j -> k))
default lanFunctor :: Functor (Lan f g :: j -> k) => Dict (Functor (Lan f g :: j -> k))
lanFunctor = Dict
epsilonLan :: forall (f :: i -> k) (g :: i -> k) id. (Category (Cod f), Category (Dom f), Functor f, Identity id) => Iso (Lan id f) (Lan id g) f g
newtype Lan1 f g a = Lan { runLan :: forall z. Functor z => (g ~> Compose z f) ~> z a }
instance Cocurried Lan1 Compose1 where
type Cocurryable Compose1 = Functor
cocurry l = Nat $ \b -> Compose $ runNat l (Lan $ \f -> case runNat f b of Compose z -> z)
uncocurry k = Nat $ \xs -> runLan xs k
instance HasLan (->) where
type Lan = Lan1
epsilonLan = dimap (Nat $ \l -> runLan l (beget rhoCompose))
(Nat $ \f -> Lan $ \k -> runNat (get rhoCompose . k) f)
instance Contravariant Lan1 where
contramap f = nat2 $ \l -> Lan $ \k -> runLan l (Nat (compose . fmap (runNat f) . decompose) . k)
instance Category (Hom :: j -> j -> *) => Functor (Lan1 f :: (i -> *) -> (j -> *)) where
fmap f = Nat $ \l -> Lan $ \k -> runLan l (k . f)
instance Functor (Lan1 f g) where
fmap f l = Lan $ fmap f . runLan l
newtype Lan2 f g a b = Lan2 { runLan2 :: forall z. Functor z => (g ~> Compose z f) ~> z a b }
instance Cocurried Lan2 Compose2 where
type Cocurryable Compose2 = Functor
cocurry l = nat2 $ \b -> Compose2 $ runNat2 l (Lan2 $ \f -> case runNat2 f b of Compose2 z -> z)
uncocurry k = nat2 $ \xs -> runLan2 xs k
instance HasLan (Nat :: (i -> *) -> (i -> *) -> *) where
type Lan = Lan2
epsilonLan = dimap (nat2 $ \l -> runLan2 l (beget rhoCompose))
(nat2 $ \f -> Lan2 $ \k -> runNat2 (get rhoCompose . k) f)
instance Contravariant Lan2 where
contramap f = nat3 $ \l -> Lan2 $ \k -> runLan2 l (Nat (compose . fmap (runNat f) . decompose) . k)
instance Category (Hom :: j -> j -> *) => Functor (Lan2 f :: (i -> k -> *) -> (j -> k -> *)) where
fmap f = nat2 $ \l -> Lan2 $ \k -> runLan2 l (k . f)
instance Functor (Lan2 f g) where
fmap f = Nat $ \l -> Lan2 $ first f . runLan2 l