Rebindable syntax for arrow with constraint

Question

Consider a free arrow which the only task is remember how it was constructed. And I want to put some constraint (e.x. Show) on arguments of the arrow:

data FreeArrow a b where 
  LeafArrow :: (Show a, Show b) => FreeArrow a b 
  SeqArrow :: (Show a, Show b, Show c) => FreeArrow a b -> FreeArrow b c -> FreeArrow a c
  ParArrow :: (Show a1, Show b1, Show a2, Show b2) => FreeArrow a1 b1 -> FreeArrow a2 b2 -> FreeArrow (a1, a2) (b1, b2)

deriving instance Show (FreeArrow a b)

To define Arrow instance for FreeArrow we need to define restricted versions of Category and Arrow:

class Category cat where
    id :: Show a => cat a a
    (.) :: (Show a, Show b, Show c) => cat b c -> cat a b -> cat a c

class Category a => Arrow a where
    arr :: (Show b, Show c) => (b -> c) -> a b c
    first :: (Show b, Show c, Show d) => a b c -> a (b,d) (c,d)
    second :: (Show b, Show c, Show d) => a b c -> a (d,b) (d,c)
    (***) :: (Show b, Show c, Show b', Show c') => a b c -> a b' c' -> a 
    (&&&) :: (Show b, Show c, Show c') => a b c -> a b c' -> a b (c,c')

There are the instances:

instance Category FreeArrow where 
  id = LeafArrow
  (.) = flip SeqArrow

instance Arrow FreeArrow where 
  arr _ = LeafArrow
  first f = ParArrow f id
  second f = ParArrow id f 
  (***) = ParArrow

The approach operates well for hand-written arrows:

myArrow :: FreeArrow Double Double
myArrow = (a &&& a) >>> arr (uncurry (+))
  where a :: FreeArrow Double Double
        a = LeafArrow

main :: IO ()
main = print myArrow

Will print:

SeqArrow (SeqArrow LeafArrow (ParArrow LeafArrow LeafArrow)) LeafArrow

But for arrow syntax (GHC 7.8.3):

myArrow :: FreeArrow Double Double
myArrow = proc v -> a -< v
  where a :: FreeArrow Double Double
        a = LeafArrow

main :: IO ()
main = print myArrow

I got errors like:

/home/ncrashed/dev/haskell/ArrowProblem.hs:54:11:
    No instance for (Show c) arising from a use of ‘arr’
    Possible fix:
      add (Show c) to the context of
        a type expected by the context: (b -> c) -> FreeArrow b c
    In the expression: arr
    When checking that ‘arr’ (needed by a syntactic construct)
      has the required type: forall b1 c1. (b1 -> c1) -> FreeArrow b1 c1
      arising from a proc expression
      at /home/ncrashed/dev/haskell/ArrowProblem.hs:1:1
    In the expression: proc v -> a -< v

/home/ncrashed/dev/haskell/ArrowProblem.hs:54:11:
    No instance for (Show c) arising from a use of ‘>>>’
    Possible fix:
      add (Show c) to the context of
        a type expected by the context:
          FreeArrow a b -> FreeArrow b c -> FreeArrow a c
    In the expression: (>>>)
    When checking that ‘(>>>)’ (needed by a syntactic construct)
      has the required type: forall a1 b1 c1.
                             FreeArrow a1 b1 -> FreeArrow b1 c1 -> FreeArrow a1 c1
      arising from a proc expression
      at /home/ncrashed/dev/haskell/ArrowProblem.hs:1:1
    In the expression: proc v -> a -< v

/home/ncrashed/dev/haskell/ArrowProblem.hs:54:11:
    No instance for (Show d) arising from a use of ‘first’
    Possible fix:
      add (Show d) to the context of
        a type expected by the context:
          FreeArrow b c -> FreeArrow (b, d) (c, d)
    In the expression: first
    When checking that ‘first’ (needed by a syntactic construct)
      has the required type: forall b1 c1 d1.
                             FreeArrow b1 c1 -> FreeArrow (b1, d1) (c1, d1)
      arising from a proc expression
      at /home/ncrashed/dev/haskell/ArrowProblem.hs:1:1

Is there any way to fix this? Is that a bug?

Perhaps I should fall back to arrowp preprocessor...

P.S. There is a full sample of the code

Answer 1

What the problem is

When you use Haskell's arrow notation, it does not naively desugar proc v -> x -< y into the literal text arr (\v -> y) >>> x (using whatever arr and >>> are in-scope) but rather it uses the true values that it is expecting, desugaring it into effectively:

Control.Arrow.arr (\v -> y) Control.Arrow.>>> x

The problem is precisely that when you ran into a problem -- let's pretend that it's a house with a closed doorway -- you chose to build your own house right next door whose door you could open perfectly well (defining your own Arrow and Category instances), and now you're trying to drive a remote-control car which is hopelessly stuck in the other house, and you're confused because the doorways look very similar, so why isn't there an RC car upstairs in this house which all your commands are seamlessly rerouted to? The answer is, you'll need to build your own RC car and controller (Haskell source-to-source converter) to complete that approach.

Clearly the easier way is to chuck all of this work and look instead for a doorknob to the other house.

How to fix your code

Let me summarize how the walls and doors that are Haskell type classes work. You're programming at an advanced enough level that this may be review, so I apologize if this is too brief. For the Show type class, for example, you construct this Show dictionary-of-functions (show, showsPrec, showList) for a type constructor, and those functions can use other functions coming from other constraints on the class's type-parameters.

The compiler then stores a Show dictionary which takes the type constructor to a pair: first, the list of constraints on the type parameters, second, the actual dictionary that you've implemented, potentially using functions from the earlier constraints. When the compiler resolves Show (MyType ParamA ParamB) it therefore looks up MyType in the Show dictionary, finds an instance, verifies that ParamA and ParamB satisfy whatever constraints they have to satisfy (getting auxiliary dictionaries-of-functions for those classes), and forms the dictionary of Show functions. Hopefully that's mostly review; if not, go and study a tutorial on how Haskell type classes work.

This means that you don't need Show in the constructors you're writing. They're constructors! They don't do anything but glue values together in a way that you can latter pattern-match apart -- they don't need the functions show or showsPrec to do those. Without them you can still write:

data FreeArrow a b where
    LeafArrow :: FreeArrow a b
    SeqArrow :: FreeArrow a t -> FreeArrow t b -> FreeArrow a b
    ParArrow :: FreeArrow a1 b1 -> FreeArrow a2 b2 -> FreeArrow (a1, a2) (b1, b2)
deriving instance Show (FreeArrow a b)

instance Category FreeArrow where id = LeafArrow; (.) = flip SeqArrow

instance Arrow FreeArrow where
    arr = const LeafArrow
    first = flip ParArrow id
    second = ParArrow id
    (***) = ParArrow

In fact you can now use show on an arbitrary arrow,

*Main> show (LeafArrow :: FreeArrow () (IO String))
"LeafArrow"

whereas with your code above you could not even create that value because the LeafArrow constructor demanded a Show instance for IO String, which can't provide it. And your intended code works easily:

*Main> :set -XArrows
*Main> print $ proc v -> (LeafArrow :: FreeArrow Double Double) -< v
SeqArrow LeafArrow (SeqArrow LeafArrow LeafArrow)

We can do all of this because your "how it was constructed" information does not actually use the Show x typeclass to define the Show x instance for any of its instances.

How to do what I think you were trying to do

The only reason I can "fix" the stuff above is that you're not introspecting deep into the parameters involved -- which is I think what you want out of the Show type class. In fact you need to define a wholly different type class to get this sort of type information available from the Haskell runtime (unless I'm totally mistaken):

class TypeOf t where
    -- the integer here is 10 for type-constructor application, otherwise it is
    -- the precedence of the enclosing type-construction-operator.
    typePrec :: Int -> t -> String -> String
    typePrec _ t = (typeof t ++)
    typeof :: t -> String
    typeof t = typePrec 0 t "" -- starts at 0 if we have no other info.

instance TypeOf Int where typeof _ = "Int"

instance (TypeOf x) => TypeOf [x] where
    typeof list = "[" ++ typeof (head list) ++ "]"
instance (TypeOf x, TypeOf y) => TypeOf (x, y) where
    typeof x = "(" ++ typeof (fst x) ++ ", " ++ typeof (snd x) ++ ")"

-- Some helper functions for precedence parsing:
arg f x = typePrec 10 (f x)
pIf m n expr | m <= n    = ('(' :) . expr . (')' :)
             | otherwise = expr
a <**> b = a . (' ' :) . b
infixr 1 <**>

instance (TypeOf x) => TypeOf (IO x) where
    typePrec n x = pIf 10 n $ ("IO" ++) <**> arg io x
        where io = undefined :: IO x -> x

instance (TypeOf x, TypeOf y) => TypeOf (Either x y) where
    typePrec n x = pIf 10 n $ ("Either" ++) <**> arg left x <**> arg right x
        where left  = undefined :: Either x y -> x
              right = undefined :: Either x y -> y

First, there may be a way to write a C-based extension to Haskell which instead provides typeof :: x -> String for all x to Haskell; then you could hypothetically get by with just adding a string parameter to your arrows. Let's skip this possibility.

The biggest problem above is the (.) from Control.Category, which explicitly forbids access to the internal type b when composing cat a b with cat b c. Overcoming that is going to be very difficult. You can't thread any phantom-type data through cat unless you can protect cat from changing types.

A secondary problem is that you're really trying to annotate an existing arrow with metadata rather than defining your own arrow to probe a structure. Along those lines you might look into this crazy pathway:

Prelude Control.Arrow Control.Monad.Free Control.Monad.Identity> :set prompt "ghci> "
ghci> type MyArrow = Kleisli Identity
ghci> let x = arr (3*) :: Kleisli (Free (ArrowMonad MyArrow)) Int Int
ghci> :t x
x :: Kleisli (Free (ArrowMonad MyArrow)) Int Int

Basically what we're looking for here is to use typeof to somehow "walk" the tree that is here embodied by the Free monad.

There are obvious restrictions preventing us from saying "this is only an arrow if both its input and its output implement TypeOf" (namely, arr will not have the needed TypeOf constraint), so those types can't be hidden as a string in the constructor; they also can't be hidden in a phantom type because it says cat b c -> cat a b -> cat a c, which are the only two obvious ways to store the intermediary types). But there is not, as far as I can see, any obvious restriction to having a class which, at the end of constructing our values, is built of things which simultaneously implement Arrow and TypeOf.