case, GADTs, Arrows

14 May 2014

      Hi Café!

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.

Now, I'm not asking why exactly does it fail. I understand, that type classes are just data types, and, if arrow is fixed, then the real type of "b" would be

b :: Show s -> a s String

and that can't be combined with something of type a () (Show s, s).

So, the second example shouldn't work at all (although the error message could use some improvement). But I'm surprised that the first one does. Another unexpected thing is that it still requires ArrowChoice from the arrow, although there are no binary alternatives here.

Therefore, the rules would be quite helpful.

Miguel Mitrofanov

Ross Paterson

MigMit

tags

participants (3)