12

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?

2 Answers 2

14

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.

2
  • 2
    Ah, that makes sense. Would there be an analogous operation for pushouts in relational languages?
    – Josh.F
    Commented Aug 19, 2016 at 2:45
  • 1
    Isn't the fundamental problem that Haskell lacks a way to express that particular diagrams commute, rather than anything to do with subsets? I wonder if TypeInType gives us enough power to talk about these ideas, painfully, at the type level.
    – dfeuer
    Commented Aug 21, 2016 at 3:24
14

Another interesting example of a pullback is type unification in type inference. You get type constraints from several places where a variable is used, and you want to find the tightest unifying constraint. I mention this example in my blog.

1
  • 2
    your blog is a treasure trove, and I am especially loving Cat. Theory for Programmers. Thank you, and I'll be obsessing over it for weeks to come until I can competently catch up to Free/Forgetful Adjunctions. Can't wait for Monads! :)
    – Josh.F
    Commented Aug 20, 2016 at 18:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.