| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
SubHask.Category
Description
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.
Associated Types
type ValidCategory cat a :: Constraint Source
Methods
id :: ValidCategory cat a => cat a a Source
Instances
| 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
Methods
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
Methods
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.
Methods
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.
Methods
($$) :: cat a b -> ProofOf_ cat a -> ProofOf_ cat b infixr 0 Source
If you want to apply a function inside of a proof, you must use the "($$)" operator instead of the more commonly used "($)".
FIXME: This is rather inelegant. Is there any way to avoid this?
Instances
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.
Instances