Ist dies ein genaues Beispiel für einen Haskell Pullback?

Question

Ich versuche immer noch, eine Intuition von Pullbacks (aus der Kategorie Theorie), Grenzen und universellen Eigenschaften zu erfassen, und ich bin nicht ganz anziehend ihre Nützlichkeit, so vielleicht könnten Sie dazu beitragen, einige Einblicke darauf sowie mein triviales Beispiel verifizieren?

Das folgende ist absichtlich ausführlich, der Pullback sollte (p, p1, p2) sein, und (q, q1, q2) ist ein Beispiel eines nicht-universellen Objekts, um den Pullback zu "testen", um zu sehen, ob Sachen richtig pendeln.

-- 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) 

Ich habe nur versucht, mit einem Beispiel zu kommen, die die Definition passen, aber nicht besonders nützlich zu sein scheinen. Wann würde ich nach einem Rückzug suchen oder einen nutzen?

Answer 1

Ich bin mir nicht sicher, Haskell Funktionen sind der beste Kontext in denen über Pull-Backs zu sprechen.

Die Pull-back von A ->B und C ->B kann mit einer Untergruppe von A x C, und Teilmenge Beziehungen sind nicht direkt ausdrückbar identifiziert werden Haskell Typ System. In Ihrem speziellen Beispiel wäre die Rückzieh das einzelne Element (1, True), weil x = 1 und b = True sind die einzigen Werte, für die f (x) = g (b).

Einige gute "praktische" Beispiele von Pull-Backs finden Sie unter ab Seite 41 von Category Theory for Scientists von David I. Spivak.

Relationale Joins sind das archetypische Beispiel für Pullbacks , die in der Informatik auftreten. Die Abfrage:

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

wählt Paare von Reihen (a, b) wobei a ist eine Zeile der Tabelle A und b ist eine Zeile von Tabelle B und in dem einige Funktion der Ein entspricht einer anderen Funktion von b. In diesem Fall sind die Funktionen , die zurückgezogen werden, f (a) = a.x und g (b) = b.y.

Answer 2

Ein weiteres interessantes Beispiel für einen Pullback ist die Typvereinheitlichung in Typinferenz. Sie erhalten Typabhängigkeiten von mehreren Stellen, an denen eine Variable verwendet wird, und Sie möchten die engste vereinheitlichende Einschränkung finden. Ich erwähne dieses Beispiel in my blog.