[Haskell] Generic combination of generic types

[Rob Myers]

Hi there,

This is a question about combining data types in a generic way.

I am using Haskell to write a first implementation of a new generic 
algorithm to decide a fairly large class of modal logics. Type classes 
provide an excellent way to generically define a modal language. In 
particular you only need to define the data type of the modal operator 
(e.g. it could be indexed by rationals) and also a special matching 
rule, which is used in the proof checker.

However I also want to combine different modal languages to create new 
ones *in a generic fashion*. The "modal language" I'm talking about is 
just a data-type with a single type variable:

   data L a
       = F | T | Atom Int
           | Neg (L a) | And (L a) (L a) | Or (L a) (L a)
           | M a (L a)
       deriving (Eq,Show)

   // convention: clause([positive literals,negative literals])
   newtype Clause a = Clause ([L a],[L a]) deriving (Eq,Show)

with a type class like this:

   class (Eq a) => Logic a where
       match :: Clause a -> [[L a]]

and instances like:

   data K = K deriving (Eq,Show)
   instance Logic K where
       match (Clause (pls,nls)) = ...

   data G = G Int deriving (Eq,Show)
   instance Logic G where
       match (Clause(pls,nls)) = ...

   data KD = KD deriving (Eq,Show)
   instance Logic KD where
       match (Clause (pl,nl)) = ...

I have various such instances of logics and I want to combine them in 
particular ways. For example I might want to interlace three instances 
in a new language such as:

   data L1 = F1 | T1 | Atom1 Int | Neg1 L1 | And1 L1 L1 | Or1 L1 L1 |
   MCP L2 L3 deriving (Eq,Show)
   data L2 = F2 | T2 | Atom2 Int | Neg2 L2 | And2 L2 L2 | Or2 L2 L2 |
   MK L1 deriving (Eq,Show)
   data L3 = F3 | T3 | Atom3 Int | Neg3 L3 | And3 L3 L3 | Or3 L3 L3 |
   MKD L1 deriving (Eq,Show)

or

   data L1 = F1 | T1 | Atom1 Int | Neg1 L1 | And1 L1 L1 | Or1 L1 L1 |
   MK L2 deriving (Eq,Show)
   data L2 = F2 | T2 | Atom2 Int | Neg2 L2 | And2 L2 L2 | Or2 L2 L2 |
   MKD L1 deriving (Eq,Show)

... the idea being that a different language(s) appear after the 
modalities (MCP, MK, MKD above).


Put simply I want to take some data types and construct a new 
(specifically ordered) data type(s) defined in terms of these. I also 
want to be able to define recursive functions over this language, with 
which I'm having a problem (see below).


I originally tried this by defining a language:

   data L a = F | T | Atom Int | Neg (L a) | And (L a) (L a) | Or (L a)
   (L a) | M a deriving (Eq,Show)

Note the last term is "M a" not "M a (L a)" as in the first type. Using 
this 'a' I could write terms like: M (K,And F (M (KD,F))), i.e. use 
tupling to define in the first component the data type of the modality 
and in the second component (and third if considering binary modal 
operators) defining what comes after the modality.

I found with this approach I was able to match these types e.g. note the 
"(K,a)"

   data K = K deriving (Eq,Show)
   instance Logic (K,a) where
       match (Clause (pl,nl)) =


However, crucially, I cannot seem to define recursive functions because 
on each recursive step I am changing the type of terms considered. The 
underlying algorithm requires me to strip off a layer of modalities 
(e.g. M (K,F) goes to F) at each step. For example if I have M (K,M 
(KD,F)) this has type: L (K,L (KD,L a)), if I pass to the subterm M 
(KD,F), then this has type: L (KD,L a). Thus Haskell could not resolve 
this type ('unification would produce infinite data type'). However this 
method seems very attractive because it only needs one data type to 
define many different languages.

I've tried alternate approaches, for example explicitly defining the 
interlaced language, such as:

   data L1 = F1 | T1 | Atom1 Int | Neg1 L1 | And1 L1 L1 | Or1 L1 L1 |
   MCP L2 L3 deriving (Eq,Show)
   data L2 = F2 | T2 | Atom2 Int | Neg2 L2 | And2 L2 L2 | Or2 L2 L2 |
   MK L1 deriving (Eq,Show)
   data L3 = F3 | T3 | Atom3 Int | Neg3 L3 | And3 L3 L3 | Or3 L3 L3 |
   MKD L1 deriving (Eq,Show)

However this becomes messy because I then need to define all of my 
operations (e.g. find conjunctive normal form) on these new 
constructors. It seems that I need to use the actual constructor to 
pattern match... I can't use some ADT functions. I've also tried the 
first method above with 2 type variables, with the same problems 
(unification of infinite data type).


Does anyone have any ideas? Frankly I'd be impressed if someone even 
takes the time to read though this.

Thanks,

Rob