Skip to content

Instantly share code, notes, and snippets.

@zraffer
Created Nov 4, 2016
Embed
What would you like to do?
Scala Types are objects of Cartesian Closed Category
// Scala Types are objects of Cartesian Closed Category
// (w/o equalities, probably not a category, sorry)
object CCC {
// category structure
def id[T0]: T0=>T0 = x0=>x0
def mul[T1, T2, T3](f23: T2=>T3, f12: T1=>T2): (T1=>T3) = x1 => f23(f12(x1))
// terminal object; adjunction;
type _1_ = Unit
def TerminalUnit[T]: T=>_1_ = x=>()
// binary product functor; adjunction;
type [A, B] = (A, B)
def /⨯/[A1, A2, B1, B2]
(a12: A1=>A2, b12: B1=>B2)
: (A1B1) => (A2B2) =
{ case (a,b) => (a12(a), b12(b)) }
def ProductUnit[A]: A => (AA) = a => (a, a)
def ProductCounit1[A, B]: (AB) => A = { case (a,b) => a }
def ProductCounit2[A, B]: (AB) => B = { case (a,b) => b }
// exponentiation; adjunction;
type ^[A, B] = B => A
def /^/[A1, A2, B1, B2]
(a12: A1=>A2, b21: B2=>B1)
: (A1 ^ B1) => (A2 ^ B2) =
ba1 => b2 => a12(ba1(b21(b2)))
def ExpUnit[A, B]: A => ((AB)^ B) = a => b => (a, b)
def ExpCounit[A, B]: ((A ^ B)⨯ B) => A = { case (ba, b) => ba(b) }
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment