On Sun, 16 Nov 1997, Patrik Jansson wrote:
| This can be done with existensial types as implemented in hbc.
| {...}
| data TShow = (Show ?a) => T ?a
Often, when you want to need existential types, you can do a nice trick
that I have used myself when I wanted to have existential types in
Haskell.
The trick also works for this example.
For a datatype, with constructor f:
data Foo = (Show ?a) => F ?a
f :: Show a => a -> Foo
f = F
we can already apply the show function to the element. (That is the only
thing you are allowed to do with it anyway!). You then get a datatype:
data Foo' = F' String
f' :: Show a => a -> Foo'
f' = F' . show
So the trick is to do the thing you might want to do with the object later
at the moment of construction, rather than destruction.
Another example is:
data Action m
= Act (m ?a) (?a -> Action m)
act :: m a -> (a -> Action m) -> Action m
act m f = Act m f
(Which represents a monadic continuation). The only thing you are allowed
to do with the existential type ?a is apply the function to the monadic
computation:
data Action' m
= Act' (m (Action' m))
act' :: m a -> (a -> Action' m) -> Action' m
act' m f = Act' (map f m)
With a little creativity, you can even do it for cases like:
data Fun
= (Show ?a) => F ?a (?a -> ?a)
f :: Show a => a -> (a -> a) -> Fun
f a g = F a g
The only thing you can do with the second component g is apply it to the
first component a finite number of times, or compute the fixpoint. The
result will still be an ?a, to which we can only apply the show function.
The datatype becomes thus:
data Fun'
= F' [String] -- = [g^0 a, g^1 a, ..]
String = fix g
f' :: Show a => a -> (a -> a) -> Fun
f' a g = F' (iterate g a) (fix g)
I found that this trick solves most cases from real programming where we
need existential types. Though having existential types would make some
programs much clearer... :-)
Note that there is hardly any overhead because of laziness.
Regards,
Koen.
--
Koen Claessen,
[EMAIL PROTECTED],
http://www.cs.chalmers.se/~koen,
Chalmers University of Technology.
