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

Answer 1

您可以应用后续演算。

简短的例子，使用 type a -> a，我们可以构造 term like: \x -> (\y -> y) x，但这仍然归一化为\x -> xwhich is 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 () ~ ()

---

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