[clean-list] Re: Existential Types

[Fergus Henderson]

On 24-Oct-2001, Ronny Wichers Schreur <ronny@cs.kun.nl> wrote:
> Your analysis is correct. The essence of the example is:
> 
>     :: T = E.s: {state :: s, colour :: s -> Int}
> 
>     c1 s
>         =   s.colour s.state
>     c2 {colour, state}
>         =   colour state
> 
> In c1 the two selections of s will give two copies of the
> existentially qualified type variable s that can't be unified
> (as if the selections where functions). In c2 the connection
> is not lost.
> 
> Perhaps the type system could be changed to accommodate for
> this situation, but that's not how the rules are in Clean.

For what it's worth, the rules are the same in Mercury.
The syntax is different,

	:- type t ---> some [S] t(state :: S, colour :: (func(S) = int)).

	c1(S) = (S^colour)(S^state).

	c2(t(State, Colour)) = Colour(State).

but the result is the same: c1 has a type error, but c2 is allowed.

-- 
Fergus Henderson <fjh@cs.mu.oz.au>  | "... it seems to me that 15 years of
The University of Melbourne         | email is plenty for one lifetime."
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- Prof. Donald E. Knuth