我如何证明一个 Haskell 类型只有一个函数？

Question

在this answer 中，Gabriel Gonzalez 展示了如何证明id 是forall a. a -> a 的唯一居民。为此（在最正式的证明迭代中），他使用Yoneda lemma 证明该类型与() 同构，并且由于() 中只有一个值，所以@987654327 的类型必须@。总结一下，他的证明是这样的：

米田说：

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 东西，我很确定没有其他此类功能。

我认为无论我选择哪种类型，Gabriel 的技巧都不会立即适用于此。是否有其他方法（同样形式化！）我可以展示这种类型和() 之间的同构？

Answer 1

您可以申请sequent calculus。

简短的例子，使用类型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 似乎是该类型的唯一居民。

---

米田引理方法，要小心居然有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 () ~ ()

---

编辑第一种方法感觉有点随意，但感觉更直接：给定一组受限的规则，如何构造证明，我们可以构造多少个证明？