On Sunday 29 July 2007, Jim Apple wrote:
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
Ah, great. That was the first trick I'd missed.
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.
This turns out not to be needed if you describe what nnf is in terms of those parameterised datatypes above. You can re-use the same datatype! I had to move the nnf function into a class to get it to compile, which makes the code more verbose, but appart from that I'm quite pleased with the result.
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.
Yeah, sorry about that. It was a late-at-night thing. I've pasted in my (compiling and working) code below, for anyone that's interested. I think I like GADTs quite a lot :) Pitty I can't get deriving clauses to work with them... Thanks Matthew data Named data Equal a b data Conjunction a b data Disjunction a b data Negation a data Existential a data Universal a data Top data Bottom data Concept t where CNamed :: String -> Concept Named CEqual :: Concept a -> Concept b -> Concept (Equal a b) CConjunction :: Concept a -> Concept b -> Concept (Conjunction a b) CDisjunction :: Concept a -> Concept b -> Concept (Disjunction a b) CNegation :: Concept a -> Concept (Negation a) CExistential :: Role Named -> Concept a -> Concept (Existential a) CUniversal :: Role Named -> Concept a -> Concept (Universal a) CTop :: Concept Top CBottom :: Concept Bottom data Role t where RNamed :: String -> Role Named class InNNF nnf instance InNNF Named instance InNNF Top instance InNNF Bottom instance InNNF (Negation Named) instance InNNF (Negation Top) instance InNNF (Negation Bottom) instance (InNNF a, InNNF b) => InNNF (Equal a b) instance (InNNF a, InNNF b) => InNNF (Conjunction a b) instance (InNNF a, InNNF b) => InNNF (Disjunction a b) instance (InNNF a) => InNNF (Existential a) instance (InNNF a) => InNNF (Universal a) class ( InNNF u ) => ToNNF t u | t -> u where nnf :: Concept t -> Concept u instance ToNNF Named Named where nnf = id instance (ToNNF a c, ToNNF b d) => ToNNF (Equal a b) (Equal c d) where nnf (CEqual lhs rhs) = CEqual (nnf lhs) (nnf rhs) instance (ToNNF a c, ToNNF b d) => ToNNF (Conjunction a b) (Conjunction c d) where nnf (CConjunction lhs rhs) = CConjunction (nnf lhs) (nnf rhs) instance (ToNNF a c, ToNNF b d) => ToNNF (Disjunction a b) (Disjunction c d) where nnf (CDisjunction lhs rhs) = CDisjunction (nnf lhs) (nnf rhs) instance (ToNNF a b) => ToNNF (Existential a) (Existential b) where nnf (CExistential r c) = CExistential r (nnf c) instance (ToNNF a b) => ToNNF (Universal a) (Universal b) where nnf (CUniversal r c) = CUniversal r (nnf c) instance ToNNF (Negation Named) (Negation Named) where nnf = id instance (ToNNF (Negation a) c, ToNNF (Negation b) d) => ToNNF (Negation (Equal a b)) (Equal c d) where nnf (CNegation (CEqual lhs rhs)) = CEqual (nnf $ CNegation lhs) (nnf $ CNegation rhs) instance (ToNNF (Negation a) c, ToNNF (Negation b) d) => ToNNF (Negation (Conjunction a b)) (Disjunction c d) where nnf (CNegation (CConjunction lhs rhs)) = CDisjunction (nnf $ CNegation lhs) (nnf $ CNegation rhs) instance (ToNNF (Negation a) c, ToNNF (Negation b) d) => ToNNF (Negation (Disjunction a b)) (Conjunction c d) where nnf (CNegation (CDisjunction lhs rhs)) = CConjunction (nnf $ CNegation lhs) (nnf $ CNegation rhs) instance (ToNNF a b) => ToNNF (Negation (Negation a)) b where nnf (CNegation (CNegation c)) = nnf c instance(ToNNF (Negation a) b) => ToNNF (Negation (Existential a)) (Universal b) where nnf (CNegation (CExistential r c)) = CUniversal r (nnf $ CNegation c) instance (ToNNF (Negation a) b) => ToNNF (Negation (Universal a)) (Existential b) where nnf (CNegation (CUniversal r c)) = CExistential r (nnf $ CNegation c) instance ToNNF (Negation Top) (Negation Top) where nnf (CNegation CTop) = CNegation CTop instance ToNNF (Negation Bottom) (Negation Bottom) where nnf (CNegation CBottom) = CNegation CBottom