如何显示Haskell类型只由一个函数居住？

Question

在这个答案中,加布里埃尔冈萨雷斯展示了如何证明这id是唯一的居民forall a. a -> a.为了做到这一点(在最正式的证明迭代中),他表明该类型与()使用Yoneda引理同构,并且由于()其中只有一个值,所以必须使用类型id.总结一下,他的证据是这样的:

Yoneda说:

Functor f => (forall b . (a -> b) -> f b) ~ f a

如果a = ()和f = Identity,这变为:

(forall b. (() -> b) -> b) ~ ()

而且从简单来说() -> b ~ b,LHS基本上就是这种类型id.

这感觉就像一个适合的"魔术" id.我正在尝试为更复杂的函数类型做同样的事情:

(b -> a) -> (a -> b -> c) -> b -> c

但我不知道从哪里开始.我知道它有人居住\f g x = g (f x) x,如果你忽略丑陋?/ undefined东西,我很确定没有其他这类功能.

我不认为加布里埃尔的伎俩会立即适用于我选择类型的方式.是否有其他方法(同样正式!),我可以用它来显示这种类型和()？之间的同构？

Answer 1

您可以应用后续微积分.

简单的例子,对于类型a -> a,我们可以构造如下的术语:\x -> (\y -> y) x但是仍然可以将\x -> x其归一化id.在后续的微积分中,系统禁止构造"可还原"的证明.

你的类型是(b -> a) -> (a -> b -> c) -> b -> c非正式的:

f: b -> a
g: a -> b -> c
x: b
--------------
Goal: c

并没有太多方法可以继续:

apply g

f: b -> a
g: a -> b -> c
x: b
---------------
Subgoal0: a
Subgoal1: b


apply f

f: b -> a
g: a -> b -> c
x: b
---------------
Subgoal0': b
Subgoal1: b


-- For both
apply x

所以最后,似乎g (f x) x是这种类型的唯一居民.

Yoneda引理方法,实际上要小心forall x!

 (b -> a) -> (a -> b -> c) -> b -> c
 forall b a. (b -> a) -> b -> forall c. (a -> b -> c) -> c

让我们集中精力结束:

 (a -> b -> c) -> c ~ ((a,b) -> c) -> c

这是同构的(a, b),所以整个类型减少到

(b -> a) -> b -> (a, b)

采取 f = Compose (Reader b) (,b)

(b -> a) -> f a ~ f b ~ b -> (b,b)

采用HP a = (a,a)仿函数这是独一无二的:

b -> (b,b) ~ (() -> b) -> HP b ~ HP () ~ ()

编辑第一种方法感觉有点手工波浪,但感觉更直接:鉴于规则有限,如何构建证据,我们可以构建多少证据？