这是Haskell回调的一个准确例子吗?

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

可以找到一些很好的"实用"的回拉例子从《科学家范畴论》第41页开始作者:David I. Spivak。

关系连接是回调的典型例子这发生在计算机科学中。查询:

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

选择行对(a，b)，其中a是表a中的一行b是表b中的一行，其中a的某个函数等于b的其他函数。在这个例子中是函数被撤出 f (a) = a.x 和 g (b) = b.y 。

Answer 2

另一个有趣的回调示例是类型推断中的类型统一。您从使用变量的几个地方获得类型约束，并且希望找到最严格的统一约束。我在我的博客中提到过这个例子。