调试：无法将预期类型“GHC.Types.Bool”与实际类型“Bool”匹配

问题描述

我正在尝试解决以下 Haskell 练习：

定义函数exists::(N-> Bool)-> N->Bool，它接收一个谓词p和一个自然n，如果在O和n之间有任何数p为真，则返回True。 示例：

exists pair three = True
exists isGreaterThanZero O = False

这段代码在我的exists函数之前：

{-#LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
{-# OPTIONS_GHC -fno-warn-missing-methods #-}

module Naturales where

import Prelude(Show)

data Bool where {   False :: Bool; 
                    True :: Bool
                } deriving Show

{- Data Type of Natural Numbers -}
data N where { O :: N ; 
               S :: N -> N 
            } deriving Show
    
    zero:: N
    zero= O
    
    one:: N
    one = S O
    
    two :: N
    two = S one 
    
    three :: N
    three = S two 
    
    four :: N
    four = S three
    ...

这就是我对所请求的函数进行编程的方式，调用exists但是当我尝试编译.hs代码时 说

exists:: (N->Bool)->N->Bool
exists = \p -> \x -> case x of {
            O -> p O;
            (S y) -> if p (S y) then True else existe p y; {- Line 288 -}
        }


    • Couldn't match expected type ‘GHC.Types.Bool’
                  with actual type ‘Bool’
      NB: ‘Bool’ is defined at EstudiandoRecursion.hs:(9,1)-(11,47)
          ‘GHC.Types.Bool’
            is defined in ‘GHC.Types’ in package ‘ghc-prim-0.5.3’
    • In the expression: p (S y)
      In the expression: if p (S y) then True else existe p y
      In a case alternative:
          (S y) -> if p (S y) then True else existe p y
    |
288 |                         (S y) -> if p (S y) then True else existe p y;     | 

我认为我的函数的逻辑存在它是正确的，但也许我在编写代码时犯了语法错误。

解决方法

您重新定义了标准的 Bool 类型。 Haskell 不知道您自己重新定义的类型实际上与标准类型相同，因此它将它们视为两种不同的类型：Bool（您的）和 GHC.Types.Bool（标准的）。>

if cond then t else e 表达式仅适用于标准 Bool 类型，不适用于您的自定义类型。因此，您不能在

中使用它

if p (S y) then True else exists p y

因为 p (S y) 返回您自己的自定义 Bool。考虑一下

case p (S y) of
   True  -> True
   False -> exists p y

与 if 不同，它应该可以工作，从您的新类型中选择正确的 True 和 False 构造函数。如果您喜欢大括号和分号，可以使用 case .. of { .. ; ... }。

,

您正在使用 if … then … else … 表达式。这要求条件的类型为 Bool，这是 builtin Bool，因此定义您自己的 Bool 类型是不够的。

然而，在您的 case … of …/True 数据构造函数上使用 False 子句并因此进行模式匹配就足够了：

exists:: (N -> Bool) -> N -> Bool
exists = \p -> \x -> case x of {
            O -> p O;
            (S y) -> case p (S y) of
                True -> True
                _ -> exists p y
        }