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
{-# 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
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
participants (2)
-
Jim Apple -
Matthew Pocock