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

Posted 2023-05-08

【中文标题】我可以验证给定的函数类型签名是不是具有潜在的实现吗？

【英文标题】：Can I verify whether a given function type signature has a potential implementation?我可以验证给定的函数类型签名是否具有潜在的实现吗？

【发布时间】：2018-07-24 04:34:11

【问题描述】：

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

foo :: a -> b
foo x = x

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

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

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

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

【问题讨论】：

您可能会发现djinn-lib 和/或djinn-ghc 有点帮助。另见djinn。另请参阅 hedonisticlearning.com/djinn 并注意 lambdabot 也知道如何使用 djinn。

参见。还有Given a Haskell type signature, is it possible to generate the code automatically? 和How does Djinn work?

【参考方案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 对应关系所解决的。

【讨论】：

“直觉逻辑中有可以决定可证明性的算法” 能否提供参考？热衷于阅读有关其工作原理的信息；我的直觉告诉我，可证明性似乎是一种可能无法确定的事情，因此对我来说可能是肥沃的学习场所:)

我正在寻找一种快速的算法解决方案，并找到了一个需要研究的特殊领域。我认为暂时检查某些东西是否不是经典的重言式就足够了。谢谢！

@BenjaminHodgson 上面我隐含地指的是简单类型/命题直觉逻辑，它是可判定的。一旦你开始添加例如我相信，rank-2 多态性、GADT 等事情不再是可判定的。无论如何，对于简单类型，您可以采用 Gentzen 的 LJ 推理规则（没有 CUT）并自下而上进行证明搜索，不确定地尝试所有可能的规则。方便的是，自下而上，LJ 规则只涉及目标公式的子公式，这些子公式是有限的，所以我们要么找到证明，要么再次访问相同的状态（允许我们修剪搜索）

@BenjaminHodgson 您可以尝试使用cool online demo 中的规则。在自下而上搜索的每一步，我们只有有限数量的选择，而且由于子公式的性质，搜索空间是有限的。因此，我们要么找到一个证明，要么重新访问以前的状态（这样我们就可以检测到我们在循环运行并修剪搜索分支）。

@ftor fix （以及任何涉及一般递归的东西）是不允许的，因为否则fix id :: T 对于任何T，并且所有类型都被居住，这并不有趣。基本上，Curry-Howard 对应在没有递归的语言中成立。 （可以允许某种形式的递归，例如原始递归）

【参考方案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。

【讨论】：

就目前而言，这并不是对这个问题的真正独立答案。你能总结一下链接的一些要点吗？在链接腐烂的情况下，这里对未来的读者没有任何帮助。

感谢您指出这一点。我在 Hackage 上添加了包本身的链接，并简要说明了它的作用。