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