Is there such as thing as "type extensions" in Haskell?

Question

I don't actually think that the term "type extension" officially means what I want, but it's the only term I could think of.

I have a polymorphic Haskell type to represent terms in a propositional logic:

 data PropLogic a = Prop a | Tautology | Contradiction | And (PropLogic a) (PropLogic a)
                | Or (PropLogic a) (PropLogic a) | Implies (PropLogic a) (PropLogic a)
                | Not (PropLogic a)
     deriving (Eq,Show)

The issue is, I also want a similar polymorphic type for propositional logic with quantification operators:

data PropQuantifiedLogic a = Prop a | Tautology | Contradiction | And (PropQuantifiedLogic a) (PropQuantifiedLogic a)
                | Or (PropQuantifiedLogic a) (PropQuantifiedLogic a) | Implies (PropQuantifiedLogic a) (PropQuantifiedLogic a)
                | Not (PropQuantifiedLogic a) | Forall (PropQuantifiedLogic a)
                | Exists (PropQuantifiedLogic a)
     deriving (Eq,Show)

Now, I could just add a prefix to the name of each value constructor where both PropLogic and PropQuantifiedLogic have conflicting names, but the point is that I want to create many types like this which will have a lot of conflicting value constructurs: A modal logic type, temporal logic type, etc... and creating new prefixes for each one wold get ugly quickly.

What I really want to do is something like:

extendtype PropQuantifiedLogic a = PropLogic a | Exists (PropQuantifiedLogic a)
                                 | Forall (PropQuantifiedLogic a)

which would be equivalent to the first definition of PropQuantifiedLogic, and would type-check.

Is it possible to do something like this in Haskell? If not, how should I handle this situation? This "extension type" concept would introduce some ambiguity, but I believe that just means type inference wouldn't work when using types like this, and I can deal with that.

Answer 1

You could always implement this as

 data PropFrame a b = OrF b b | AndF b b ... | Prop a | Top

And then

type Prop a = Fix (PropFrame a)

Then you can add a new primitive

data QualifiedF a b = All (b -> b) | Exists (b -> b) | LiftProp (PropFrame a b)
type Qualified a = Fix (QualifiedF a)

This is a littler uglier, but can be sugared up with -XPatternSynonyms. The main idea here is to factor out the problematic recursive case into an explicit parameter and use Fix to regain the recursion.

Example of use

qand :: Qualified a -> Qualified a -> Qualified a
qand l r = Fix (LiftProp (AndF l r))

orOrAll :: (Qualified a -> Qualified a) -> Qualified a
orOrAll f = Fix (All f) `qand` Fix (Exists f)