Is it possible to 'uncurry' a forall quantifier?

Question

Suppose we have a type constructor f that takes two types, by means of a DataKinds-promoted pair.

forall (f :: (ka, kb) -> *)

I can then implement a function forward, which is like curry for the forall quantifier:

forward :: forall (f :: (ka, kb) -> *).
           (forall (ab :: (ka, kb)).     f ab) ->
           (forall (a :: ka) (b :: kb).  f '(a, b))
forward x = x

However, the reverse function is problematic:

backward :: forall (f :: (*, *) -> *).
            (forall (a :: *) (b :: *). f '(a, b)) ->
            (forall (ab :: (*, *)). f ab)
backward x = x

GHC 8.0.1 gives the error message:

    • Couldn't match type ‘ab’ with ‘'(a0, b0)’
      ‘ab’ is a rigid type variable bound by
        the type signature for:
          backward :: forall (ab :: (*, *)). (forall a b. f '(a, b)) -> f ab
        at :6:116
      Expected type: f ab
        Actual type: f '(a0, b0)
    • In the expression: x
      In an equation for ‘backward’: backward x = x

Conceptually, it seems like a valid program. Is there another way to implement this function? Or is this a known limitation of GHC?

Not sure if type level computation is an appropriate label when 'computing' at the type level is not the goal. — Robert Hensing
As far as I'm aware, and much to my annoyance, GHC is not yet of the opinion that ab ~ '(Fst ab, Snd ab), where Fst and Snd are the type-level projections. — pigworker
Dunno for sure, but at a guess: Any strikes again. (Any :: (*, *) but it is not the case that Any ~ (a, b) for any a and b.) — Daniel Wagner
Pardon my ignorance, but what is the purpose of these forward and backward functions? When would you want to use them? They just look like complicated id functions to me. — Alexis King
@AlexisKing: well, logically speaking, any true statement is a tautology... ...seriously though, I could see this as quite useful if you need to “stuff” multiple types into a single functor. — leftaroundabout

dfeuer dfeuer · Accepted Answer · 2016-09-06T18:46:24

The trouble, as pigworker and Daniel Wagner indicate, is that ab may be a "stuck type". You can sometimes work around this with type families (as I learned in one of pigworker's papers):

type family Fst (x :: (k1, k2)) :: k1 where
  Fst '(t1, t2) = t1

type family Snd (x :: (k1, k2)) :: k2 where
  Snd '(t1, t2) = t2

backward :: forall (f :: (*, *) -> *) (ab :: (*, *)) proxy .
            proxy ab ->
            (forall (a :: *) (b :: *). f '(a, b)) ->
            f '(Fst ab, Snd ab)
backward _ x = x

Another option, sometimes, is to use wrappers.

newtype Curry f x y = Curry (f '(x,y))

data Uncurry f xy where
  Uncurry :: f x y -> f '(x, y)

Is it possible to 'uncurry' a forall quantifier?

1 Answers