> {-# OPTIONS -fglasgow-exts #-} > > module NNF where The way I would do this would be to encode as much of the value as I cared to in the constructors for concepts, rather than just encoding the top-level constructor.
> data Named > data Equal a b > data Negation a > data Top > > data Concept t where > CNamed :: String -> Concept Named > CEqual :: Concept a -> Concept b -> Concept (Equal a b) > CNegation :: Concept a -> Concept (Negation a) > CTop :: Concept Top Then, I could form a datatype that does not contain a Concept, but merely certifies that all Concepts of a certain type are in NNF. > data NNF x where > NNFnamed :: NNF Named > NNFequal :: NNF a -> NNF b -> NNF (Equal a b) > NNFnegateName :: NNF (Negation Named) > NNFnegateTop :: NNF (Negation Top) Now I have a generic constructor for some Concept of NNF, value unknown, that encodes a concept and a proof of its NNF-ness. > data NNFConcept = forall t . NNFConcept (Concept t) (NNF t) And I take a Concept with some value, transform its value somehow, and get an NNF concept. > nnf :: Concept t -> NNFConcept > nnf (CNamed x) = NNFConcept (CNamed x) NNFnamed > nnf (CEqual x y) = > case (nnf x, nnf y) of > (NNFConcept a a', NNFConcept b b') -> > NNFConcept (CEqual a b) (NNFequal a' b') > nnf (CNegation (CEqual x y)) = > case (nnf (CNegation x), nnf (CNegation y)) of > (NNFConcept a a', NNFConcept b b') -> > NNFConcept (CEqual a b) (NNFequal a' b') The above function is not total, even for the limited subset of Concepts discussed above. By the way, the code you included last time did not compile. I think you'll probably get a quicker response than my lazy two-day turnaround if you make sure to run your posted code through Your Favorite Compiler first. Hope this helps, Jim _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe