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以及Propositional_expression类型的构造函数Logical_value混合在一起。事实上，您始终使用相同的名称，掩盖了相当多的区别和问题。首先，Logical_value情况下的Propositional_expression实际上并不包含一个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