如何证明 Haskell 类型包含一个且只有一个函数？

Question

在this answer, Gabriel Gonzalez shows how to show that id is the only inhabitant of forall a. a -> a. To do so (in the most formal iteration of the proof), he shows that the type is isomorphic to () using the Yoneda lemma中，由于()里面只有一个值，所以id的类型也必须如此。总结一下，他的证明是这样的：

Yoneda says:
Functor f => (forall b . (a -> b) -> f b) ~ f a
If a = () and f = Identity, this becomes:
(forall b. (() -> b) -> b) ~ ()
And since trivially () -> b ~ b, the LHS is basically the type of 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。在后续演算中系统禁止构造"reducable"证明。

您的类型是 (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 () ~ ()

EDIT 第一种方法感觉有点麻烦，但感觉更直接：给定一组受限制的规则，如何构建证明，有多少证明我们可以建造吗？

如何证明 Haskell 类型包含一个且只有一个函数？

How do I show that a Haskell type is inhabited by one and only one function?

haskell

category-theory

type-theory