Is this an accurate example of a Haskell pullback?

Question

I'm still trying to understand the intuition of failures (from category theory), limitations, and universal properties, and I don’t quite understand their usefulness, so maybe you could help shed some insight into this, as well as confirming my trivial example?

The following is intentionally verbose, the rollback should be (p, p1, p2) , and (q, q1, q2) is one example of a non-universal object for “checking” rollbacks to check if things are moving correctly.

 -- MY DIAGRAM, A -> B <- C type A = Int type C = Bool type B = (A, C) f :: A -> B fx = (x, True) g :: C -> B gx = (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 fits the definition, but it doesn't seem particularly useful. When will I “look for” a rollback or use it?

Answer 1

I'm not sure if Haskell functions are the best context in which to talk about waste.

A rollback A → B and C → B can be identified with a subset of A x C, and the relations of the subset are not directly expressed in Haskell's type. In your specific example, the guy will be the only element (1, True), since x = 1 and b = True are the only values ​​for which f (x) = g (b).

Some good “practical” examples of passages can be found starting on page 41 of Category Theory for Scientists by David I. Spivak.

Relational associations are a typical example of guy ropes that occur in computer science. Request:

 SELECT ... FROM A, B WHERE Ax = By 

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 is equal to some other function b. In this case, the functions (a) = ax and g (b) = by

Answer 2

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