Tim Docker wrote:
I wish to define a flexible report, consisting of a set of columns. The contents of each column can be defined by mapping a function to a row descriptor, generating a value, and then converting each value to a string. I also wish to present an aggregate value at the bottom of the column defined by another function.
It seems that existential types are required to get this sort of thing to work. Is there another way?
It seems there is. Here's your code:
data ColDesc rowv = forall a. ColDesc (rowv -> a) ([a] -> a) (a -> String)
calculate :: [rowv] -> ColDesc rowv -> ([String],String) calculate rs (ColDesc valf sumf fmtf) = let vals = map valf rs in (map fmtf vals, (fmtf.sumf) vals)
Here's the new code:
data ColDesc rowv = ColDesc (rowv -> String) ([rowv] -> String)
calculate :: [rowv] -> ColDesc rowv -> ([String],String) calculate rs (ColDesc fmtf sumf) = (map fmtf rs, sumf rs)
rows = ["I","wish","to","define","a","report"]
mapp g f = g . (map f)
cols = [ ColDesc (id.id) $ id.(\_ -> ""), ColDesc (show.length) $ show.(mapp sum length), let valf = (\s -> length s * length s) in ColDesc (show.valf) $ show.(mapp maximum valf) ]
values = [ calculate rows col | col <- cols ]
It was derived with a simple transformation: composing (rowv -> a) with (a->String) to eliminate the existential type a. It seems there is a pattern here. When we write data Foo a b = forall ex. Foo <something1> <something2> <something3> with ex unconstrained, then one of <something> must be a function F(a,b) -> ex and another something is a function ex -> G(a,b). Here F(a,b) is some expression that includes ground types, a, b -- but not ex. Indeed, otherwise we have no way to convert something into ex and to get anything out. The third something is perhaps a transformer ex -> H(a,b) -> ex. It seems therefore we are guaranteed that there is always a composition of <something>s that does not include ex. Therefore, instead of carrying original <something>, we can carry the compositions, and get rid of the existential quantification. It seems that (g.f) :: i -> o is equivalent to stating exists c. f:: (i->c) ^ g::(c->o) or, in the Haskell type language data P i o = forall c. P (i->c) (c->o) P f g I also have a nagging feeling that this approach relates to Skolemization. Indeed, Mike Gunter's transformation from
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
to
data Stat i o = Stat { update :: i -> Stat i o , result :: o }
looks awfully like a Skolemization, with 'Stat i o' being the Skolem function.
On Thu, 9 Oct 2003 19:13:48 -0700 (PDT) oleg@pobox.com wrote:
It was derived with a simple transformation: composing (rowv -> a) with (a->String) to eliminate the existential type a.
It seems there is a pattern here. When we write data Foo a b = forall ex. Foo <something1> <something2> <something3>
with ex unconstrained, then one of <something> must be a function F(a,b) -> ex and another something is a function ex -> G(a,b). Here F(a,b) is some expression that includes ground types, a, b -- but not ex. Indeed, otherwise we have no way to convert something into ex and to get anything out. The third something is perhaps a transformer ex -> H(a,b) -> ex. It seems therefore we are guaranteed that there is always a composition of <something>s that does not include ex. Therefore, instead of carrying original <something>, we can carry the compositions, and get rid of the existential quantification.
It seems that (g.f) :: i -> o is equivalent to stating exists c. f:: (i->c) ^ g::(c->o) or, in the Haskell type language data P i o = forall c. P (i->c) (c->o) P f g
As always, the wiki has some remarks about this, http://www.haskell.org/hawiki/ExistentialTypes.
At 22:48 09/10/03 -0400, Derek Elkins wrote:
As always, the wiki has some remarks about this, http://www.haskell.org/hawiki/ExistentialTypes.
Thanks for the reminder :-) Interestingly, when I read this: [[ However this won't work since the elements of the list can be of SEVERAL different types (like a sphere and a polygon and a mesh etc. etc.) but lists need to have elements of the same type. ]] I was reminded of very similar issues I encountered in my own development, which for the most part I resolved without using existential types. Originally, I had contemplated using type classes, so that (w.r.t. the above example) spheres and polygons would be different types that are instances of a common class. That's how we do it with OOP, right? But it falls foul of exactly the point made here -- you can't mix the types in (say) a list. It never occurred to me that existential types might be the appropriate appoach here. Instead, I replace the class instances by a single algebraic data type, whose members are functions corresponding to OO-style class methods. #g -- ------------ Graham Klyne GK@NineByNine.org
Derek Elkins
On Thu, 9 Oct 2003 19:13:48 -0700 (PDT) oleg@pobox.com wrote:
... It seems that (g.f) :: i -> o is equivalent to stating exists c. f:: (i->c) ^ g::(c->o) or, in the Haskell type language data P i o = forall c. P (i->c) (c->o) P f g
As always, the wiki has some remarks about this, http://www.haskell.org/hawiki/ExistentialTypes.
Interestingly, the Haskell Wiki page has an example very similar to the one which prompted my questioning in the first place. I've been reading the paper by John Hughes and Doaitse Swierstra from this year's ICFP, "Polish Parsers, step by step" (or words to that effect). There they use a type pretty similar to this one from the Wiki page:
data Expr a = Val a | forall b . Apply (Expr (b -> a)) (Expr b)
I've been trying to convince myself that we really need the existential types here. Q: What can we do with a value of type (b -> a)? A: Apply it to a "b". Q: What can we do with a value of type b? A: Apply (b -> a) to it. Now (Expr a) is really two things: * A structural representation of a term * A fancy representation of a set of function applications So there are really two functions of interest:
getValue :: Expr a -> a -- polymorphic recursion! Signature required! getValue (Val a) = a getValue (Apply f b) = getValue f $ getValue b
getStructure :: Expr a -> Expr b -- Strip out the Vals getStructure (Val a) = Val undefined getStructure (Apply f b) = Apply (getStructure f) (getStructure b)
Using this observation, we might redefine Expr in a number of ways which avoid the existential type:
-- First, a version in which the rightmost Val is the result of getValue. data Expr' a = Val' a | Apply' (Expr' ()) (Expr' a)
val = Val
apply :: Expr' (a -> b) -> Expr' b -> Expr' a apply f b = Apply' (getStructure' f) (applyVal (getValue' f) b) -- in practice you'd want a getStructureAndValue here so that -- this can't leak space. But the original data structure had -- the same issue.
applyVal :: (a -> b) -> Expr a -> Expr b applyVal f (Val' v) = f v applyVal f (Apply' g b) = Apply' g (applyVal f b)
getValue' :: Expr' a -> a getValue' (Val' v) = v getValue' (Apply f v) = getValue' v
getStructure' :: Expr a -> Expr b getStructure' e = applyVal (const undefined) e
I've sort-of convinced myself that you could use this trick on the data structure in the paper.
-- Similarly, we might just keep value and structure separate data Expr'' a = Expr'' a Structure data Structure = Value | Application Structure Structure
val' a = Expr'' a Value
apply :: Expr'' (a -> b) -> Expr'' b -> Expr'' a apply (Expr'' f s) (Expr'' b t) = Expr'' (f b) (Application s t)
getValue'' (Expr'' v _) = v getStructure'' (Expr'' _ s) = s
I guess I'm now back to my original puzzlement: do we *ever* need existential types given laziness and higher-order functions? Or are they just a convenience? I'm crystallizing a bunch of hunches here. That's made this conversation incredibly useful for me. Thanks to all so far. -Jan-Willem Maessen jmaessen@alum.mit.edu
Jan-Willem Maessen wrote:
data Expr a = Val a | forall b . Apply (Expr (b -> a)) (Expr b)
I've been trying to convince myself that we really need the existential types here. ... Now (Expr a) is really two things: * A structural representation of a term * A fancy representation of a set of function applications
Using this observation, we might redefine Expr in a number of ways which avoid the existential type:
Funny I've been thinking about the same example. I have also found a way to eliminate the existential quantification, in the most faithful way: by implicitly preserving it. The question remains: do existential-free expressions "equivalent" to the original ones? It seems, with the existential quantification we can do more things. However, all these things are equivalent under observation. Let's start with the original problem:
data Expr a = Val a | forall b . Apply (Expr (b -> a)) (Expr b)
test = Apply (Val fromEnum) (Apply (Apply (Val (==)) (Val 'd')) (Val 'c'))
We can compute its value:
eval:: forall a. Expr a -> a -- polymorphic recursion! eval t = case t of (Val x) -> x (Apply f x) -> (eval f) (eval x)
and its size (a structural characteristic)
size:: forall a. Expr a -> Int size t = case t of (Val x) -> 1 (Apply f x) -> (size f) + (size x) + 1
Here's a quantification-free re-formulation. Note: it's Haskell 98:
makev v f g seed = (g seed,v) makea opr opa f g seed = let (seed1,opr') = opr f g seed in let (seed2,opa') = opa f g seed1 in (f seed2,(opr' opa'))
test1 = makea (makev fromEnum) (makea (makea (makev (==)) (makev 'd')) (makev 'c'))
eval1 t = snd $ t id id id
size1 t = fst $ t (+1) (+1) 0
There is no polymorphic recursion anymore. As expected, the structure is represented by a fold combinator, and the value is represented by a composition of functions. The composition has inside itself the existential quantification, as was mentioned earlier. But even Haskell98 permits that. If we want to make the structure explicit, we can make it so:
data Tree = Leaf | Fork Tree Tree deriving Show toTree t = fst $ t (\(k1:k2:rest)-> (Fork k2 k1):rest) (Leaf:) []
*> toTree test1 *> [Fork (Fork Leaf (Fork Leaf Leaf)) Leaf] I still have an uneasy feeling. The original representation would let us do more operations: we can flatten the tree:
flatten1 n@(Val x) = n flatten1 (Apply f a) = Apply (Val $ eval f) (Val $ eval a)
so the tree would have at most two levels (counting the root). If the tree represents an expression, the flattened tree represents a partially evaluated expression. We are able to assign correct values of the correct types to the branches of the Apply node: even if we do not know the types of those values! We can't make such a _harmonious_ flattening in other representations. We can produce a flattened tree that has different children of the Apply node -- yet the tree value is the same. So, the existential quantification permits more nuanced transformations -- and yet the nuances aren't observable. So, they don't matter?
Oleg replies to my message on eliminating existentials:
Jan-Willem Maessen wrote:
data Expr a = Val a | forall b . Apply (Expr (b -> a)) (Expr b)
I've been trying to convince myself that we really need the existential types here. ... Now (Expr a) is really two things: * A structural representation of a term * A fancy representation of a set of function applications
Funny I've been thinking about the same example. I have also found a way to eliminate the existential quantification, in the most faithful way: by implicitly preserving it. The question remains: do existential-free expressions "equivalent" to the original ones? It seems, with the existential quantification we can do more things. However, all these things are equivalent under observation. ... [snip] Here's a quantification-free re-formulation. Note: it's Haskell 98:
makev v f g seed = (g seed,v) makea opr opa f g seed = let (seed1,opr') = opr f g seed in let (seed2,opa') = opa f g seed1 in (f seed2,(opr' opa'))
test1 = makea (makev fromEnum) (makea (makea (makev (==)) (makev 'd')) (mak *>ev 'c'))
eval1 t = snd $ t id id id
size1 t = fst $ t (+1) (+1) 0
This is similar to my second formulation (a pair of value and structure), except that you're quantifying over the traversal of that structure and eliminating the structural type entirely. I do wonder how you'd write the type "Expr a" in this setting. I think the intermediate value of the traversal must inevitably get involved, at which point we need either extra type variables or existential type.
There is no polymorphic recursion anymore.
Indeed, my second formulation (tupling) eliminated the need for polymorphic recursion. Interestingly, by making traversal explicit in this way you throw away the chief advantage of laziness: memoization. The two formulations I presented both memoize the result of eval1 (which I called getValue). This memoization did not occur in the original structure, and might not even be desirable. With a bit of tweaking, I can control evaluation of subtrees by using "seq" on the structural representation. But there isn't an easy way to *not* memoize eval1 unless we resort to a formulation like the one you give.
I still have an uneasy feeling. The original representation would let us do more operations: we can flatten the tree:
flatten1 n@(Val x) = n flatten1 (Apply f a) = Apply (Val $ eval f) (Val $ eval a)
so the tree would have at most two levels (counting the root).
Surprisingly easy if you explicitly represent the structure---again, just as long as you're comfortable with the memoization that's going on. If you aren't, then it's hard. I speculate that most of the time we don't care that the memoization is happening, and it might even be a good thing. I'm not sure that's the case for the Hughes/Swierstra parser trick---on the other hand, they cook up a very special set of functions to push values deeper into the structure, which we may get for free in a separated formulation.
So, the existential quantification permits more nuanced transformations -- and yet the nuances aren't observable. So, they don't matter?
Whether they matter or not depends upon our aims. I'm curious about what's possible---in the hopes that I can get a better handle on what's really desirable in a particular situation. -Jan-Willem Maessen jmaessen@alum.mit.edu
On Mon, 13 Oct 2003 11:37:43 -0400
Jan-Willem Maessen
So, the existential quantification permits more nuanced transformations -- and yet the nuances aren't observable. So, they don't matter?
Whether they matter or not depends upon our aims. I'm curious about what's possible---in the hopes that I can get a better handle on what's really desirable in a particular situation.
Indeed. One of the issues is useability or at least naturality. It seems that existentials in some situations better achieve the intent/goal. Anyways, if another challenge is desired, I would be interested in seeing how one would go about converting the implementation of Dynamics in "A Lightweight Implementation of Generics and Dynamics" into a form that doesn't use existentials* but still provides the same (or very similar or I guess simpler) interface. * No coding existentials as universals :P data Showable = Showable (forall r.(forall a.Show a => a -> r) -> r) mapM_ (\(Showable v) -> v print) [Showable ($ 5),Showable ($ True)] 5 True
Derek Elkins wrote:
Anyways, if another challenge is desired, I would be interested in seeing how one would go about converting the implementation of Dynamics in "A Lightweight Implementation of Generics and Dynamics" into a form that doesn't use existentials* but still provides the same (or very similar or I guess simpler) interface.
data Showable = Showable (forall r.(forall a.Show a => a -> r) -> r) mapM_ (\(Showable v) -> v print) [Showable ($ 5),Showable ($ True)]
I'm sorry I don't understand if the latter is meant to relate to the former. The latter does not seem to include the existential quantification: (1) data E = forall a. E a (2) data U = U (forall a. a->a) Only E in (1) is an existentially-quantified constructor (according to GHC's users_guide/type-extensions.html). Indeed, in (U f), f must be a fully polymorphic function forall a. a->a. That is, 'id' plus various flavors of undefined and error. OTH, in (E v), v is a value that can _only_ be *passed* to a fully polymorphic function of a signature forall a. a->something. That is, we can apply f to _any_thing and to pass v to a function that takes _every_thing. The duality of the universal and existential quantification can be summarized by the following Haskell code:
test (E a) (U f) = E (f a)
More examples:
data E1 = forall x. E1 (x->x) data U1 = U1 (forall x. x)
E1 not -- OK U1 undefined -- OK Indeed, we can apply the constructor U1 only to the bottom -- the only fully polymorphic value. OTH, we can apply the constructor E1 to any function of a type x->x. If we have the value E1, we can pass the enclosed value only to a function of the signature forall x. (x->x) -> something. For example, ($): let e1 = E1 not in case e1 of (E1 f) -> E $ ($) f let e1 = E1 (1+) in case e1 of (E1 f) -> E $ ($) f both expressions are OK. As to the implementation of Generics and Dynamics without the use of existentials, I wonder if the type heaps (extensively discussed in the context of safe casts) will do the trick, at least to some extent. Incidentally, a type heap is another way to eliminate an existential quantification. Indeed, to emulate data E = forall a. E a we can write data E' = E' TypeHeapType Int the values in the typeheap (and their types) are indexed by integers. I admit to some cheating: we can only place into E' values of the types used in the construction of the typeheap (not any values). Perhaps other type universes can be used too. The trick is of course the existence of a value representation of a type.
On Mon, 13 Oct 2003 23:41:17 -0700 (PDT) oleg@pobox.com wrote:
Derek Elkins wrote:
Anyways, if another challenge is desired, I would be interested in seeing how one would go about converting the implementation of Dynamics in "A Lightweight Implementation of Generics and Dynamics" into a form that doesn't use existentials* but still provides the same(or very similar or I guess simpler) interface.
data Showable = Showable (forall r.(forall a.Show a => a -> r) -> r) mapM_ (\(Showable v) -> v print) [Showable ($ 5),Showable ($ True)]
I'm sorry I don't understand if the latter is meant to relate to the former. The latter does not seem to include the existential quantification:
Of course not! That was the point. It encodes existential quantification using (rank-2) universal quantification. So this could be used to provide an existential-free implementation of Dynamics (and I have converted some of the Dynamics implementation to this form fairly mechanically, and don't doubt that it would extend to the full implementation). Anyways, the basis for it is exists x. P x <=> ~forall x.~P x <=> ~forall x.P x -> _|_ <=> (forall x.P x -> _|_) -> _|_. Now with a classical logic version of the Curry-Howard isomorphism this is interpreted as a continuation. Alternatively, you can think operationally. The closure (e.g. ($ 5)) holds the witness in it's environment and the universal quantification limits what you can do to the type to what is provided and the continuation aspect controls the scope all analogous to how existentials work.
As to the implementation of Generics and Dynamics without the use of existentials, I wonder if the type heaps (extensively discussed in the context of safe casts) will do the trick, at least to some extent.
Well, if you can provide a very similar/identical interface, then that's acceptable.
participants (4)
-
Derek Elkins -
Graham Klyne -
Jan-Willem Maessen -
oleg＠pobox.com