【问题标题】:Church Numerals in haskell哈斯克尔的教堂数​​字
【发布时间】:2011-06-24 02:37:04
【问题描述】:

我正在尝试使用定义在 haskell 中打印教堂数字:

0 := λfx.x
1 := λfx.f x

Haskell 代码:

c0 = \f x -> x
c1 = \f x -> f x

当我在 haskell 控制台中输入它时,我收到一个错误提示

    test> c1

    <interactive>:1:0:
    No instance for (Show ((t -> t1) -> t -> t1))
      arising from a use of `print' at <interactive>:1:0-1
    Possible fix:
      add an instance declaration for (Show ((t -> t1) -> t -> t1))
    In a stmt of an interactive GHCi command: print it

我无法准确弄清楚错误的含义。

谢谢!

【问题讨论】:

    标签: haskell lambda-calculus


    【解决方案1】:

    这里的问题是,默认情况下,不能在 Haskell 中打印值。 print 函数和 GHCi REPL 等使用的默认打印方式是 show 函数,由类型类 Show 定义。

    然后,您得到的错误是通知您已评估了一个类型的表达式,该类型没有定义 Show 的实例。模数一些废话,这就是错误消息的全部内容:

    No instance for (Show ((t -> t1) -> t -> t1))
    

    ((t -&gt; t1) -&gt; t -&gt; t1) 类型是为您评估的表达式推断的。这是 Church 数字 1 的有效类型,但 Church 数字的“正确”类型实际上应该是 (a -&gt; a) -&gt; a -&gt; a

      arising from a use of `print' at <interactive>:1:0-1
    

    它隐式使用print 函数来显示值。通常这会告诉您在程序的哪个位置发现了错误,但在这种情况下,它会显示&lt;interactive&gt;:1:0-1,因为错误是由 REPL 中的表达式引起的。

    Possible fix:
      add an instance declaration for (Show ((t -> t1) -> t -> t1))
    

    这只是建议您可以通过定义它所期望的实例来修复错误。


    现在,您可能想实际打印您的 Church 数字,而不仅仅是知道为什么不能。不幸的是,这并不像添加它要求的实例那么简单:如果您为(a -&gt; a) -&gt; a -&gt; a 编写一个实例,Haskell 会将其解释为任何特定a 的实例,而正确的解释Church 数字的 of 是一个多态函数,适用于任意 a

    换句话说,你希望你的show 函数是这样的:

    showChurch n = show $ n (+1) 0
    

    如果你真的想要,你可以像这样实现 Show 实例:

    instance (Show a, Num a) => Show ((a -> a) -> a -> a) where
        show n = show $ n (+1) 0
    

    并将{-#LANGUAGE FlexibleInstances#-} 添加到文件的第一行。或者您可以实现类似的东西将它们转换为常规数字

    > churchToInt c1
    1
    > showChurch c1
    "1"
    

    等等

    【讨论】:

    • 感谢对错误消息的详细剖析。现在对我来说更有意义了。我正在努力更好地理解抛出的错误:)
    • @RBK:不客气。 :] 一旦您知道所使用的基本结构/行话,GHC 的错误消息通常非常简单且很有帮助,但我不知道有任何独立的学习指南。在 IRC 和诸如此类的人的帮助下,我主要是自己想出来的。
    • 我尝试实现这个并得到一个错误,“Show ((a -&gt; a) -&gt; a -&gt; a) 的非法实例声明(所有实例类型必须是形式......不同的类型变量”。作为 Haskell 的新手,我是不知道如何修改。希望在接下来的几个小时内有一个 lambda 演算的操场,而不必先学习所有 Haskell。帮助?
    【解决方案2】:

    编辑:剧透警报,如评论中所述

    或者,您可以使用 Church 数字类型,如下所示:

    data Church x = Church ((x -> x) -> x -> x)
    
    zero :: Church x
    zero = Church (\f x -> x)
    
    -- Hack to not clash with the standard succ
    succ_ :: Church x -> Church x
    succ_ (Church n) = Church (\f x -> (f (n f x)))
    
    instance (Num x) => Show (Church x) where
      show (Church f) = show $ f (1 +) 0
    

    【讨论】:

    • 警告:如果您想弄清楚如何自己实现教堂数字,请不要阅读此答案!它把一切都给了!
    • 不幸的是,这仍然不太理想——它适用于简单的表达式,但在更复杂的用途中,类型变量 x 可以与你不想要的东西统一。你真正想要的是data Church = Church (forall x. (x -&gt; x) -&gt; x -&gt; x)
    • 我一直在考虑那些线路,但因为我自己对 2 级类型不太了解,所以决定放弃。
    • 谢谢大家。我需要更多地阅读关于类型类的主题。将使用 SCombinator 的解决方案作为参考,并尝试自己做。
    • 如果有帮助,您可以将 forall a. (...) 解读为 System F 的大写 lambda 抽象,即我们可以将 succ 定义为 λn:(Λa. (a → a) → a → a). Λa. λf:(a → a). λx:a. f (n a f x)) 之类的东西。如果您对 λ 演算比花哨的类型系统更熟悉,那可能更容易理解。
    猜你喜欢
    • 2012-04-02
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    相关资源
    最近更新 更多