Является ли это точным примером Haskell Pullback?

Question

Я все еще пытаюсь понять интуицию откат (от теории категорий), пределы и универсальные свойства, и я не совсем понимаю их полезность, так что, возможно, вы могли бы помочь пролить некоторое понимание на это, а также проверить мой тривиальный пример?

Ниже приведено намеренное подробное описание. Откат должен быть (p, p1, p2), а (q, q1, q2) является одним из примеров не универсального объекта для «проверки» отката, чтобы проверить, правильно ли перемещаются вещи.

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

Я просто пытался придумать пример, который соответствует определению, но он не кажется особенно полезным. Когда я буду «искать» откат или использовать его?

Answer 1

Я не уверен, что функции Haskell - лучший контекст , в котором можно говорить о отрывах.

Выдвижная задняя часть ->B и C ->B могут быть идентифицированы с подмножеством A х C, и подмножество отношения не непосредственно выражается Система типа Haskell's . В вашем конкретном примере втягивания обратно будет один элемент (1, True), потому что х = 1 и б = True, являются только значения, для которых е (х) = г (b).

Некоторые хорошие «практические» примеры выдвижных спины можно найти на стр 41 Category Theory for Scientists Дэвид И. Спивак.

Реляционные соединения - это типичный пример отката , который встречается в информатике. Запрос:

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

выбирает пары строк (, б), где является строкой из таблицы А и б является строкой из таблицы B и где некоторая функция a равна некоторой другой функции b. В этом случае функции , оттянутые назад, равны f (a) = a.x и g (b) = b.y.

Answer 2

Другим интересным примером отката является унификация типа в выводе типа. Вы получаете ограничения типа из нескольких мест, где используется переменная, и вы хотите найти самое узкое унифицирующее ограничение. Я упоминаю этот пример в my blog.