[Haskell-cafe] Using GADTs

[Matthew Pocock]

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