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’
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:
However, you can define functions mimicking the constructors, e.g. --and use these in an infix way using the backquotes:
a `propAnd` b
. As suggested in the comments, this is not necessary asAnd
can already be used in the infix way:a `And` b
Another option is to define the constructors themselves in an infix way:
and then both
a `And` b
andAnd a b
work.Note: your data type is infinite since all the constructors take one or more
Prop
s. I think you should also include some "atomic" constructors.