On Thu, Oct 02, 2003 at 06:42:59PM -0700, oleg@pobox.com wrote:

...

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!

I think I have used unconstrained existentially quantified types in a useful way. Below is a combinator library for calculating statistics with aggregate functions (type Stat). I use a datatype 'Stat i o' to represent an aggregate function that can be fed with values of type 'i' and returns a result of type 'o'. I use existentially quantified constructor to hide the internal state of particular aggregate function. For example, avg's internal state is a pair of numbers, but it is hidden, because users of the library shouldn't have to know that. However this approach has caveats. For example you can't store the state of Stat and restart it later. All steps are done within one call to runStat. Example uses: {- average of the list of values -} runStat avg [1..20] 10.5 {- separate average for odd and even numbers -} runStat (fmap fmToList (categorize even (projectInput fromIntegral avg))) [1..20] [(False,10.0),(True,11.0)] {- word frequency -} runStat rank (words "this is a test is a test") [(2,"test"),(2,"is"),(2,"a"),(1,"this")] {- group words by lengths -} runStat (fmap fmToList (categorize length (fold (flip (:)) []))) (words "a aa ba wwww zz") [(1,["a"]),(2,["zz","ba","aa"]),(4,["wwww"])] ... etc Best regards, Tom ---------------------------------------------------------------------- {-# OPTIONS -fglasgow-exts #-} module Stat where import Data.FiniteMap import Prelude hiding (sum) import List (sort) data Stat i o = -- aggregate function taking i's on input and producing o forall s. Stat s -- init (s -> i -> s) -- update (s -> o) -- result runStat :: Stat i o -> [i] -> o runStat (Stat init update result) l = result (foldl update init l) fold :: (a -> b -> a) -> a -> Stat b a fold f i = Stat i f id count :: Num n => Stat a n count = fold (\s _ -> s+1) 0 sum :: Num n => Stat n n sum = fold (+) 0 pair :: Stat a b -> Stat a c -> Stat a (b,c) pair (Stat init1 update1 result1) (Stat init2 update2 result2) = Stat (init1, init2) (\(s1,s2) x -> (update1 s1 x, update2 s2 x)) (\(s1,s2) -> (result1 s1, result2 s2)) instance Functor (Stat a) where fmap f (Stat init update result) = (Stat init update (f . result)) projectInput :: (i -> j) -> Stat j a -> Stat i a projectInput f (Stat init update result) = Stat init (\s i -> update s (f i)) result avg :: Fractional n => Stat n n avg = fmap (\(s,c) -> if c /= 0 then s/c else 0) (pair sum count) avgMaybe :: Fractional n => Stat n (Maybe n) avgMaybe = fmap (\(s,c) -> if c /= 0 then Just (s/c) else Nothing) (pair sum count) categorize :: Ord k => (a -> k) -> Stat a b -> Stat a (FiniteMap k b) categorize fk (Stat init update result) = Stat emptyFM (\fm a -> addToFM fm (fk a) (update (maybe init id (lookupFM fm (fk a))) a)) (mapFM (const result)) rank :: Ord k => Stat k [(Int,k)] rank = fmap (reverse . sort . (map(\(k,c)->(c,k))) . fmToList) (categorize id count) -- .signature: Too many levels of symbolic links

Tomasz Zielonka wrote:

I think I have used unconstrained existentially quantified types in a useful way. Below is a combinator library for calculating statistics with aggregate functions (type Stat).

[BIG SNIP]

data Stat i o = -- aggregate function taking i's on input and producing o forall s. Stat s -- init (s -> i -> s) -- update (s -> o) -- result

I really liked this example, as it neatly crystallizes a few issues about existential types: * Existential types only make sense if you include a function which takes the type as an argument (here the update and result functions). Sometimes this function is the method of a class. * But it bugs me that an awful lot of examples of existential typing could be obtained simply by currying / lazy evaluation. In this case, however, the "update" function lets us absorb additional input as in the subsequent message (which I've now accidentally deleted):

oneInput :: Stat i o -> i -> Stat i o oneInput (Stat s update result) i = Stat (update s i) update result

I'd like to know, for my own edification: THEORY 1: It is possible to eliminate an existential type s from any data structure unless the structure includes one function (possibly a method) which mentions type s in both covariant and contravariant positions, and one function or data structure which mentions s only in covariant position [or did I mean contravariant here?]. Is this theory correct? This would go a long way to explaining why we might *need* (as opposed to merely "want") existential types. Of course, in the bad old days (or in Haskell 98) we'd just include extra type parameters. A bit ugly, but arguably we do the same thing whenever we write state transformers. -Jan-Willem Maessen jmaessen@alum.mit.edu PS - I note that the type "Stat" is a classic OO-style iterator that does basically the same thing as foldl. Interestingly, by writing in this way we can just include bits of the equational theory of foldl. The function pair is a great example of this:

pair :: Stat a b -> Stat a c -> Stat a (b,c)

On Wed, Oct 08, 2003 at 09:40:35AM -0700, Mike Gunter wrote:
> 
> Jan-Willem Maessen  writes:
> 
> > Tomasz Zielonka  wrote:
> > [...]
> > > data Stat i o = -- aggregate function taking i's on input and producing o
> > >     forall s. Stat
> > > 	s		-- init
> > > 	(s -> i -> s)	-- update
> > > 	(s -> o)	-- result
> > [...]
> > * But it bugs me that an awful lot of examples of existential typing
> >   could be obtained simply by currying / lazy evaluation.  In this
> >   case, however, the "update" function lets us absorb additional input
> >   as in the subsequent message (which I've now accidentally deleted):
> 
> I'm not convinced that existentials are needed here.
> 
> 	mike

You are right. When I came up with updateStat, I could go futher and
remove existential type.

Best regards,
Tom

-- 
.signature: Too many levels of symbolic links

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"