Using existential types

[Graham Klyne]

I've been trying to use existential types [*] in my code.
[*] cf. Glasgow Haskell Compiler (GHC) user guide, section 7.3.12

My experiments have thrown up a couple of questions:

1.  forall x introduces x as existential when it appears immediately
     preceding a datatype constructor declaration, e.g. at -1- below.
     In position -2-, it appears to signal a universal quantifier.

     Is this a correct reading of the situation?


2.  I have been trying to use existential types to allow an auxiliary
     type to appear in the implementation of a datatype, and have ended
     up using one datatype to "wrap" another.  Is there a cleaner way?


The code below has been adapted from my development code to provide a 
stand-alone example of the kind of thing I'm trying to do.  It runs OK 
under Hugs.

#g
--


--  spike-existential.hs
--
--  experimenting with existential types
--
--  Questions:
--
--  1.  forall x introduces x as existential when it appears immediately
--      preceding a datatype constructor declaration, e.g. at -1- below.
--      In position -2-, it appears to be a universal quantifier.
--      ?
--
--  2.  Is there cleaner way to hide the datatype vt in the declaration
--      of DatatypeVal below, on the basis that I don't really want it to
--      be visible outside the inference rules that are specific to this
--      datatype, referenced by typeRules  If I apply the existential at
--      position -1-, an error is reported by Hugs:
--      "cannot use selectors with existentially typed components".
--
--      The approach I have adopted is to define two datatypes,
--      DatatypeVal which is parameterized by expression type and value
--      type, and Datatype which wraps a DatatypeVal with the value
--      type being an existential.  I've yet to work out implementation
--      details for the stuff that uses the value type, but I anticipate
--      using a constructor function that takes the DatatypeMap value
--      as an argument.
--

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

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

-- Type Datatype wraps DatatypeVal with an existential, thus
-- hiding the value type.  Also define access methods for those
-- components that don't reference the value type.

data Datatype ex = forall vt . Datatype (DatatypeVal ex vt)
typeName  (Datatype dtv) = tvalName  dtv
typeSuper (Datatype dtv) = tvalSuper dtv
typeRules (Datatype dtv) = tvalRules dtv


-- Type DatatypeVal uses a value type (vt) in its implementation.
-- See tvalMap;  the intent is that an implemenatation of tvalRules,
-- and other code may make use of this component.

data DatatypeVal ex vt = DatatypeVal
{-1- data DatatypeVal ex = forall vt . Datatype -1-}
     { tvalName   :: String
     , tvalSuper  :: [Datatype ex]
                                 -- ^ List of datatypes that are each a 
supertype
                                 --   of the current datatype.  The value space
                                 --   of the current datatype is a subset 
of the
                                 --   value space of each of these datatypes.
                                 --   NOTE:  these supertypes may be 
implemented
                                 --   using a different value type;  e.g. a
                                 --   supertype of xsd:integer is xsd:decimal
     , tvalMap    :: {-2- forall vt. -2-} DatatypeMap vt
                                 -- ^ Lexical to value mapping, where 'vt' is
                                 --   a datatype used within a Haskell program
                                 --   to represent and manipulate values in
                                 --   the datatype's value space
     , tvalRules  :: Ruleset ex  -- ^ A set of named expressions and rules
                                 --   that are valid in in any theory that
                                 --   recognizes the current datatype.
     }


data DatatypeMap vt = DatatypeMap
     { mapL2V    :: String -> Maybe vt
                             -- ^ Function to map lexical string to
                             --   datatype value.  This effectively
                             --   defines the lexical space of the
                             --   datatype to be all strings for which
                             --   yield a value other than Nothing.
     , mapV2L    :: vt -> Maybe String
                             -- ^ Function to map a value to its canonical
                             --   lexical form, if it has such.
     }

datatypevalXsdInteger :: DatatypeVal Expr Integer
datatypevalXsdInteger = DatatypeVal
     { tvalName   = "http://www.w3.org/2001/XMLSchema#integer"
     , tvalSuper  = [datatypeXsdInteger]
     , tvalMap    = mapXsdInteger
     , tvalRules  = rulesetXsdInteger
     }

datatypeXsdInteger :: Datatype Expr
datatypeXsdInteger = Datatype datatypevalXsdInteger

-- |mapXsdInteger contains functions that perform lexical-to-value
--  and value-to-canonical-lexical mappings for xsd:integer values
--
mapXsdInteger :: DatatypeMap Integer
mapXsdInteger = DatatypeMap
     { -- mapL2V :: String -> Maybe Integer
       mapL2V = \ s -> case [ x | (x,t) <- reads s, ("","") <- lex t ] of
                     [] -> Nothing
                     is -> Just $ head is
       -- mapV2L :: Integer -> Maybe String
     , mapV2L = Just . show
     }

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

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



------------
Graham Klyne
GK at NineByNine.org