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