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
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
