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

Question

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

foo :: a -> b
foo x = x

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

然而，在我的场景中，我只有一个函数签名，需要验证它是否被潜在实现“占用” - 希望这个解释完全有道理！

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

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

Answer 1

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

您可能想看看Curry-Howard correspondence。

基本上，函数式程序中的类型对应于逻辑公式。 只需将 -> 替换为蕴涵，(,) 替换为合取 (AND)，Either 替换为析取 (OR)。有栖类型正是那些有对应公式的类型，这是直觉逻辑中的重言式。

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

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

比如上面提到的两种

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

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

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

Answer 2

Here's a recent implementation of that as a GHC plugin 目前需要 GHC HEAD。

---

它由一个类型类和一个方法组成

class JustDoIt a where
  justDoIt :: a

这样justDoIt 在插件可以找到其推断类型的居民时进行类型检查。

foo :: (r -> Either e a) -> (a -> (r -> Either e b)) -> (r -> Either e (a,b))
foo = justDoIt

有关更多信息，请阅读 Joachim Breitner 的 blogpost，其中还提到了一些其他选项：djinn（已经在此处的其他 cmets 中）、exference、curryhoward 用于 Scala，hezarfen 用于 Idris。