[Haskell-cafe] Using GADTs
Jim Apple
jbapple+haskell-cafe at gmail.com
Sun Jul 29 11:27:18 EDT 2007
> {-# 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
More information about the Haskell-Cafe
mailing list