# Is it possible to 'uncurry' a forall quantifier?

4

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

6

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)
``````