|
|
|
|
|
by Tekmo
3879 days ago
|
|
The generic benefit of a category is the proof that it satisfies the identity and associativity laws. This lets you write "generic proofs" that work for any category. For example, take the following example type: newtype Example f c a b = Example (f (c a b))
instance (Applicative f, Category c) => Category (Example f c) where
id = Example (pure id)
Example f . Example g = Example (liftA2 (.) f g)
You can prove that if `c` satisfies the `Category` laws and `f` satisfies the `Applicative` laws, then `Example f c` also satisfies the `Category` laws.This in turn lets you take any `Category` and keep extending it with as many `Applicative`s as you want in any order, confident in the knowledge that your extended `Category` still satisfies the `Category` laws. This is a common pattern in code that is organized around category theory and/or abstract algebra and I wrote a post showing a simpler example of this phenomenon (using `Monoid` instead of `Category`): http://www.haskellforall.com/2014/07/equational-reasoning-at... |
|