At 10:41 pm +0000 4/11/99, Marcin 'Qrczak' Kowalczyk wrote:
>Thu, 4 Nov 1999 09:47:27 +0100 (MET), Koen Claessen <[EMAIL PROTECTED]> pisze:
>
> > data Expr a = Val a | forall b . Apply (b -> a) b
>
>For me it's isomorphic to
> data Expr a = Val a | Applied a
>if only we ignore the seq function. Because the only way you could
>use an `Apply x y', except passing its components around and applying
>seq to them, is to apply x to y yielding something of a known type,
>so it's just as we already had the result of the application.
>
> > data Action = forall b . Act (IORef b) (b -> IO ())
>
>Yes, I think that here existential is unavoidable.
I missed the start of this and am a bit confused - I keep seeing "forall", which is
universal, not "there exists", which is existential - at least as I know them. Are the
existentials talked about in relation to Haskell something different, or has the
notation just got confused?
As way of comparison, in Hope+C the type:
typevar a
stack(b) == pack(a x (b x a -> a) x (a -> b x a))
(Note Hope+C is not a curried language) is the type of a stack of b with some hidden
implementation (a), a push function (b x a -> a) and a pop function (a -> b x a). The
type of pack is:
forall b. there exists b. a x (b x a -> a) x (a -> b x a) -> stack(b)
such ADT's can be used as in:
let pack(s, push, pop) == e in ... use of s, push & pop, structure of s
inaccessible
The similarity to Cardelli & Wegner's pack is clear. Type system/checker & compiler
writers should also see a parallel in there with application & definition of
universally quantified functions (this is what makes implementing existential types
easy in this case).
Having said that, existentials where primarily used to support typed interlanguage
working within the continuation I/O system:
data IO == sum data type one constructor of which was:
CallImp(ImpFun(a, b) x a x (b -> IO))
and a & b must be existentially quantified or the whole thing doesn't work.
--
Nigel Perry, New Zealand. It makes as much sense to wear a "cycle style" helmet in a
car as on a bike... Choosing to wear one on a bike but not in a car is mere
inconsistency. Refusing to wear one in a car while insisting others do so on a bike is
pure hypocrisy. Don't be a hypocrite.
