Re: Existential types, save me now?

1999-11-22 Thread Alex Ferguson


Hi Fergus.

   data OrdFuncExist = OE (Ord a = Char - a)
  
 That's not the syntax for a existential type,
 that's the syntax for a universally quantified type
 with rank-2 polymorphism.  With that syntax, the
 argument of `OE' must be a polymorphic function
 with type `forall a . Ord a = Char - a'.

That would explain a lot.  There seems to be a discrepancy between ghc
and the ghc user-guide, in that event.


 Is this supposed to be a heterogenous list,
 or a homogeneous list?

Sorry, I should have been a tad less terse:  it's intended to be
a homogeneous list, else the maximum wouldn't be well-typed.


 Hmm, I'm not sure exactly what you're trying to achieve here...
 but perhaps you just need to add
   
   instance Ord AnyOrd where
   compare (MkAnyOrd x) (MkAnyOrd y) = compare x y
 
 to make it work.

I haven't tried this, but this is unwrapping two (potentially)
_different_ types, and then trying to compare them, isn't it?
(Been there, done that, didn't like the type errors, in a previous
brush with existential types...)

Cheers,
Alex.



RE: Existential types, save me now?

1999-11-22 Thread Mark P Jones

Hi Alex,

| Here's some of the threatened examples:
| 
|  data OrdFuncExist = OE (Ord a = Char - a)
|  data OrdListExist = OLE (Ord a = [a])

Perhaps this is a GHC/Hugs difference, but the syntax that you've
used here isn't permitted in Hugs ... and in old versions where it
might have been allowed, it would suggest *universal* quantification
rather than existential.

I just rewrote the definitions to fit with the Hugs syntax for
existentials as follows:

 data OrdFuncExist = forall a. Ord a = OE (Char - a)
 data OrdListExist = forall a. Ord a = OLE [a]

and now the rest of the code that you sent type checks without any
apparent problem, including emap, blah, and emax.

[We keep trying to argue that it makes sense to use the "forall" keyword
here (because the constructor function that is being defined really does
have a polymorphic type).  But perhaps this is a further indication that
the time for a "exists" keyword has come!]

Hope this helps!

All the best,
Mark


[EMAIL PROTECTED]  Pacific Software Research Center, Oregon Graduate Institute
Looking for a PhD or PostDoc?  Interested in joining PacSoft?  Let us know!




Re: Existential types, save me now?

1999-11-22 Thread Fergus Henderson

On 22-Nov-1999, Alex Ferguson [EMAIL PROTECTED] wrote:
 
 Here's some of the threatened examples:
 
  data OrdFuncExist = OE (Ord a = Char - a)
 
That's not the syntax for a existential type,
that's the syntax for a universally quantified type
with rank-2 polymorphism.  With that syntax, the
argument of `OE' must be a polymorphic function
with type `forall a . Ord a = Char - a'.

I think the syntax for what you want is
data OrdFuncExist = Ord a = OE (Char - a)

  data OrdListExist = OLE (Ord a = [a])

Is this supposed to be a heterogenous list,
or a homogeneous list?  That is, must the elements
all have the same type `a', or is the choice of `a' 
supposed to be allowed to vary for each element?

If you want a homogeneous existentially quantified list,
then use

data OrdListExist = Ord a = OLE [a]

But I suspect you want a heterogenous existentially quantified list.
In that case, you should use something like this:

data AnyOrd = Ord a = MkAnyOrd a
data OrdListExist = [AnyOrd]

  emap :: OrdFuncExist - [Char] - OrdListExist
  emap (OE f) l = OLE (map f l)

You'll probably need something along the lines of

emap (OE f) l = OLE (map (MkAnyOrd . f) l)

 The other problem:
 
  emax :: OrdListExist - OrdListExist
  emax (OLE l) = OLE [maximum l]
 
 Now, I think I see why this doesn't work:  but any ideas on how to fix?

Hmm, I'm not sure exactly what you're trying to achieve here...
but perhaps you just need to add

instance Ord AnyOrd where
compare (MkAnyOrd x) (MkAnyOrd y) = compare x y

to make it work.

-- 
Fergus Henderson [EMAIL PROTECTED]  |  "I have always known that the pursuit
WWW: http://www.cs.mu.oz.au/~fjh  |  of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED]| -- the last words of T. S. Garp.



RE: Existential types, save me now?

1999-11-22 Thread Alex Ferguson


Hi Mark, all:  thanks for the swiftly muddle-dispelling response.

 | Here's some of the threatened examples:
 | 
 |  data OrdFuncExist = OE (Ord a = Char - a)
 |  data OrdListExist = OLE (Ord a = [a])
 
 Perhaps this is a GHC/Hugs difference, but the syntax that you've
 used here isn't permitted in Hugs ... and in old versions where it
 might have been allowed, it would suggest *universal* quantification
 rather than existential.

Must be such a difference.  This is what ghc accepts, and documents:
the user guide even claims to following hugs, here, so that'll be a
tad out of date, then...


 I just rewrote the definitions to fit with the Hugs syntax for
 existentials as follows:
 
  data OrdFuncExist = forall a. Ord a = OE (Char - a)
  data OrdListExist = forall a. Ord a = OLE [a]
 
 and now the rest of the code that you sent type checks without any
 apparent problem, including emap, blah, and emax.

It does me ego no end of good to find out that I'm right, and the
compiler is wrong (for a change, it must be said...).  Unless either
ghc or hbc catch up to the Hugs extension, though, avails me little
in practice, sadly.  (Hint, hint.)


 [We keep trying to argue that it makes sense to use the "forall" keyword
 here (because the constructor function that is being defined really does
 have a polymorphic type).  But perhaps this is a further indication that
 the time for a "exists" keyword has come!]

The forall looks syntactically _unnecessary_, slap-bang next to a context,
but it's not confusing in and of itself -- well, not beyond my usual
level of confusion about positive and negative quantifier occurrences.
(Different systems and different docs certainly are, though.)

Cheers,
Alex.



Re: Existential types, save me now?

1999-11-22 Thread Fergus Henderson

On 22-Nov-1999, Alex Ferguson [EMAIL PROTECTED] wrote:
 
  Is this supposed to be a heterogenous list,
  or a homogeneous list?
 
 Sorry, I should have been a tad less terse:  it's intended to be
 a homogeneous list, else the maximum wouldn't be well-typed.

Oh, of course -- you're quite correct.

-- 
Fergus Henderson [EMAIL PROTECTED]  |  "I have always known that the pursuit
WWW: http://www.cs.mu.oz.au/~fjh  |  of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED]| -- the last words of T. S. Garp.