Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Overloaded Categories, desugar Arrow
into classes in this module.
Enabled with
{-# OPTIONS -fplugin=Overloaded -fplugin-opt=Overloaded:Categories #-}
Description
Arrows
notation - GHC manual chapter -
is cool, but it desugars into "wrong" classes.
The arr
combinator is used for plumbing. We should desugar to proper
type-classes:
CartesianCategory
, notArrow
CocartesianCategory
, notArrowChoice
(implementation relies onBicartesianCategory
)CCC
, notArrowApply
(not implemented yet)
Examples
Expression like
catAssoc ::CartesianCategory
cat => cat (Product
cat (Product
cat a b) c) (Product
cat a (Product
cat b c)) catAssoc = proc ((x, y), z) ->identity
-< (x, (y, z))
are desugared to (a mess which is)
fanout
(proj1
%%
proj1
) (fanout
(proj2
%%
proj1
)proj2
)
If you are familiar with arrows-operators, this is similar to
(fst
.fst
)&&&
(snd
.fst
&&&
snd
)
expression.
The catAssoc
could be instantiated to cat = (->)
,
or more interestingly for example instantiate it to STLC morphisms to get an expression
like:
Lam (Pair (Fst (Fst (Var Here))) (Pair (Snd (Fst (Var Here))) (Snd (Var Here))))
proc
notation is nicer than writing de Bruijn indices.
This is very similar idea to Conal Elliott's Compiling to Categories work. This approach is syntactically more heavy, but works in more correct stage of compiler, before actual desugarer.
As one more example, we implement the automatic differentiation, as in Conal's paper(s). To keep things simple we use
newtype AD a b = AD (a -> (b, a -> b))
representation, i.e. use ordinary maps to represent linear maps. We then define a function
evaluateAD :: Functor f => AD a b -> a -> f a -> (b, f b) evaluateAD (AD f) x xs = let (y, f') = f x in (y, fmap f' xs)
which would allow to calculuate function value and derivatives in given directions. Then we can define simple quadratic function:
quad :: AD (Double, Double) Double quad = proc (x, y) -> do x2 <- mult -< (x, x) y2 <- mult -< (y, y) plus -< (x2, y2)
It's not as simple as writing quad x y = x * x + y * y
,
but not too far.
Then we can play with it. At origo everything is zero:
let sqrthf = 1 / sqrt 2 in evaluateAD quad (0, 0) [(1,0), (0,1), (sqrthf, sqrthf)] = (0.0,[0.0,0.0,0.0])
If we evaluate at some other point, we see things working:
evaluateAD quad (1, 2) [(1,0), (0,1), (sqrthf, sqrthf)] = (5.0,[2.0,4.0,4.242640687119285])
Obviously, if we would use inspectable representation for linear maps,
as Conal describe, we'd get more benefits. And then arr
wouldn't
be definable!
Synopsis
- class Category (cat :: k -> k -> Type)
- identity :: Category cat => cat a a
- (%%) :: Category cat => cat b c -> cat a b -> cat a c
- class Category cat => SemigroupalCategory (cat :: k -> k -> Type) where
- defaultAssoc :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat (Tensor cat a b) c) (Tensor cat a (Tensor cat b c))
- defaultUnassoc :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat a (Tensor cat b c)) (Tensor cat (Tensor cat a b) c)
- class SemigroupalCategory cat => MonoidalCategory (cat :: k -> k -> Type) where
- defaultLunit :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat (Unit cat) a) a
- defaultRunit :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat a (Unit cat)) a
- defaultUnrunit :: (CategoryWith1 cat, Tensor cat ~ Product cat, Unit cat ~ Terminal cat) => cat a (Tensor cat a (Unit cat))
- defaultUnlunit :: (CategoryWith1 cat, Tensor cat ~ Product cat, Unit cat ~ Terminal cat) => cat a (Tensor cat (Unit cat) a)
- class SemigroupalCategory cat => CommutativeCategory cat where
- defaultSwap :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat a b) (Tensor cat b a)
- class Category cat => CartesianCategory (cat :: k -> k -> Type) where
- class CartesianCategory cat => CategoryWith1 (cat :: k -> k -> Type) where
- class CocartesianCategory cat => CategoryWith0 (cat :: k -> k -> Type) where
- class Category cat => CocartesianCategory (cat :: k -> k -> Type) where
- class (CartesianCategory cat, CocartesianCategory cat) => BicartesianCategory cat where
- class CartesianCategory cat => CCC (cat :: k -> k -> Type) where
- type Exponential cat :: k -> k -> k
- eval :: cat (Product cat (Exponential cat a b) a) b
- transpose :: cat (Product cat a b) c -> cat a (Exponential cat b c)
- class Category cat => GeneralizedElement (cat :: k -> k -> Type) where
- newtype WrappedArrow arr a b = WrapArrow {
- unwrapArrow :: arr a b
Category
class Category (cat :: k -> k -> Type) #
A class for categories. Instances should satisfy the laws
Instances
Category (Coercion :: k -> k -> Type) | Since: base-4.7.0.0 |
Category ((:~:) :: k -> k -> Type) | Since: base-4.7.0.0 |
Category ((:~~:) :: k -> k -> Type) | Since: base-4.10.0.0 |
Category arr => Category (WrappedArrow arr :: k -> k -> Type) Source # | |
Defined in Overloaded.Categories id :: forall (a :: k0). WrappedArrow arr a a # (.) :: forall (b :: k0) (c :: k0) (a :: k0). WrappedArrow arr b c -> WrappedArrow arr a b -> WrappedArrow arr a c # | |
Category k2 => Category (Dual k2 :: k1 -> k1 -> Type) | |
Category p => Category (WrappedArrow p :: k -> k -> Type) | |
Defined in Data.Profunctor.Types id :: forall (a :: k0). WrappedArrow p a a # (.) :: forall (b :: k0) (c :: k0) (a :: k0). WrappedArrow p b c -> WrappedArrow p a b -> WrappedArrow p a c # | |
(Category p, Category q) => Category (Product p q :: k -> k -> Type) | |
(Applicative f, Category p) => Category (Tannen f p :: k -> k -> Type) | |
Category Op | |
Monad m => Category (Kleisli m :: Type -> Type -> Type) | Since: base-3.0 |
(Applicative f, Monad f) => Category (WhenMissing f :: Type -> Type -> Type) | Since: containers-0.5.9 |
Defined in Data.IntMap.Internal id :: forall (a :: k). WhenMissing f a a # (.) :: forall (b :: k) (c :: k) (a :: k). WhenMissing f b c -> WhenMissing f a b -> WhenMissing f a c # | |
Category ((->) :: Type -> Type -> Type) | Since: base-3.0 |
Defined in Control.Category | |
(Monad f, Applicative f) => Category (WhenMatched f x :: Type -> Type -> Type) | Since: containers-0.5.9 |
Defined in Data.IntMap.Internal id :: forall (a :: k). WhenMatched f x a a # (.) :: forall (b :: k) (c :: k) (a :: k). WhenMatched f x b c -> WhenMatched f x a b -> WhenMatched f x a c # | |
(Applicative f, Monad f) => Category (WhenMissing f k :: Type -> Type -> Type) | Since: containers-0.5.9 |
Defined in Data.Map.Internal id :: forall (a :: k0). WhenMissing f k a a # (.) :: forall (b :: k0) (c :: k0) (a :: k0). WhenMissing f k b c -> WhenMissing f k a b -> WhenMissing f k a c # | |
Monad f => Category (Star f :: Type -> Type -> Type) | |
(Monad f, Applicative f) => Category (WhenMatched f k x :: Type -> Type -> Type) | Since: containers-0.5.9 |
Defined in Data.Map.Internal id :: forall (a :: k0). WhenMatched f k x a a # (.) :: forall (b :: k0) (c :: k0) (a :: k0). WhenMatched f k x b c -> WhenMatched f k x a b -> WhenMatched f k x a c # |
Monoidial
class Category cat => SemigroupalCategory (cat :: k -> k -> Type) where Source #
defaultAssoc :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat (Tensor cat a b) c) (Tensor cat a (Tensor cat b c)) Source #
defaultUnassoc :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat a (Tensor cat b c)) (Tensor cat (Tensor cat a b) c) Source #
class SemigroupalCategory cat => MonoidalCategory (cat :: k -> k -> Type) where Source #
defaultLunit :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat (Unit cat) a) a Source #
defaultRunit :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat a (Unit cat)) a Source #
defaultUnrunit :: (CategoryWith1 cat, Tensor cat ~ Product cat, Unit cat ~ Terminal cat) => cat a (Tensor cat a (Unit cat)) Source #
defaultUnlunit :: (CategoryWith1 cat, Tensor cat ~ Product cat, Unit cat ~ Terminal cat) => cat a (Tensor cat (Unit cat) a) Source #
class SemigroupalCategory cat => CommutativeCategory cat where Source #
defaultSwap :: (CartesianCategory cat, Tensor cat ~ Product cat) => cat (Tensor cat a b) (Tensor cat b a) Source #
Product and Terminal
class Category cat => CartesianCategory (cat :: k -> k -> Type) where Source #
Cartesian category is a monoidal category where monoidal product is the categorical product.
proj1 :: cat (Product cat a b) a Source #
proj2 :: cat (Product cat a b) b Source #
fanout :: cat a b -> cat a c -> cat a (Product cat b c) Source #
is written as \(\langle f, g \rangle\) in category theory literature.fanout
f g
Instances
CocartesianCategory cat => CartesianCategory (Dual cat :: k -> k -> Type) Source # | |
Defined in Overloaded.Categories | |
CartesianCategory Op Source # | |
Monad m => CartesianCategory (Kleisli m :: Type -> Type -> Type) Source # | |
Defined in Overloaded.Categories | |
CartesianCategory ((->) :: Type -> Type -> Type) Source # | |
Defined in Overloaded.Categories | |
Monad m => CartesianCategory (Star m :: Type -> Type -> Type) Source # | |
Defined in Overloaded.Categories | |
Arrow arr => CartesianCategory (WrappedArrow arr :: Type -> Type -> Type) Source # | |
Defined in Overloaded.Categories type Product (WrappedArrow arr) :: k -> k -> k Source # proj1 :: forall (a :: k) (b :: k). WrappedArrow arr (Product (WrappedArrow arr) a b) a Source # proj2 :: forall (a :: k) (b :: k). WrappedArrow arr (Product (WrappedArrow arr) a b) b Source # fanout :: forall (a :: k) (b :: k) (c :: k). WrappedArrow arr a b -> WrappedArrow arr a c -> WrappedArrow arr a (Product (WrappedArrow arr) b c) Source # |
class CartesianCategory cat => CategoryWith1 (cat :: k -> k -> Type) where Source #
Category with terminal object.
Instances
CategoryWith0 cat => CategoryWith1 (Dual cat :: k -> k -> Type) Source # | |
CategoryWith1 Op Source # | |
Monad m => CategoryWith1 (Kleisli m :: Type -> Type -> Type) Source # | |
CategoryWith1 ((->) :: Type -> Type -> Type) Source # | |
Monad m => CategoryWith1 (Star m :: Type -> Type -> Type) Source # | |
Arrow arr => CategoryWith1 (WrappedArrow arr :: Type -> Type -> Type) Source # | |
Defined in Overloaded.Categories type Terminal (WrappedArrow arr) :: k Source # terminal :: forall (a :: k). WrappedArrow arr a (Terminal (WrappedArrow arr)) Source # |
Coproduct and initial
class CocartesianCategory cat => CategoryWith0 (cat :: k -> k -> Type) where Source #
Category with initial object.
Instances
CategoryWith1 cat => CategoryWith0 (Dual cat :: k -> k -> Type) Source # | |
CategoryWith0 Op Source # | |
Monad m => CategoryWith0 (Kleisli m :: Type -> Type -> Type) Source # | |
CategoryWith0 ((->) :: Type -> Type -> Type) Source # | |
Monad m => CategoryWith0 (Star m :: Type -> Type -> Type) Source # | |
ArrowChoice arr => CategoryWith0 (WrappedArrow arr :: Type -> Type -> Type) Source # | |
Defined in Overloaded.Categories type Initial (WrappedArrow arr) :: k Source # initial :: forall (a :: k). WrappedArrow arr (Initial (WrappedArrow arr)) a Source # |
class Category cat => CocartesianCategory (cat :: k -> k -> Type) where Source #
Cocartesian category is a monoidal category where monoidal product is the categorical coproduct.
inl :: cat a (Coproduct cat a b) Source #
inr :: cat b (Coproduct cat a b) Source #
fanin :: cat a c -> cat b c -> cat (Coproduct cat a b) c Source #
is written as \([f, g]\) in category theory literature.fanin
f g
Instances
Bicartesian
class (CartesianCategory cat, CocartesianCategory cat) => BicartesianCategory cat where Source #
Bicartesian category is category which is both cartesian and cocartesian.
We also require distributive morpism.
distr :: cat (Product cat (Coproduct cat a b) c) (Coproduct cat (Product cat a c) (Product cat b c)) Source #
Instances
Monad m => BicartesianCategory (Kleisli m :: Type -> Type -> Type) Source # | |
BicartesianCategory ((->) :: Type -> Type -> Type) Source # | |
Monad m => BicartesianCategory (Star m :: Type -> Type -> Type) Source # | |
ArrowChoice arr => BicartesianCategory (WrappedArrow arr :: Type -> Type -> Type) Source # | |
Defined in Overloaded.Categories distr :: forall (a :: k) (b :: k) (c :: k). WrappedArrow arr (Product (WrappedArrow arr) (Coproduct (WrappedArrow arr) a b) c) (Coproduct (WrappedArrow arr) (Product (WrappedArrow arr) a c) (Product (WrappedArrow arr) b c)) Source # |
Closed cartesian category
class CartesianCategory cat => CCC (cat :: k -> k -> Type) where Source #
Closed cartesian category.
type Exponential cat :: k -> k -> k Source #
represents \(B^A\). This is due how (->) works.Exponential
cat a b
eval :: cat (Product cat (Exponential cat a b) a) b Source #
transpose :: cat (Product cat a b) c -> cat a (Exponential cat b c) Source #
Instances
Monad m => CCC (Kleisli m :: Type -> Type -> Type) Source # | |
Defined in Overloaded.Categories type Exponential (Kleisli m) :: k -> k -> k Source # | |
CCC ((->) :: Type -> Type -> Type) Source # | |
Defined in Overloaded.Categories type Exponential (->) :: k -> k -> k Source # eval :: forall (a :: k) (b :: k). Product (->) (Exponential (->) a b) a -> b Source # transpose :: forall (a :: k) (b :: k) (c :: k). (Product (->) a b -> c) -> a -> Exponential (->) b c Source # | |
Monad m => CCC (Star m :: Type -> Type -> Type) Source # | |
Defined in Overloaded.Categories type Exponential (Star m) :: k -> k -> k Source # | |
ArrowApply arr => CCC (WrappedArrow arr :: Type -> Type -> Type) Source # | |
Defined in Overloaded.Categories type Exponential (WrappedArrow arr) :: k -> k -> k Source # eval :: forall (a :: k) (b :: k). WrappedArrow arr (Product (WrappedArrow arr) (Exponential (WrappedArrow arr) a b) a) b Source # transpose :: forall (a :: k) (b :: k) (c :: k). WrappedArrow arr (Product (WrappedArrow arr) a b) c -> WrappedArrow arr a (Exponential (WrappedArrow arr) b c) Source # |
Generalized element
class Category cat => GeneralizedElement (cat :: k -> k -> Type) where Source #
Instances
GeneralizedElement ((->) :: Type -> Type -> Type) Source # | |
Arrow arr => GeneralizedElement (WrappedArrow arr :: Type -> Type -> Type) Source # | |
Defined in Overloaded.Categories type Object (WrappedArrow arr) a Source # konst :: forall (a :: k) (x :: k). Object (WrappedArrow arr) a -> WrappedArrow arr x a Source # |
WrappedArrow
newtype WrappedArrow arr a b Source #
WrapArrow | |
|