[clean-list] Re: Existential Types

[Ronny Wichers Schreur]

Jay Kint wrote (to the Clean Discussion List): 

>[..] I have an intersection function that returns the
>"surface", as you can see, an existential type. 
>[..] The parameter pattern {state, colorSurface} seems to
>do some sort of type binding/checking that the "(found, d,
>surface=:{state, colorSurface}) = Intersect r surfs" doesn't
>do.  Is this correct, and if so, why can't the second
>expression do the same type checking?

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.



Cheers,

Ronny Wichers Schreur