{-# 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