[Haskell-cafe] case, GADTs, Arrows

[MigMit]

Thanks.

Отправлено с iPhone

> 15 мая 2014 г., в 3:48, Ross Paterson <R.Paterson at city.ac.uk> написал(а):
> 
>> On Wed, May 14, 2014 at 02:45:29PM +0400, Miguel Mitrofanov wrote:
>> Are there EXACT rules for desugaring "case" construct in Arrow syntax? The documentation says just "The translation is similar to that of if commands". But that can't be right in case of GADTs.
>> 
>> For example, let's say we have
>> 
>> data A where A :: Show s => s -> A
>> 
>> Then the following would work fine:
>> 
>> proc () ->
>>  do a <- arr A -< "test"
>>     case a of
>>       A s ->
>>         returnA -< show s
>> 
>> But if we abstract part of it:
>> 
>> b :: (Arrow a, Show s) => a s String
>> b =
>>  proc(s) ->
>>    returnA -< show s
>> 
>> proc() ->
>>  do a <- arr A -< "test"
>>     case a of
>>       A s ->
>>         b -< s
>> 
>> then it fails.
> 
> Actually the first one doesn't work either: it is accepted, but
> it generates invalid core -- the arrow translation doesn't handle
> existentials (this is bug #344).
> 
> The translation goes
> 
>    proc p -> case {p1 -> c1; ...; pn -> cn}
>    =
>    arr (\ p -> case {p1 -> (v1, p); ...; pn -> (vn, p)}) >>>
>        ((proc (v1, p) -> c1) ||| ... ||| (proc (vn, p) -> c))
> 
> where vi is the tuple of variables in pi.  Now if n = 1 there's no need
> for (|||) and therefore the ArrowChoice constraint, so that's a bit of
> a bug.  When there are existentials we should also include the required
> dictionaries in the tuple, but unfortunately that's not working.
> (#5777 is another arrows GADT bug.)
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe