I'm not familiar with modal logic, but if modalities stack, you might be able to do something like this.<br><br>-- Garrett Mitchener<br><br>{-# OPTIONS_GHC -fglasgow-exts #-}<br><br>module Test where<br><br>data L a<br>
= F | T | Atom Int<br> | Neg (L a) | And (L a) (L a) | Or (L a) (L a)<br> | M (L a) -- the modality a is a phantom type for this<br> deriving (Read, Show, Eq)<br><br>-- Actually I never use the data constructors, just the types, so you could leave them out.
<br>data NullModality = NullModality<br> deriving (Read, Show, Eq)<br> <br>data KModality a = KModality a<br> deriving (Read, Show, Eq)<br><br>data KDModality a = KDModality a
<br> deriving (Read, Show, Eq)<br><br>-- Need multi-parameter type classes for this:<br>class StripModality m1 m2 | m1 -> m2 where<br> stripModality :: L m1 -> L m2<br> stripModality F = F<br> stripModality T = T
<br> stripModality (Atom n) = Atom n<br> stripModality (Neg p) = Neg (stripModality p)<br> stripModality (And p q) = And (stripModality p) (stripModality q)<br> stripModality (Or p q) = And (stripModality p) (stripModality q)
<br> stripModality (M p) = M (stripModality p)<br><br>instance StripModality NullModality NullModality<br><br>instance StripModality (KModality m) m<br><br>instance StripModality (KDModality m) m<br><br>expr :: L (KDModality (KModality NullModality)) -- for modality KD on top of K
<br>expr = And (Atom 1) (M (Atom 2))<br><br>-- This is kind of dumb but it shows something this can do<br><br>listMAtoms :: StripModality m1 m2 => L m1 -> [L m2]<br>listMAtoms p@(Atom n) = [stripModality p]<br>listMAtoms (Neg p) = listMAtoms p
<br>listMAtoms (And p q) = listMAtoms p ++ listMAtoms q<br>listMAtoms (Or p q) = listMAtoms p ++ listMAtoms q<br>listMAtoms (M p) = listMAtoms p<br>listMAtoms _ = []<br>