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

Question

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

foo :: a -> b
foo x = x

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

然而,在我的场景中,我只有一个函数签名,需要验证它是否被潜在的实现"居住" - 希望这个解释完全有意义!

由于parametricity财产我认为两者foo并bar没有不存在的实现,因此,两者都应该被拒绝.但我不知道如何以编程方式结束.

目标是整理所有或至少一部分无效类型签名,如上所述.我很感激每一个提示.

Answer 1

目标是整理所有或至少一部分无效类型签名,如上所述.我很感激每一个提示.

基本上,功能程序中的类型对应于逻辑公式.只需->用含义,(,)连词(AND)和Either析取(OR)替换.有人居住的类型正是具有相应公式的那些,这是直觉逻辑中的重言式.

有些算法可以决定直觉逻辑中的可证明性(例如,在Gentzen的序列中利用切割消除),但问题是PSPACE完全,因此通常我们不能使用非常大的类型.但是,对于中型类型,剪切消除算法工作正常.

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

例如,两种都是上述类型

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

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

最后请注意,在Haskell undefined :: T和let x = x in x :: T任何类型中T,技术上每种类型都有人居住.一旦限制终止没有运行时错误的程序,我们就会得到一个更有意义的"有人居住"的概念,这是Curry-Howard通信所解决的概念.

Answer 2

它由一个带有单个方法的类型类组成

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(已经在此处的其他评论中),exferences,curry,Scala,forzar.