Using existential types

[oleg at pobox.com]

>data InjProjMap ex = InjProjMap
>         { mapL2V    :: String -> Maybe Univ
>         , mapV2L    :: Univ -> Maybe String
>         }
>
>
>data Univ = UInt Integer | UBool Bool

> I have a couple of questions:

> (1) is there any purpose served by having InjProjMap parameterized with 
> ex?  I don't see it.

Everything else in the Datatype was parameterized by 'ex' (although it
wasn't clear from the present code how 'ex' was actually used). So I
thought, why not.


> (2) the use of datatype Univ suggests to me that one must know in advance 
> all of the datatypes that will be used for my 'vt'.  That is something I'm 
> trying to avoid, as I'm explicitly trying to construct a framework in 
> which, while I know that there will be such an underlying type with certain 
> properties, I don't know anything about how it may be implemented.  (For 
> one of my target applications, I want to treat IP addresses as a distinct 
> datatype.)

The article about safe casts pointed out that the tagged union
Universe is the least convenient to extend. Still, Haskell module
system can help. We merely need to store the declaration
	data Univ = UInt Integer | UBool Bool ...
in a module and import that module (with the datatype and only the
constructors we need). If we don't import any constructors, the
datatype becomes abstract. To extend the datatype, we need to change
only one module. Alas, we need to recompile all the dependent code.

> Rather, what I want to do is expose relationships between (textual)
> representations of a datatype, while keeping the actual values used to
> derive those relationships hidden from view.

Tomasz Zielonka's approach can help. He has observed that writing
	forall vt. Datatype (DatatypeVal ex vt)
is useful -- provided that we pack into the data structure not
only the existentially quantified value itself but also *all* the
functions that may use that value. In your case, it seems that you
need to make the ruleset a part of the typeMap. Also, when a
datatype contains a quantified value, we can't use the record syntax
(we have to use the positional syntax). Here's your code with some
enhancements. I do want to note that the casting approach seems
generally a little bit more convenient. We need to pack only the
injector and the projector.

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
     , typeRules  :: Ruleset ex
     }

data InjProjMap = 
  forall vt. InjProjMap
	{- mapL2V -} (String -> Maybe vt)
	{- mapV2L -} (vt -> Maybe String)
	{- mapV2V -} (vt -> vt)
	
	
datatypeXsdInteger = Datatype
     { typeName   = "http://www.w3.org/2001/XMLSchema#integer"
     , typeSuper  = [datatypeXsdInteger]
     , typeMap    = integerMap
     , typeRules  = rulesetXsdInteger
     }

integerMap = 
  InjProjMap 
      -- mapL2V :: String -> Maybe Integer
      (\s -> case [ x | (x,t) <- reads s, ("","") <- lex t ] of
                     [] -> Nothing
                     is -> Just $ head is)
       -- mapV2L :: Integer -> Maybe String
     (Just . show)
     (2*)

positiveIntegerMap = InjProjMap
       {- mapL2V -}(\ s -> case [ x | (x,t) <- reads s, ("","") <- lex t ] of
                     [] -> Nothing
                     (is:_) | is > 0 -> Just is
		     _  -> Nothing)
       -- mapV2L :: Integer -> Maybe String
     {- mapV2L -} (Just . show)
     {- mapV2V -} (1+)

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

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


within_the_typemap dt lex = case (typeMap dt) of 
    InjProjMap mapL2V mapV2L mapV2V  -> doit $ mapL2V lex
                where 
	          doit (Just vt) = mapV2L $ mapV2V vt
	          doit _ = Nothing
	       

test4 = within_the_typemap datatypeXsdInteger "123"