Overloaded.Categories

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, not Arrow
• CocartesianCategory, not ArrowChoice (implementation relies on BicartesianCategory)
• CCC, not ArrowApply (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!

Documentation

class Category (cat :: k -> k -> Type)

A class for categories. Instances should satisfy the laws

f . id  =  f  -- (right identity)
id . f  =  f  -- (left identity)
f . (g . h)  =  (f . g) . h  -- (associativity)

Minimal complete definition

id, (.)

Instances

Category (Coercion :: k -> k -> Type)

Since: base-4.7.0.0

Defined in Control.Category

Methods

id :: Coercion a a

(.) :: Coercion b c -> Coercion a b -> Coercion a c

Category ((:~:) :: k -> k -> Type)

Since: base-4.7.0.0

Defined in Control.Category

Methods

id :: a :~: a

(.) :: (b :~: c) -> (a :~: b) -> a :~: c

Category ((:~~:) :: k -> k -> Type)

Since: base-4.10.0.0

Defined in Control.Category

Methods

id :: a :~~: a

(.) :: (b :~~: c) -> (a :~~: b) -> a :~~: c

(Category p, Category q) => Category (Product p q :: k -> k -> Type)

Defined in Data.Bifunctor.Product

Methods

id :: Product p q a a

(.) :: Product p q b c -> Product p q a b -> Product p q a c

(Applicative f, Category p) => Category (Tannen f p :: k -> k -> Type)

Defined in Data.Bifunctor.Tannen

Methods

id :: Tannen f p a a

(.) :: Tannen f p b c -> Tannen f p a b -> Tannen f p a c

(Applicative f, Monad f) => Category (WhenMissing f :: Type -> Type -> Type)

Since: containers-0.5.9

Defined in Data.IntMap.Internal

Methods

id :: WhenMissing f a a

(.) :: WhenMissing f b c -> WhenMissing f a b -> WhenMissing f a c

Category ((->) :: Type -> Type -> Type)

Since: base-3.0

Defined in Control.Category

Methods

id :: a -> a

(.) :: (b -> c) -> (a -> b) -> a -> c

(Monad f, Applicative f) => Category (WhenMatched f x :: Type -> Type -> Type)

Since: containers-0.5.9

Defined in Data.IntMap.Internal

Methods

id :: WhenMatched f x a a

(.) :: 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

Methods

id :: WhenMissing f k a a

(.) :: WhenMissing f k b c -> WhenMissing f k a b -> WhenMissing f k a c

(Monad f, Applicative f) => Category (WhenMatched f k x :: Type -> Type -> Type)

Since: containers-0.5.9

Defined in Data.Map.Internal

Methods

id :: WhenMatched f k x a a

(.) :: WhenMatched f k x b c -> WhenMatched f k x a b -> WhenMatched f k x a c

identity :: Category cat => cat a a

A non-clashing name for id.

(%%) :: Category cat => cat b c -> cat a b -> cat a c infixr 9

A non-clashing name for (.).

class Category cat => CategoryWith1 (cat :: k -> k -> Type) where

Category with terminal object.

Associated Types

type Terminal cat :: k

Methods

terminal :: cat a (Terminal cat)

Instances

CategoryWith1 ((->) :: Type -> Type -> Type)

Defined in Overloaded.Categories

Associated Types

type Terminal (->) :: k

Methods

terminal :: a -> Terminal (->)

class CategoryWith1 cat => CartesianCategory (cat :: k -> k -> Type) where

Cartesian category is a monoidal category where monoidal product is the categorical product.

Associated Types

type Product cat :: k -> k -> k

Methods

proj1 :: cat (Product cat a b) a

proj2 :: cat (Product cat a b) b

fanout :: cat a b -> cat a c -> cat a (Product cat b c)

fanout f g is written as \(\langle f, g \rangle\) in category theory literature.

Instances

CartesianCategory ((->) :: Type -> Type -> Type)

Defined in Overloaded.Categories

Associated Types

type Product (->) :: k -> k -> k

Methods

proj1 :: Product (->) a b -> a

proj2 :: Product (->) a b -> b

fanout :: (a -> b) -> (a -> c) -> a -> Product (->) b c

class Category cat => CocartesianCategory (cat :: k -> k -> Type) where

Cocartesian category is a monoidal category where monoidal product is the categorical coproduct.

Associated Types

type Coproduct cat :: k -> k -> k

Methods

inl :: cat a (Coproduct cat a b)

inr :: cat b (Coproduct cat a b)

fanin :: cat a c -> cat b c -> cat (Coproduct cat a b) c

fanin f g is written as \([f, g]\) in category theory literature.

Instances

CocartesianCategory ((->) :: Type -> Type -> Type)

Defined in Overloaded.Categories

Associated Types

type Coproduct (->) :: k -> k -> k

Methods

inl :: a -> Coproduct (->) a b

inr :: b -> Coproduct (->) a b

fanin :: (a -> c) -> (b -> c) -> Coproduct (->) a b -> c

class (CartesianCategory cat, CocartesianCategory cat) => BicartesianCategory cat where

Bicartesian category is category which is both cartesian and cocartesian.

We also require distributive morpism.

Methods

distr :: cat (Product cat (Coproduct cat a b) c) (Coproduct cat (Product cat a c) (Product cat b c))

Instances

BicartesianCategory ((->) :: Type -> Type -> Type)

Defined in Overloaded.Categories

Methods

distr :: Product (->) (Coproduct (->) a b) c -> Coproduct (->) (Product (->) a c) (Product (->) b c)

class CartesianCategory cat => CCC (cat :: k -> k -> Type) where

Closed cartesian category.

Associated Types

type Exponential cat :: k -> k -> k

Exponential cat a b represents \(B^A\). This is due how (->) works.

Methods

eval :: cat (Product cat (Exponential cat a b) a) b

transpose :: cat (Product cat a b) c -> cat a (Exponential cat b c)

Instances

CCC ((->) :: Type -> Type -> Type)

Defined in Overloaded.Categories

Associated Types

type Exponential (->) :: k -> k -> k

Methods

eval :: Product (->) (Exponential (->) a b) a -> b

transpose :: (Product (->) a b -> c) -> a -> Exponential (->) b c

class Category cat => GeneralizedElement (cat :: k -> k -> Type) where

Associated Types

type Object cat (a :: k) :: Type

Methods

konst :: Object cat a -> cat x a

Instances

GeneralizedElement ((->) :: Type -> Type -> Type)

Defined in Overloaded.Categories

Associated Types

type Object (->) a :: Type

Methods

konst :: Object (->) a -> x -> a