Safe Haskell | None |
---|---|

Language | Haskell2010 |

SubHask supports two ways to encode categories in Haskell.

- *Method 1**

Create a data type of kind `k -> k -> *`

,
and define an instance of the Category class.
Because our version of Category uses the ConstraintKinds extension,
we can encode many more categories than the standard Data.Category class.

There are many subclasses of Category for categories with extra features. Most of this module is spent defining these categories and instantiating appropriate instances for Hask.

Unfortunately, many of the terms used in category theory are non-standard. In this module, we try to follow the names used out in John Baez and Mike Stay's Rosetta Stone paper. This is a fairly accessible introduction to category theory for Haskeller's ready to move beyond "monads are monoids in the category of endofunctors."

FIXME: Writing laws for any classes in this file requires at least the Eq class from SubHask.Algebra. Hence, the laws are not explicitly stated anywhere.

- *Method 2**

For any subcategory of Hask, we can define a type "ProofOf subcat".
Then any function of type `ProofOf subcat a -> ProofOf subcat b`

is an arrow within `subcat`

.
This is essentially a generalization of automatic differentiation to any category.

TODO: This needs a much better explanation and examples.

- *Comparison** Method 1 is the primary way to represent a category. It's main advantage is that we have complete control over the representation in memory. With method 2, everything must be wrapped within function calls. Besides this layer of indirection, we also increase the chance for accidental space leaks.

Usually, it is easier to work with functions using method 1, but it is easier to construct functions using method 2.

FIXME: Currently, each category comes with its own mechanism for converting between the two representations. We need something more generic.

- class Category cat where
- type ValidCategory cat a :: Constraint
- id :: ValidCategory cat a => cat a a
- (.) :: cat b c -> cat a b -> cat a c

- (<<<) :: Category cat => cat b c -> cat a b -> cat a c
- (>>>) :: Category cat => cat a b -> cat b c -> cat a c
- type Hask = (->)
- ($) :: Concrete subcat => subcat a b -> a -> b
- ($!) :: Concrete subcat => subcat a b -> a -> b
- embedHask :: Concrete subcat => subcat a b -> a -> b
- embedHask2 :: Concrete subcat => subcat a (subcat b c) -> a -> b -> c
- withCategory :: Concrete subcat => proxy subcat -> subcat a b -> a -> b
- embed2 :: subcat <: cat => subcat a (subcat a b) -> cat a (cat a b)
- fst :: (a, b) -> a
- snd :: (a, b) -> b
- type Concrete cat = cat <: (->)
- class (Category cat, ValidCategory cat (TUnit cat)) => Monoidal cat where
- type Tensor cat :: k -> k -> k
- type TUnit cat :: k
- tensor :: (ValidCategory cat a, ValidCategory cat b) => cat a (cat b (Tensor cat a b))
- tunit :: proxy cat -> TUnit cat

- class Monoidal cat => Braided cat where
- class Braided cat => Symmetric cat
- class Symmetric cat => Cartesian cat where
- fst_ :: (ValidCategory cat a, ValidCategory cat b, ValidCategory cat (Tensor cat a b)) => cat (Tensor cat a b) a
- snd_ :: (ValidCategory cat a, ValidCategory cat b, ValidCategory cat (Tensor cat a b)) => cat (Tensor cat a b) b
- terminal :: ValidCategory cat a => a -> cat a (TUnit cat)
- initial :: ValidCategory cat a => a -> cat (TUnit cat) a

- const :: (Cartesian cat, ValidCategory cat a, ValidCategory cat b) => a -> cat b a
- const2 :: (Cartesian cat, ValidCategory cat a, ValidCategory cat b) => a -> b -> cat b a
- class Braided cat => Closed cat where
- class Category cat => Groupoid cat where
- inverse :: cat a b -> cat b a

- class Symmetric cat => Compact cat where
- class Category cat => Dagger cat where
- trans :: cat a b -> cat b a

- class Concrete cat => Provable cat where
- type family ProofOf_ cat a
- data family ProofOf cat a

# Documentation

class Category cat where Source

This `Category`

class modifies the one in the Haskell standard to include the `ValidCategory`

type constraint.
This constraint let's us make instances of arbitrary subcategories of Hask.

Subcategories are defined using the subtyping mechanism "(<:)". Intuitively, arrows and objects in a subcategory satisfy additional properties that elements of the larger category do not necessarily satisfy. Elements of a subcategory can always be embeded in the larger category. Going in the other direction, however, requires a proof. These proofs can (usually) not be verified by the type system and are therefore labeled unsafe.

type ValidCategory cat a :: Constraint Source

id :: ValidCategory cat a => cat a a Source

Category * (->) Source | |

Category * DenseFunction Source | |

Category * SparseFunctionMonoid Source | |

Category * SparseFunction Source | |

Category * Polynomial_ Source | |

Category * (+>) Source | |

Category * cat => Category * (IncreasingT cat) Source | |

Category * cat => Category * (MonT cat) Source | |

Category * cat => Category * ((/) cat obj) Source | |

Category * cat => Category * (ConstrainedT xs cat) Source | |

Category k cat => Category k (BijectiveT k k cat) Source | |

Category k cat => Category k (SurjectiveT k k cat) Source | |

Category k cat => Category k (InjectiveT k k cat) Source | |

(Category k cat1, Category k cat2) => Category k ((><) k k cat1 cat2) Source | |

Monad cat f => Category * (Kleisli * * * cat f) Source | |

(Category k1 cat1, Category k1 cat2, Category k cat3) => Category k (Comma (k -> k -> *) k k cat1 cat2 cat3) Source |

