[Haskell-cafe] Using GADTs
Matthew Pocock
matthew.pocock at ncl.ac.uk
Sun Jul 29 17:31:02 EDT 2007
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
More information about the Haskell-Cafe
mailing list