haskell - 我可以验证给定的函数类型签名是否具有潜在的实现吗？

Question

在显式类型注释的情况下，Haskell 检查推断类型是否至少与其签名一样多态，或者换句话说，推断类型是否是显式类型的子类型。因此，以下函数是错误类型的:

foo :: a -> b
foo x = x

bar :: (a -> b) -> a -> c
bar f x = f x

然而，在我的场景中，我只有一个函数签名并且需要验证它是否被一个潜在的实现“占据”——希望这个解释是有道理的!

由于参数属性，我假设这两个 foo和 bar不存在实现，因此，两者都应该被拒绝。但我不知道如何以编程方式得出结论。

目标是整理出所有或至少一部分无效类型签名，如上面的那些。我很感激每一个提示。

Answer 1

Goal is to sort out all or at least a subset of invalid type signatures like ones above. I am grateful for every hint.

您可能想看看 Curry-Howard correspondence .

基本上，函数式程序中的类型对应于逻辑公式。
只需更换 ->暗示， (,)与连词 (AND) 和 Either带析取(OR)。居住类型正是那些具有相应公式的那些，这是直觉逻辑中的重言式。

有一些算法可以决定直觉逻辑中的可证明性(例如，在 Gentzen 的序列中利用削减消除)，但问题是 PSPACE 完全的，所以通常我们不能处理非常大的类型。但是，对于中型类型，切割消除算法可以正常工作。

如果您只想要一个无人居住类型的子集，则可以限制为具有相应公式的那些，这不是经典逻辑中的重言式。这是正确的，因为直觉主义的重言式也是经典的。检查公式是否 P不是经典的重言式可以通过询问 not P 来完成是一个可满足的公式。所以，问题出在NP上。不多，但比 PSPACE-complete 好。

例如，上述两种类型

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

显然不是重言式!因此他们没有人居住。

最后，请注意在 Haskell 中 undefined :: T和 let x = x in x :: T对于任何类型 T ，所以从技术上讲，每种类型都有人居住。一旦限制为终止没有运行时错误的程序，我们就会得到一个更有意义的“inhabited”概念，这是 Curry-Howard 对应关系所解决的概念。