Haskell - Implementing First Order Logic Expressions

Question

I am trying to implement FOL using Haskell. First order logic can be in the form of propositions connected together with connectives like And and Or. There is also quantifiers that have a limited scope in the expression.

What I did so far is:

import Data.List

data Prop 
    = Not Prop
    | Prop And Prop
    | Prop Or Prop
    | Prop Impl Prop
    | Prop Equiv Prop
    | ForAll String Prop
    | Exists String Prop
    deriving (Eq, Ord)

But I am getting this error:

 Multiple declarations of ‘Prop’

Answer 1

When you declare an algebraic data type, the right-hand side of the declaration is a "list" of possible constructors for this type. However, the constructors are just functions, meaning that they are used in prefix notation. You try to use the e.g. And constructor in an infix way which does not work.

The following code works well:

data Prop
    = Not Prop
    | And Prop Prop
    | Or Prop Prop
    | Impl Prop Prop
    | Equiv Prop Prop
    | ForAll String Prop
    | Exists String Prop
    deriving (Eq, Ord)

However, you can define functions mimicking the constructors, e.g. --

propAnd :: Prop -> Prop -> Prop
propAnd a b = And a b

and use these in an infix way using the backquotes: a `propAnd` b. As suggested in the comments, this is not necessary as And can already be used in the infix way: a `And` b

Another option is to define the constructors themselves in an infix way:

data Prop
    = Not Prop
    | Prop `And` Prop
    | Prop `Or` Prop
    | Prop `Impl` Prop
    | Prop `Equiv` Prop
    | ForAll String Prop
    | Exists String Prop
    deriving (Eq, Ord)

and then both a `And` b and And a b work.

Note: your data type is infinite since all the constructors take one or more Props. I think you should also include some "atomic" constructors.