Using existential types

[oleg at pobox.com]

> data Datatype ex = forall vt . Datatype (DatatypeVal ex vt)

In practice one rarely would write 
	forall vt. Datatype (DatatypeVal ex vt)
unless he is writing something like the ST monad. 
You can only pass vt to functions with the signature
	forall vt. vt -> C1 vt C2 C3 ...

where C1, C2, C3 do not depend on vt in any way. For example,
functions like 'id', (\vt x -> (vt,x)), (\x -> 1), etc. As you can
notice these functions don't do anything with their vt argument. They
merely pass it through or disregard. You can't do anything with the
unconstrainedly quantified argument! This fact is precisely why the
quantified arguments are useful (or useless). Therefore, when you
quantify a value, you typically want to impose a constraint

	forall vt. (C vt) => Datatype (DatatypeVal ex vt)

At the very least the class C should be 'Typable', which lets you cast 
values of quantified types into those of the regular type. The messages

	http://www.mail-archive.com/haskell@haskell.org/msg13114.html
	http://www.haskell.org/pipermail/haskell/2003-February/011288.html
	http://www.haskell.org/pipermail/haskell/2003-February/011293.html

talk more about uses and uselessness of existential quantification
and types. See also a message 
	http://www.mail-archive.com/haskell@haskell.org/msg13131.html
that discusses safe casts. Incidentally, your typeMap looks exactly
like an injection-projection pair mentioned in that message.

Given one of the simplest universes, your code can be written as
follows. There is no need to existentially quantify anything. Your
code becomes pure Haskell98.


data Expr       = Expr  String       -- Dummy expression type for spike
     deriving Eq

data Ruleset ex = Ruleset ex String  -- Dummy ruleset type for spike
     deriving Eq

data Datatype ex = Datatype
     { typeName   :: String
     , typeSuper  :: [Datatype ex]
     , typeMap :: InjProjMap ex
     , typeRules  :: Ruleset ex
     }
     

data InjProjMap ex = InjProjMap
	{ mapL2V    :: String -> Maybe Univ
	, mapV2L    :: Univ -> Maybe String
	}
	

data Univ = UInt Integer | UBool Bool

datatypeXsdInteger = Datatype
     { typeName   = "http://www.w3.org/2001/XMLSchema#integer"
     , typeSuper  = [datatypeXsdInteger]
     , typeMap    = mapXsdInteger
     , typeRules  = rulesetXsdInteger
     }

mapXsdInteger = InjProjMap
     { -- mapL2V :: String -> Maybe Univ
       mapL2V = \ s -> case [ x | (x,t) <- reads s, ("","") <- lex t ] of
                     [] -> Nothing
                     is -> Just $ UInt $ head is
       -- mapV2L :: Integer -> Maybe String
     , mapV2L = \v -> case v of {(UInt x) -> Just $ show x; _ -> Nothing }
     }

rulesetXsdInteger = Ruleset (Expr "expr") "rules"

test1 = typeName datatypeXsdInteger == "http://www.w3.org/2001/XMLSchema#integer" 
test2 = typeName (head $ typeSuper datatypeXsdInteger) == typeName datatypeXsdInteger
test3 = typeRules datatypeXsdInteger == rulesetXsdInteger