Skip to content

Instantly share code, notes, and snippets.

@ekmett
Created December 1, 2010 11:00
Embed
What would you like to do?
package scalaz
/**
* Defines a category.
*
* <p>
* All instances must satisfy 3 laws:
* <ol>
* <li><strong>left identity</strong><br/><code>∀ a. compose(id, a) == a</code></li>
* <li><strong>right identity</strong><br/><code>∀ a. compose(a, id) == a</code></li>
* <li><strong>associativity</strong><br/><code>∀ a b c. compose(a, compose(b, c)) == compose(compose(a, b), c)</code></li>
* </ol>
* </p>
*/
trait Hom {
type L
type H>:L
type C[_ >: L <: H, _ >: L <: H]
}
trait GeneralizedCategory {
type U <: Hom
type =>:[A>:U#L<:U#H,B>:U#L<:U#H] = U#C[A,B]
def id[A>:U#L<:U#H]: A =>: A
def compose[A>:U#L<:U#H, B>:U#L<:U#H, C>:U#L<:U#H](
f: B =>: C,
g: A =>: B
): A =>: C
def *[UY<:Hom](that : GeneralizedCategory {type U=UY}) = Category.ProductCategory[U,UY](this,that)
}
trait GeneralizedGroupoid extends GeneralizedCategory {
def invert[A>:U#L<:U#H,B>:U#L<:U#H](f : A =>: B): B =>: A
}
trait Category[~>:[_,_]] extends GeneralizedCategory {
trait U extends Hom {
type L = Nothing
type H = Any
type C[A,B] = ~>:[A,B]
}
}
trait Groupoid[~>:[_, _]] extends GeneralizedGroupoid with Category[~>:]
object Category {
import Scalaz._
import Leibniz._
/*
* Product Categories
*/
/** Index for a product category */
sealed trait P[+IX,+IY] { type _1 = IX; type _2 = IY }
case class ProductCategory[UX<:Hom,UY<:Hom](
_1: GeneralizedCategory{type U = UX},
_2: GeneralizedCategory{type U = UY}
) extends GeneralizedCategory with Hom {
type _1 = _1.type
type _2 = _2.type
type L = P[UX#L,UY#L]
type H = P[UX#H,UY#H]
case class C[A>:L<:H,B>:L<:H](
_1: UX#C[A#_1,B#_1],
_2: UY#C[A#_2,B#_2]
) extends P[UX#C[A#_1,B#_1], UY#C[A#_2,B#_2]]
type U = ProductCategory[UX,UY]
def id[A>:U#L<:U#H] = C(_1.id[A#_1],_2.id[A#_2])
def compose [A>:U#L<:U#H, B>:U#L<:U#H, C>:U#L<:U#H](f: B =>: C, g: A =>: B) =
C(_1.compose(f._1,g._1), _2.compose(f._2,g._2))
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment