Using existential types

Thu, 02 Oct 2003 11:44:55 -0700 

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
[EMAIL PROTECTED]

_______________________________________________
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to