proarrow-0: Category theory with a central role for profunctors
Safe HaskellNone
LanguageHaskell2010

Proarrow.Helper.CCC

Synopsis
  • toCCC :: forall {k} (a :: FK k) (b :: FK k). (BiCCC k, IsFK a, IsFK b) => Free ('[] :: [FK k]) (a --> b) -> FromFree a ~> FromFree b
  • lam :: forall {k} (a :: FK k) (b :: FK k) (i :: [FK k]). (IsFK a, IsFK b, IsFKs i) => ((forall (x :: [FK k]). Cast x (a ': i) => Free x a) -> Free (a ': i) b) -> Free i (a --> b)
  • ($) :: forall {k} (a :: FK k) (b :: FK k) (i :: [FK k]). (IsFK a, IsFK b, IsFKs i) => Free i (a --> b) -> Free i a -> Free i b
  • lift :: forall {k} (a :: k) (b :: k) (i :: [FK k]). (a ~> b) -> Free i ('F a) -> Free i ('F b)
  • pattern (:&) :: (IsFK a, IsFK b, IsFKs i) => Free i a -> Free i b -> Free i (a *! b)
  • data Free (a :: [FK k]) (b :: FK k) where
    • Lft :: forall {k} (a1 :: FK k) (b1 :: FK k) (a :: [FK k]). (IsFK a1, IsFK b1, IsFKs a) => Free a a1 -> Free a (a1 + b1)
    • Rgt :: forall {k} (a1 :: FK k) (b1 :: FK k) (a :: [FK k]). (IsFK a1, IsFK b1, IsFKs a) => Free a b1 -> Free a (a1 + b1)
  • either :: forall {k} (a :: FK k) (b :: FK k) (c :: FK k) (i :: [FK k]). (IsFK a, IsFK b, IsFK c, IsFKs i, Closed k) => Free i (a --> c) -> Free i (b --> c) -> Free i (a + b) -> Free i c
  • data family InitF :: k
  • data family TermF :: k
  • data family (a :: k) *! (b :: k) :: 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, IsFK a, IsFK b) => Free ('[] :: [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 :: FK k) (b :: FK k) (i :: [FK k]). (IsFK a, IsFK b, IsFKs i) => ((forall (x :: [FK k]). Cast x (a ': i) => Free x a) -> Free (a ': i) b) -> Free i (a --> b) Source Comments #

($) :: forall {k} (a :: FK k) (b :: FK k) (i :: [FK k]). (IsFK a, IsFK b, IsFKs i) => Free i (a --> b) -> Free i a -> Free i b infixr 0 Source Comments #

lift :: forall {k} (a :: k) (b :: k) (i :: [FK k]). (a ~> b) -> Free i ('F a) -> Free i ('F b) Source Comments #

pattern (:&) :: (IsFK a, IsFK b, IsFKs i) => Free i a -> Free i b -> Free i (a *! b) Source Comments #

data Free (a :: [FK k]) (b :: FK k) where Source Comments #

Constructors

Lft :: forall {k} (a1 :: FK k) (b1 :: FK k) (a :: [FK k]). (IsFK a1, IsFK b1, IsFKs a) => Free a a1 -> Free a (a1 + b1) 
Rgt :: forall {k} (a1 :: FK k) (b1 :: FK k) (a :: [FK k]). (IsFK a1, IsFK b1, IsFKs a) => Free a b1 -> Free a (a1 + b1) 

Instances

Instances details
Show (Free a b) Source Comments # 
Instance details

Defined in Proarrow.Helper.CCC

Methods

showsPrec :: Int -> Free a b -> ShowS Comments #

show :: Free a b -> String Comments #

showList :: [Free a b] -> ShowS Comments #

either :: forall {k} (a :: FK k) (b :: FK k) (c :: FK k) (i :: [FK k]). (IsFK a, IsFK b, IsFK c, IsFKs i, Closed k) => Free i (a --> c) -> Free i (b --> c) -> Free i (a + b) -> Free i c Source 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 family (a :: k) --> (b :: k) :: k infixr 2 Source Comments #

data FK k Source Comments #

Constructors

F k 

Instances

Instances details
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