[Haskell-cafe] A practical Haskell puzzle

[Yves Parès]

Okay thanks I got the difference between both.
The 'exists' syntax seems very useful. Is it planned to be added to GHC in a
near future?


2011/2/28 Heinrich Apfelmus <apfelmus at quantentunnel.de>

> 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
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110303/cdf7091a/attachment.htm>