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

Question

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

foo :: a -> b
foo x = x

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

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

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

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

score 9 · Accepted Answer

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

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

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

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

例如，上述两种类型

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

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

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

score 7 · Accepted Answer

这是最近作为 GHC 插件实现的，不幸的是目前需要 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 的博文，其中还提到了其他一些选项：djinn（已经在此处的其他评论中）、exference、Scala 的curryhoward 、Idris 的 hezarfen。

2 回答 2