Safe Haskell	None
Language	Haskell2010

Proarrow.Helper.CCC

Synopsis

toCCC :: forall {k} (a :: FK k) (b :: FK k). (BiCCC k, Ob a, Ob b) => ((TermF :: FK k) ~> (a --> b)) -> FromFree a ~> FromFree b
lam :: forall {k} (a :: k) (b :: k) (i :: k). (CCC k, Ob i, Ob a, Ob b) => ((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b) -> i ~> (a ~~> b)
($) :: forall {k} (i :: k) (a :: k) (b :: k). (CCC k, Ob b) => (i ~> (a ~~> b)) -> (i ~> a) -> i ~> b
lift :: forall {k} (i :: k) (a :: k) (b :: k). CCC k => (a ~> b) -> (i ~> a) -> i ~> b
pattern (:&) :: forall {k} (i :: k) (a :: k) (b :: k). (CCC k, Ob a, Ob b) => (i ~> a) -> (i ~> b) -> i ~> (a && b)
left :: forall {k} (a :: k) (b :: k) (i :: k). (HasBinaryCoproducts k, Ob a, Ob b) => (i ~> a) -> i ~> (a || b)
right :: forall {k} (a :: k) (b :: k) (i :: k). (HasBinaryCoproducts k, Ob a, Ob b) => (i ~> b) -> i ~> (a || b)
either :: forall {k} (a :: k) (b :: k) (c :: k) (i :: k). (HasBinaryCoproducts k, CCC k, Ob a, Ob b, Ob c) => (i ~> (a ~~> c)) -> (i ~> (b ~~> c)) -> i ~> ((a || b) ~~> c)
data FreeCCC (a :: FK k) (b :: FK k)
data family InitF :: k
data family TermF :: k
data family (a :: k) * (b :: k) :: k
data family (a :: k) + (b :: k) :: k
data FK k = F k

Documentation

toCCC :: forall {k} (a :: FK k) (b :: FK k). (BiCCC k, Ob a, Ob b) => ((TermF :: FK k) ~> (a --> b)) -> FromFree a ~> FromFree b Source Comments #

Adapted from Phil Freeman: https://blog.functorial.com/posts/2017-10-08-HOAS-CCCs.html

lam :: forall {k} (a :: k) (b :: k) (i :: k). (CCC k, Ob i, Ob a, Ob b) => ((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b) -> i ~> (a ~~> b) Source Comments #

($) :: forall {k} (i :: k) (a :: k) (b :: k). (CCC k, Ob b) => (i ~> (a ~~> b)) -> (i ~> a) -> i ~> b Source Comments #

lift :: forall {k} (i :: k) (a :: k) (b :: k). CCC k => (a ~> b) -> (i ~> a) -> i ~> b Source Comments #

pattern (:&) :: forall {k} (i :: k) (a :: k) (b :: k). (CCC k, Ob a, Ob b) => (i ~> a) -> (i ~> b) -> i ~> (a && b) Source Comments #

left :: forall {k} (a :: k) (b :: k) (i :: k). (HasBinaryCoproducts k, Ob a, Ob b) => (i ~> a) -> i ~> (a || b) Source Comments #

right :: forall {k} (a :: k) (b :: k) (i :: k). (HasBinaryCoproducts k, Ob a, Ob b) => (i ~> b) -> i ~> (a || b) Source Comments #

either :: forall {k} (a :: k) (b :: k) (c :: k) (i :: k). (HasBinaryCoproducts k, CCC k, Ob a, Ob b, Ob c) => (i ~> (a ~~> c)) -> (i ~> (b ~~> c)) -> i ~> ((a || b) ~~> c) Source Comments #

data FreeCCC (a :: FK k) (b :: FK k) Source Comments #

Instances

Instances details

BiCCC k => Promonad (FreeCCC :: FK k -> FK k -> Type) Source Comments #
Instance details Defined in Proarrow.Helper.CCC Methods id :: forall (a :: FK k). Ob a => FreeCCC a a Source Comments # (.) :: forall (b :: FK k) (c :: FK k) (a :: FK k). FreeCCC b c -> FreeCCC a b -> FreeCCC a c Source Comments #
BiCCC k => MonoidalProfunctor (FreeCCC :: FK k -> FK k -> Type) Source Comments #
Instance details Defined in Proarrow.Helper.CCC Methods par0 :: FreeCCC (Unit :: FK k) (Unit :: FK k) Source Comments # par :: forall (x1 :: FK k) (x2 :: FK k) (y1 :: FK k) (y2 :: FK k). FreeCCC x1 x2 -> FreeCCC y1 y2 -> FreeCCC (x1 y1) (x2 y2) Source Comments #
BiCCC k => Profunctor (FreeCCC :: FK k -> FK k -> Type) Source Comments #
Instance details Defined in Proarrow.Helper.CCC Methods dimap :: forall (c :: FK k) (a :: FK k) (b :: FK k) (d :: FK k). (c ~> a) -> (b ~> d) -> FreeCCC a b -> FreeCCC c d Source Comments # (\\) :: forall (a :: FK k) (b :: FK k) r. ((Ob a, Ob b) => r) -> FreeCCC a b -> r Source Comments #
Show (FreeCCC a b) Source Comments #
Instance details Defined in Proarrow.Helper.CCC Methods showsPrec :: Int -> FreeCCC a b -> ShowS Comments # show :: FreeCCC a b -> String Comments # showList :: [FreeCCC a b] -> ShowS Comments #

data family InitF :: k Source Comments #

data family TermF :: k Source Comments #

data family (a :: k) * (b :: k) :: k Source Comments #

data family (a :: k) + (b :: k) :: k Source Comments #

data FK k Source Comments #

Constructors

F k

Instances

Instances details

BiCCC k => Monoidal (FK k) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

Associated Types

type Unit
Instance details Defined in Proarrow.Helper.CCC type Unit = TerminalObject :: FK k

Methods

leftUnitor :: forall (a :: FK k). Ob a => ((Unit :: FK k) ** a) ~> a Source Comments #

leftUnitorInv :: forall (a :: FK k). Ob a => a ~> ((Unit :: FK k) ** a) Source Comments #

rightUnitor :: forall (a :: FK k). Ob a => (a ** (Unit :: FK k)) ~> a Source Comments #

rightUnitorInv :: forall (a :: FK k). Ob a => a ~> (a ** (Unit :: FK k)) Source Comments #

associator :: forall (a :: FK k) (b :: FK k) (c :: FK k). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Comments #

associatorInv :: forall (a :: FK k) (b :: FK k) (c :: FK k). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Comments #

BiCCC k => CategoryOf (FK k) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

Associated Types

type (~>)
Instance details Defined in Proarrow.Helper.CCC type (~>) = FreeCCC :: FK k -> FK k -> Type

BiCCC k => HasBinaryCoproducts (FK k) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

Methods

lft :: forall (a :: FK k) (b :: FK k). (Ob a, Ob b) => a ~> (a || b) Source Comments #

lft' :: forall (a :: FK k) (a' :: FK k) (b :: FK k). (a ~> a') -> Obj b -> a ~> (a' || b) Source Comments #

rgt :: forall (a :: FK k) (b :: FK k). (Ob a, Ob b) => b ~> (a || b) Source Comments #

rgt' :: forall (a :: FK k) (b :: FK k) (b' :: FK k). Obj a -> (b ~> b') -> b ~> (a || b') Source Comments #

