[Haskell-cafe] Using GADTs

[Jim Apple]

> {-# 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