Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Is this an accurate example of a Haskell Pullback?

I'm still trying to grasp an intuition of pullbacks (from category theory), limits, and universal properties, and I'm not quite catching their usefulness, so maybe you could help shed some insight on that as well as verifying my trivial example?

The following is intentionally verbose, the pullback should be (p, p1, p2), and (q, q1, q2) is one example of a non-universal object to "test" the pullback against to see if things commute properly.

-- MY DIAGRAM, A -> B <- C
type A = Int
type C = Bool
type B = (A, C)
f :: A -> B
f x = (x, True)
g :: C -> B
g x = (1, x)

-- PULLBACK, (p, p1, p2)
type PL = Int
type PR = Bool
type P = (PL, PR)
p = (1, True) :: P
p1 = fst
p2 = snd
-- (g . p2) p == (f . p1) p

-- TEST CASE
type QL = Int
type QR = Bool
type Q = (QL, QR)
q = (152, False) :: Q
q1 :: Q -> A
q1 = ((+) 1) . fst
q2 :: Q -> C
q2 = ((||) True) . snd

u :: Q -> P
u (_, _) = (1, True)
-- (p2 . u == q2) && (p1 . u = q1)

I was just trying to come up with an example that fit the definition, but it doesn't seem particularly useful. When would I "look for" a pull back, or use one?

like image 691
Josh.F Avatar asked Aug 18 '16 22:08

Josh.F


1 Answers

I'm not sure Haskell functions are the best context in which to talk about pull-backs.

The pull-back of A -> B and C -> B can be identified with a subset of A x C, and subset relationships are not directly expressible in Haskell's type system. In your specific example the pull-back would be the single element (1, True) because x = 1 and b = True are the only values for which f(x) = g(b).

Some good "practical" examples of pull-backs may be found starting on page 41 of Category Theory for Scientists by David I. Spivak.

Relational joins are the archetypal example of pull-backs which occur in computer science. The query:

SELECT ...
FROM A, B
WHERE A.x = B.y

selects pairs of rows (a,b) where a is a row from table A and b is a row from table B and where some function of a equals some other function of b. In this case the functions being pulled back are f(a) = a.x and g(b) = b.y.

like image 110
ErikR Avatar answered Nov 09 '22 01:11

ErikR