Hi, I'm trying to get to grips with GADTs, and my first attempt was to convert a simple logic language into negative normal form, while attempting to push the knowledge about what consitutes negative normal form into the types. My code is below. I'm not entirely happy with it, and would appreciate any feedback. The rules are that in nnf, only named concepts, the concept Top and the concept Bottom can be negated. So, I've added three NNFNegation_* constructors capturing these legal cases. Is there a way to use one constructor, that is allowed to 'range over' these three cases and none of the others? I've ended up producing two data types, one for the general form and one for the nnf. Actually, the constraint on what constitutes nnf is fairly obvious - no complex terms are negated. Is there a way to use just the one data type but to describe two levels of constraints - one for the general case, and one for the nnf case? Or is the whole point that you capture each set of constraints in a different data type? Thanks, Matthe data Named data Equal data Conjunction data Disjunction data Negation data Existential data Universal data Top data Bottom data Concept t where CNamed :: String -> Concept Named CEqual :: Concept a -> Concept b -> Concept Equal CConjunction :: Concept a -> Concept b -> Concept Conjunction CDisjunction :: Concept a -> Concept b -> Concept Disjunction CNegation :: Concept a -> Concept Negation CExistential :: Role Named -> Concept Existential CUniversal :: Role Named -> Concept Universal CTop :: Concept Top CBottom :: Concept Bottom data NNFConcept t where NNFCNamed :: String -> NNFConcept Named NNFCEqual :: NNFConcept a -> NNFConcept b -> NNFConcept Equal NNFCConjunction :: NNFConcept a -> NNFConcept b -> NNFConcept Conjunction NNFCDisjunction :: NNFConcept a -> NNFConcept b -> NNFConcept Disjunction NNFCExistential :: Role Named -> NNFConcept Existential NNFCUniversal :: Role Named -> NNFConcept Universal NNFCTop :: NNFConcept Top NNFCBottom :: NNFConcept Bottom NNFCNegation_N :: NNFConcept Named -> Concept Negation NNFCNegation_T :: NNFConcept Top -> Concept Negation NNFCNegation_B :: NNFConcept Bottom -> Concept Negation data Role t where RNamed :: String -> RNamed Named -- terms not prefixed with a negation are already in nnf nnf :: Concept t -> NNFConcept u nnf CNamed name = NNFCNamed name nnf CEqual lhs rhs = NNFConcept (nnf lhs) (nnf rhs) nnf CConjunction lhs rhs = NNFCConjunction (nnf lhs) (nnf rhs) nnf CDijunction lhs rhs = NNFCDisjunction (nnf lhs) (nnf rhs) nnf CExistential r c = NNFCExistential r (nnf c) nnf CUniversal r c = NNFCUniversal r (nnf c) -- if negated, we must look at the term and then do The Right Thing(tm) nnf CNegation (CNamed name) = NNFCNegation_N NNFCNamed name nnf CNegation (CEqual lhs rhs) = NNFCEqual (nnf $ CNegation lhs) (nnf $ CNegation rhs) nnf CNegation (CConjunction lhs rhs) = NNFCDisjunction (nnf $ CNegation lhs) (nnf $ CNegation rhs) nnf CNegation (CDisjunction lhs rhs) = NNFCConjunction (nnf $ CNegation lhs) (nnf $ CNegation rhs) nnf CNegation (CNegation c) = nnf c nnf CNegation (CExistential r c) = NNFCUniversal r (nnf $ CNegation c) nnf CNegation (CUniveral r c) = NNFCExistential r (nnf $ CNegation c) nnf CNegation CTop = NNFCNegation_T NNFCTop nnf CNegation CBottom = NNFCNegation_B NNFCBottom