[Haskell-cafe] Using GADTs

[Matthew Pocock]

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