Mismatched types with propositional logic implementation in haskell

Question

I'm trying to implement propositional logic in haskell with the following code:

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

I'm having the following compiling error:

[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.

I think my syntax is correct: if a propositional_expression can be a Logical_value I expected Haskell matches it correctly but it must be something I'm missing. Can anyone help me?

Thanks

Answer 1

Your problem is that you are mixing up Logical_value, the type with constructors TRUE, FALSE and INDETERMINATE, and Logical_value, the constructor of the Propositional_expression type. The fact that you are using the same names throughout is obscuring quite a few distinctions and issues. For one, the Logical_value case of Propositional_expression doesn't actually contain a Logical_value, as it is just an atomic value. What follows is an adjustment of your types so that they have clearer names and behave in the way you want them to:

-- 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

And here is how interpretation would look like. Note how the constructors (ValueExpr, SymbolExpr, etc.) are used to pick the case that each equation handles. That is what lies behind your type error -- TRUE, FALSE and INDETERMINATE are not constructors of PropositionalExpression, neither in your original code nor in my modified version (by the way, you were right in suspecting it wasn't a syntax error: the syntax in your original code was legal, but it didn't do what you expected, leading to a type error).

-- 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