[Haskell-cafe] A practical Haskell puzzle

[Heinrich Apfelmus]

Yves Parès wrote:
>>  takeC :: Int -> Compoz a b -> (exists c. Compoz a c)
>>  dropC :: Int -> Compoz a b -> (exists c. Compoz c b)
> 
> What does 'exists' means? To create a rank-2 type can't you use:
> 
> takeC :: Int -> Compoz a b -> (forall c. Compoz a c)
> 
> ??

Ah, (exists c. Compoz a c)  means  "There exists a type  c  such that 
the whole thing has type  Compoz a c ".

What you describe would be the type "For any type  c  the whole thing 
can be treated as having type   Compoz a c " which is something entirely 
different.

The point is that in the former version, the function  takeC  determines 
what the type  c  should be and the caller has no clue what it is. In 
the latter version, the function that calls  takeC  can choose which 
type it should be.

What I wrote is *not* legal Haskell. (At least not in GHC. If I remember 
correctly, the EHC from Utrecht supports first-class existential 
quantification ). You have to encode it in some way, for instance with a 
data type

    data Exists f = forall c . Exists (f c)
    takeC :: Int -> Compoz a b -> Exists (Compoz a)


Regards,
Heinrich Apfelmus

--
http://apfelmus.nfshost.com