(|||) :: forall (x :: FK k) (a :: FK k) (y :: FK k). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Comments #

(+++) :: forall (a :: FK k) (b :: FK k) (x :: FK k) (y :: FK k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Comments #

BiCCC k => HasBinaryProducts (FK k) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

Methods

fst :: forall (a :: FK k) (b :: FK k). (Ob a, Ob b) => (a && b) ~> a Source Comments #

fst' :: forall (a :: FK k) (a' :: FK k) (b :: FK k). (a ~> a') -> Obj b -> (a && b) ~> a' Source Comments #

snd :: forall (a :: FK k) (b :: FK k). (Ob a, Ob b) => (a && b) ~> b Source Comments #

snd' :: forall (a :: FK k) (b :: FK k) (b' :: FK k). Obj a -> (b ~> b') -> (a && b) ~> b' Source Comments #

(&&&) :: forall (a :: FK k) (x :: FK k) (y :: FK k). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments #

(***) :: forall (a :: FK k) (b :: FK k) (x :: FK k) (y :: FK k). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments #

BiCCC k => Closed (FK k) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

Methods

curry' :: forall (a :: FK k) (b :: FK k) (c :: FK k). Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c) Source Comments #

uncurry' :: forall (b :: FK k) (c :: FK k) (a :: FK k). Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c Source Comments #

(^^^) :: forall (b :: FK k) (y :: FK k) (x :: FK k) (a :: FK k). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Comments #

BiCCC k => HasInitialObject (FK k) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

Associated Types

type InitialObject
Instance details Defined in Proarrow.Helper.CCC type InitialObject = InitF :: FK k

Methods

initiate :: forall (a :: FK k). Ob a => (InitialObject :: FK k) ~> a Source Comments #

initiate' :: forall (a' :: FK k) (a :: FK k). (a' ~> a) -> (InitialObject :: FK k) ~> a Source Comments #

BiCCC k => HasTerminalObject (FK k) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Helper.CCC type TerminalObject = TermF :: FK k

Methods

terminate :: forall (a :: FK k). Ob a => a ~> (TerminalObject :: FK k) Source Comments #

terminate' :: forall (a :: FK k) (a' :: FK k). (a ~> a') -> a ~> (TerminalObject :: FK k) Source Comments #

BiCCC k => Promonad (FreeCCC :: FK k -> FK k -> Type) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

Methods

id :: forall (a :: FK k). Ob a => FreeCCC a a Source Comments #

(.) :: forall (b :: FK k) (c :: FK k) (a :: FK k). FreeCCC b c -> FreeCCC a b -> FreeCCC a c Source Comments #

BiCCC k => MonoidalProfunctor (FreeCCC :: FK k -> FK k -> Type) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

Methods

par0 :: FreeCCC (Unit :: FK k) (Unit :: FK k) Source Comments #

par :: forall (x1 :: FK k) (x2 :: FK k) (y1 :: FK k) (y2 :: FK k). FreeCCC x1 x2 -> FreeCCC y1 y2 -> FreeCCC (x1 ** y1) (x2 ** y2) Source Comments #

BiCCC k => Profunctor (FreeCCC :: FK k -> FK k -> Type) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

Methods

dimap :: forall (c :: FK k) (a :: FK k) (b :: FK k) (d :: FK k). (c ~> a) -> (b ~> d) -> FreeCCC a b -> FreeCCC c d Source Comments #

(\\) :: forall (a :: FK k) (b :: FK k) r. ((Ob a, Ob b) => r) -> FreeCCC a b -> r Source Comments #

type UN ('F :: j -> FK j) ('F a :: FK j) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

type UN ('F :: j -> FK j) ('F a :: FK j) = a

type Unit Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

type Unit = TerminalObject :: FK k

type (~>) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

type (~>) = FreeCCC :: FK k -> FK k -> Type

type InitialObject Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

type InitialObject = InitF :: FK k

type TerminalObject Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

type TerminalObject = TermF :: FK k

type Ob (a :: FK k) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

type Ob (a :: FK k)

type (a :: FK k) ** (b :: FK k) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

type (a :: FK k) ** (b :: FK k) = a && b

type (a :: FK k) || (b :: FK k) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

type (a :: FK k) || (b :: FK k) = a + b

type (a :: FK k) && (b :: FK k) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

type (a :: FK k) && (b :: FK k) = a * b

type (a :: FK k) ~~> (b :: FK k) Source Comments #

Instance details

Defined in Proarrow.Helper.CCC

type (a :: FK k) ~~> (b :: FK k)