Re: [Haskell-cafe] case, GADTs, Arrows

15 May 2014


      Thanks.

Отправлено с iPhone
...
15 мая 2014 г., в 3:48, Ross Paterson  написал(а):
...
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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] case, GADTs, Arrows

MigMit