Haskell中命题逻辑实现的类型不匹配

Question

我正在尝试使用以下代码在 haskell 中实现命题逻辑：

module Propositional_Logic where

--Syntax
--It will be considered three logical values.
data Logical_value = TRUE | FALSE | INDETERMINATE deriving (Show, Eq)
--A propositional symbol (variable) is a string.
type Propositional_symbol = String 
--Four basics logicals connectives.
data Propositional_connective = And 
                              | Or 
                              | Impl 
                              | Dimpl 
                              deriving (Show, Eq)
--A well-formed formula (propositional expression) can be a logical value, a propositional symbol, the negation of a well-formed formula, two well-formed formulas connected by a logical connective and the conjunction or disjunction of well-formed formulas.
data Propositional_expression = Logical_value
                              | Propositional_symbol
                              | Neg Propositional_expression
                              | Propositional_expression Propositional_connective Propositional_expression
                              | Propositional_connective [Propositional_expression] -- Semantic will throw error if connective is not And or Or.
                              deriving (Show, Eq)

--Semantic
--Type to assign logical values to propositional symbols.
type Interpretation = Propositional_symbol -> Logical_value

interpretationInit :: Interpretation
interpretationInit _ = INDETERMINATE

--Function to add interpretations for basic propositional symbols.
update :: Interpretation -> Interpretation -> Interpretation
update i1 i2 = (\x -> if i2 x == INDETERMINATE then i2 x else i1 x)

--Function to obtain the logical value from a propositional expression and the interpretation from basic propositional variables.
interpretation :: Propositional_expression -> Interpretation -> Logical_value
--Logical Values
interpretation (TRUE) i = TRUE
interpretation (FALSE) i = FALSE
interpretation (INDETERMINATE) i = INDETERMINATE

我遇到以下编译错误：

[1 of 1] Compiling Propositional_Logic ( propositional_logic.hs, interpreted )

propositional_logic.hs:36:21:
Couldn't match expected type ‘Propositional_expression’
            with actual type ‘Logical_value’
In the pattern: TRUE
In an equation for ‘interpretation’: interpretation (TRUE) i = TRUE

propositional_logic.hs:37:21:
Couldn't match expected type ‘Propositional_expression’
            with actual type ‘Logical_value’
In the pattern: FALSE
In an equation for ‘interpretation’:
    interpretation (FALSE) i = FALSE

propositional_logic.hs:38:21:
Couldn't match expected type ‘Propositional_expression’
            with actual type ‘Logical_value’
In the pattern: INDETERMINATE
In an equation for ‘interpretation’:
    interpretation (INDETERMINATE) i = INDETERMINATE
Failed, modules loaded: none.

我认为我的语法是正确的：如果一个propositional_expression 可以是一个Logical_value，我希望Haskell 可以正确匹配它，但它一定是我缺少的东西。谁能帮帮我？

谢谢

Answer 1

您的问题是您将Logical_value（类型）与构造函数TRUE、FALSE 和INDETERMINATE 以及Logical_value（构造函数）混在一起 Propositional_expression 类型的 em>。您自始至终使用相同的名称这一事实掩盖了很多区别和问题。一方面，Propositional_expression 的Logical_value 案例实际上并不包含Logical_value，因为它只是一个原子值。接下来是对您的类型进行调整，以便它们具有更清晰的名称并按照您希望的方式运行：

-- I'm changing the names to CamelCase out of habit -- feel free not to. 

-- It will be considered three logical values.
data LogicalValue = TRUE | FALSE | INDETERMINATE deriving (Show, Eq)

-- A propositional symbol (variable) is a string.
type PropositionalSymbol = String 

-- Four basics logicals connectives.
data PropositionalConnective
    = And 
    | Or 
    | Impl 
    | Dimpl 
    deriving (Show, Eq)

-- A well-formed formula (propositional expression) can be a logical
-- value, a propositional symbol, the negation of a well-formed formula,
-- two well-formed formulas connected by a logical connective and the 
-- conjunction or disjunction of well-formed formulas.
data PropositionalExpression 
    = ValueExpr LogicalValue
    | SymbolExpr PropositionalSymbol
    | NegExpr PropositionalExpression
    | ConnectiveExpr
        PropositionalExpression PropositionalConnective PropositionalExpression
    | ListExpr PropositionalConnective [PropositionalExpression] 
        -- Semantic will throw error if connective is not And or Or.
    deriving (Show, Eq)

-- Semantic
-- Type to assign logical values to propositional symbols.
type Interpretation = PropositionalSymbol -> LogicalValue

这就是interpretation 的样子。请注意构造函数（ValueExpr、SymbolExpr 等）如何用于选择每个方程处理的情况。这就是您的类型错误背后的原因——TRUE、FALSE 和 INDETERMINATE 不是PropositionalExpression 的构造函数，无论是在您的原始代码中还是在我的修改版本中（顺便说一句，你怀疑它是对的不是语法错误：原始代码中的语法是合法的，但它没有达到您的预期，导致类型错误）。

-- Function to obtain the logical value from a propositional expression
-- and the interpretation from basic propositional variables.
interpretation :: PropositionalExpression -> Interpretation -> LogicalValue
-- Logical Values
-- All three cases here can be subsumed into one.
-- _ simply means "ignore this argument".
interpretation (ValueExpr x) _ = x
-- And so forth for the other PropositionalExpression cases