这是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函数是讨论回调的最佳背景.

A - > B和C - > B的回拉可以用A x C的子集来识别,并且子集关系不能在Haskell的类型系统中直接表达.在您的具体示例中,回拉将是单个元素(1,True),因为x = 1和b = True是f(x)= g(b)的唯一值.

从 David I. Spivak的Science Theory for Scientists第41页开始,可以找到一些好的"实用"回撤示例.

关系连接是计算机科学中出现的回调的典型例子.查询:

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

选择对行(的一个,b),其中一个是从表A和行b是从表B和其中的一些功能的行一个 等于的一些其它函数b.在这种情况下,被拉回的函数是f(a)= ax和g(b)= by.

Answer 2

回调的另一个有趣例子是类型推断中的类型统一.您可以从使用变量的多个位置获取类型约束,并且您希望找到最紧密的统一约束.我在博客中提到了这个例子.