How to define a polyvariadic arrow?

2
votes

This question is somewhat related to this earlier one:

I am trying to define a couple of semi-dependent types, which allow you to track the 'monotonicity' of functions (as described in the Monotonicity Types paper), so that the programmer does not have to do this manually (and fail at compile-time when a non-monotonic operation is passed to something that requires one).

More generally: I'd like to keep track of some 'qualifiers' of a function

Based on answers to this earlier question, I have been able to define an 'indexed category' and 'indexed arrow' where the qualifiers of h in h = f >>> g depend on the qualifiers of f and g.

This works well, as long as you only work with single-argument functions. However, (and normal arrows also have this problem), when you try to create an arrow with multiple arguments, you have the following options. (Using (+) :: Int -> Int -> Int as example):

  1. Plain arr (+). The result type of this will be Arrow x => x Int (Int -> Int), since the function is curried. This means that only the first parameter is lifted into the arrow context, since the arrow 'returns a function with one parameter less'. In other words: The arrow context is not used for the rest of the arguments, so that's not what we want.
  2. arr (uncurry (+)). The result type of this will be Arrow x => x (Int, Int) Int. Now both parameters have become part of the arrow, but we lose the ability to e.g. partially apply it. It also is not clear to me how to do uncurrying in an arity-independent way: What if we want three, four, five, ...-parameter functions?

I know it is possible to define a 'recursive typeclass' to create a polyvariadic function, such as for instance described on Rosettacode here. I have tried to define a more general function-wrapping type that might work that way, but I have not managed to do so far. I have no idea how to properly discern in the typeclass instance for a -> b whether b is the final result or another function (b' -> c), and how to extract and use the qualifier of b' if it turns out to be the second case.

Is this possible? Am I missing something here? Or am I completely on the wrong track and is there another way to lift an n-argument function into an arrow, regardless of the value of n?

1
haskellarrows

1 Answers

3
votes

Here's how you can define arrowfy to turn a function a -> b -> ... into an arrow a `r` b `r` ... (where r :: Type -> Type -> Type is your arrow type), and a function uncurry_ to turn a function into one with a single tuple argument (a, (b, ...)) -> z (which can then be lifted to an arbitrary arrow with arr :: (u -> v) -> r u v).

{-# LANGUAGE
    AllowAmbiguousTypes,
    FlexibleContexts,
    FlexibleInstances,
    MultiParamTypeClasses,
    UndecidableInstances,
    TypeApplications
  #-}

import Control.Category hiding ((.), id)
import Control.Arrow
import Data.Kind (Type)

Both approaches use a multiparameter type class with overlapping instances. One instance for functions, which will be selected as long as the initial type is a function type, and one instance for the base case, which will be selected as soon as it's not a function type.

-- Turn (a -> (b -> (c -> ...))) into (a `r` (b `r` (c `r` ...)))
class Arrowfy (r :: Type -> Type -> Type) x y where
  arrowfy :: x -> y

instance {-# OVERLAPPING #-} (Arrow r, Arrowfy r b z, y ~ r a z) => Arrowfy r (a -> b) y where
  arrowfy f = arr (arrowfy @r @b @z . f)

instance (x ~ y) => Arrowfy r x y where
  arrowfy = id

Side note about arrowfy @r @b @z syntax

This is TypeApplications syntax, available since GHC 8.0.

The type of arrowfy is:

arrowfy :: forall r x y. Arrowfy r x y => x -> y

The problem is that r is ambiguous: in an expression, the context can only determine x and y, and this doesn't necessarily restrict r. The @r annotation allows us to explicitly specialize arrowfy. Note that the type arguments of arrowfy must occur in a fixed order:

arrowfy :: forall r x y. ...

arrowfy @r1 @b @z             -- r = r1, x = b, y = z

(GHC user guide on TypeApplications)

Now, for example, if you have an arrow (:->), you can write this to turn it into an arrow:

test :: Int :-> (Int :-> Int)
test = arrowfy (+)

For uncurry_, there is a small additional trick so that n-argument functions are turned into functions on n-tuple, rather than (n+1)-tuples capped by a unit which you would get naively. Both instances are now indexed by function types, and what is actually being tested is whether the result type is a function.

-- Turn (a -> (b -> (c -> ... (... -> z) ...))) into ((a, (b, (c, ...))) -> z)
class Uncurry x y z where
  uncurry_ :: x -> y -> z

instance {-# OVERLAPPING #-} (Uncurry (b -> c) yb z, y ~ (a, yb)) => Uncurry (a -> b -> c) y z where
  uncurry_ f (a, yb) = uncurry_ (f a) yb

instance (a ~ y, b ~ z) => Uncurry (a -> b) y z where
  uncurry_ = id

Some examples:

testUncurry :: (Int, Int) -> Int
testUncurry = uncurry_ (+)

-- combined with arr
testUncurry2 :: (Int, (Int, (Int, Int))) :-> Int
testUncurry2 = arr (uncurry_ (\a b c d -> a + b + c + d))

Full gist: https://gist.github.com/Lysxia/c754f2fd6a514d66559b92469e373352