(<<<) :: Category cat => cat b c -> cat a b -> cat a c Source

An alternative form of function composition taken from Control.Arrow

(>>>) :: Category cat => cat a b -> cat b c -> cat a c Source

An alternative form of function composition taken from Control.Arrow

# Hask

The category with Haskell types as objects, and functions as arrows.

More details available at the Haskell wiki.

($) :: Concrete subcat => subcat a b -> a -> b infixr 0 Source

We generalize the Prelude's definition of "$" so that it applies to any
subcategory of `Hask`

(that is, any `Concrete`

`Category`

. This lets us
easily use these subcategories as functions. For example, given a polynomial
function

f :: Polynomial Double

we can evaluate the polynomial at the number 5 by

f $ 5

NOTE:
Base's implementation of `$`

has special compiler support that let's it work with the RankNTypes extension.
This version does not.
See this stackoverflow question for more detail.

embedHask2 :: Concrete subcat => subcat a (subcat b c) -> a -> b -> c Source

Embeds a binary function into `Hask`

withCategory :: Concrete subcat => proxy subcat -> subcat a b -> a -> b Source

This is a special form of the `embed`

function which can make specifying the
category we are embedding into easier.

embed2 :: subcat <: cat => subcat a (subcat a b) -> cat a (cat a b) Source

FIXME: This would be a useful function to have, but I'm not sure how to implement it yet!

"fst" specialized to Hask to aid with type inference FIXME: this will not be needed with injective types

"snd" specialized to Hask to aid with type inference FIXME: this will not be needed with injective types

# Special types of categories

type Concrete cat = cat <: (->) Source

Technicaly, a concrete category is any category equiped with a faithful
functor to the category of sets. This is just a little too platonic to
be represented in Haskell, but `Hask`

makes a pretty good approximation.
So we call any `SubCategory`

of `Hask`

`Concrete`

. Importantly, not
all categories are concrete. See the `Slice`

category for an example.

class (Category cat, ValidCategory cat (TUnit cat)) => Monoidal cat where Source

The intuition behind a monoidal category is similar to the intuition
behind the `Monoid`

algebraic structure. Unfortunately,
there are a number of rather awkward laws to work out the technical details.
The associator and unitor functions are provided to demonstrate the
required isomorphisms.

More details available at wikipedia

tensor :: (ValidCategory cat a, ValidCategory cat b) => cat a (cat b (Tensor cat a b)) Source

class Monoidal cat => Braided cat where Source

Braided categories let us switch the order of tensored objects.

class Symmetric cat => Cartesian cat where Source

In a cartesian monoidal category, the monoid object acts in a particularly nice way where we can compose and decompose it.
Intuitively, we can delete information using the `fst`

and `snd`

arrows, as well as
duplicate information using the `duplicate`

arrow.

More details available at ncatlab

fst_ :: (ValidCategory cat a, ValidCategory cat b, ValidCategory cat (Tensor cat a b)) => cat (Tensor cat a b) a Source

snd_ :: (ValidCategory cat a, ValidCategory cat b, ValidCategory cat (Tensor cat a b)) => cat (Tensor cat a b) b Source

terminal :: ValidCategory cat a => a -> cat a (TUnit cat) Source

initial :: ValidCategory cat a => a -> cat (TUnit cat) a Source

const :: (Cartesian cat, ValidCategory cat a, ValidCategory cat b) => a -> cat b a Source

Creates an arrow that ignores its first parameter.

const2 :: (Cartesian cat, ValidCategory cat a, ValidCategory cat b) => a -> b -> cat b a Source

Based on the type signature, this looks like it should be the inverse of "embed" function. But it's not. This function completely ignores its second argument!

class Braided cat => Closed cat where Source

Closed monoidal categories allow currying, and closed braided categories allow flipping. We combine them into a single Closed class to simplify notation.

In general, closed categories need not be either Monoidal or Braided. All a closed category requires is that all arrows are also objects in the category. For example, `a +> (b +> c)` is a vallid arrow in the category `(+>)`. But I don't know of any uses for this general definition of a closed category. And this restricted definition seems to have a lot of uses.

curry :: cat (Tensor cat a b) c -> cat a (cat b c) Source

uncurry :: cat a (cat b c) -> cat (Tensor cat a b) c Source

flip :: cat a (cat b c) -> cat b (cat a c) Source

The default definition should be correct for any category, but can be overridden with a more efficient implementation.

FIXME: does this actually need to be in a class? or should it be a stand-alone function like "const"?

class Category cat => Groupoid cat where Source

Groupoids are categories where every arrow can be reversed.
This generalizes bijective and inverse functions.
Notably, `Hask`

is NOT a Groupoid.

More details available at wikipedia ncatlib, and stack overflow.

class Symmetric cat => Compact cat where Source

Compact categories are another generalization from linear algebra.
In a compact category, we can dualize any object in the same way that we
can generate a covector from a vector.
Notably, `Hask`

is NOT compact.

class Category cat => Dagger cat where Source

A dagger (also called an involution) is an arrow that is its own inverse.
Daggers generalize the idea of a transpose from linear algebra.
Notably, `Hask`

is NOT a dagger category.

# Proofs

class Concrete cat => Provable cat where Source

A provable category gives us the opposite ability as a Concrete category. Instead of embedding a function in the subcategory into Hask, we can embed certain functions from Hask into the subcategory.

data family ProofOf cat a Source

This data family can be used to provide proofs that an arrow in Hask (i.e. a function) can be embedded in some subcategory. We're travelling in the opposite direction of the subtyping mechanism. That's valid only in a small number of cases. These proofs give a type safe way to capture some (but not all) of those cases.