27

它在标题中所说的。如果我编写类型签名，是否可以通过算法生成具有该类型签名的表达式？

似乎有可能做到这一点。我们已经知道，如果类型是库函数类型签名的特例，Hoogle 可以通过算法找到该函数。另一方面，许多与一般表达式相关的简单问题实际上是无法解决的（例如，不可能知道两个函数是否做同样的事情），所以这是其中之一几乎是难以置信的。

一次问几个问题可能是不好的形式，但我想知道：

  • 可以做到吗？

  • 如果是这样，怎么做？

  • 如果没有，是否有任何限制情况成为可能？

  • 两个不同的表达式很可能具有相同的类型签名。你能计算出所有这些吗？甚至其中一些？

  • 有没有人有工作代码可以真正做到这一点？

4

4 回答 4

34

Djinn为 Haskell 类型的受限子集执行此操作，对应于一阶逻辑。但是，它不能管理递归类型或需要递归来实现的类型；因此，例如，它不能写出对应于命题“如果a蕴涵a，则a(a -> a) -> a ”的类型项（的类型），这显然是错误的；你可以用它来证明任何事情。确实，这就是产生⊥的原因。fixfix

如果您确实允许fix，那么编写一个程序来给出任何类型的术语都是微不足道的；该程序将简单地打印fix id每种类型。

Djinn 主要是一个玩具，但它可以做一些有趣的事情，比如为 and 派生正确的实例Monad和Reader给Cont定的类型。您可以通过安装djinn包或使用lambdabot来尝试，后者将其集成为命令。return(>>=)@djinn

于 2012-04-18T08:48:49.350 回答
14

okmij.org的Oleg对此有一个实现。这里有一个简短的介绍，但有文字的 Haskell 源代码包含该过程的详细信息和描述。（我不确定这与 Djinn 掌权有何对应，但这是另一个例子。）

在某些情况下没有唯一功能：

fst', snd' :: (a, a) -> a
fst' (a,_) = a
snd' (_,b) = b

不仅如此；在某些情况下，函数的数量是无限的：

list0, list1, list2 :: [a] -> a
list0 l = l !! 0
list1 l = l !! 1
list2 l = l !! 2
-- etc.

-- Or 
mkList0, mkList1, mkList2 :: a -> [a]
mkList0 _ = []
mkList1 a = [a]
mkList2 a = [a,a]
-- etc.

（如果你只想要总函数，那么考虑[a]限制为无限列表list0等list1，即data List a = Cons a (List a)）

事实上，如果你有递归类型，任何涉及这些的类型都对应于无数个函数。但是，至少在上述情况下，函数的数量是可数的，因此可以创建一个包含所有函数的（无限）列表。但是，我认为该类型[a] -> [a]对应于无数个函数（再次限制[a]为无限列表），因此您甚至无法枚举它们！

（总结：有些类型对应于有限、可数无限和不可数无限数量的函数。）

于 2012-04-18T09:20:39.567 回答
7

这在一般情况下是不可能的（对于像 Haskell 这样甚至没有强大的规范化属性的语言），并且仅在某些（非常）特殊情况下（以及对于更受限制的语言）才有可能，例如当 codomain 类型只有一个时构造函数（例如，一个函数f :: forall a. a -> ()可以唯一确定）。为了将给定签名的一组可能定义减少为只有一个定义的单例集，需要给出更多限制（例如，以附加属性的形式，如果不给出，仍然很难想象这会有什么帮助使用示例）。

从 (n-) 分类的角度来看，类型对应于对象，项对应于箭头（构造函数也对应于箭头），函数定义对应于 2 个箭头。这个问题类似于是否可以通过仅指定一组对象来构造具有所需属性的 2 类的问题。这是不可能的，因为您需要箭头和 2 箭头的显式构造（即编写术语和定义），或者允许使用特定属性集（仍需要显式定义）推断必要结构的演绎系统。

还有一个有趣的问题：给定一个 ADT（即 Hask 的子类别）是否可以自动派生 Typeable、Data（是的，使用SYB）、Traversable、Foldable、Functor、Pointed、Applicative、Monad 等的实例（？ ）。在这种情况下，我们有必要的签名以及额外的属性（例如，monad 定律，虽然这些属性不能用 Haskell 表示，但它们可以用具有依赖类型的语言表示）。有一些有趣的结构：

http://ulissesaraujo.wordpress.com/2007/12/19/catamorphisms-in-haskell

它显示了可以为列表 ADT 做什么。

于 2012-04-18T10:08:41.427 回答
3

这个问题实际上相当深，我不确定答案，如果你问的是 Haskell 类型的全部荣耀，包括类型系列、GADT 等。

您要问的是程序是否可以通过显示这样的值来自动证明存在任意类型（包含值）。一个叫做 Curry-Howard Correspondence 的原则说，类型可以被解释为数学命题，如果命题是建设性可证明的，则类型是可居住的。所以你问是否有一个程序可以证明某一类命题是定理。在像 Agda 这样的语言中，类型系统足够强大，可以表达任意数学命题，证明任意命题是哥德尔不完备定理不可判定的。另一方面，如果你下降到（比如说）纯 Hindley-Milner，你会得到一个更弱且（我认为）可判定的系统。对于 Haskell 98，我不确定，因为类型类应该能够等同于 GADT。

对于 GADT，我不知道它是否可以确定，但也许这里的一些知识渊博的人会马上知道。例如，可以将给定图灵机的停机问题编码为 GADT，因此如果机器停机，则存在该类型的值。在那种情况下，可居住性显然是无法确定的。但是，也许这样的编码不太可能，即使是类型族。我目前在这个主题上还不够流利，因此无论哪种方式对我来说都是显而易见的，尽管正如我所说，也许这里的其他人知道答案。

（更新：）哦，我对您的问题有一个更简单的解释：您可能会问是否每个 Haskell 类型都有人居住。答案显然不是。考虑多态类型

a -> b

There is no function with that signature (not counting something like unsafeCoerce, which makes the type system inconsistent).

于 2012-04-18T17:09:59.207 回答