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?
ab ~ '(Fst ab, Snd ab)
, whereFst
andSnd
are the type-level projections. – pigworkerAny
strikes again. (Any :: (*, *)
but it is not the case thatAny ~ (a, b)
for anya
andb
.) – Daniel Wagnerforward
andbackward
functions? When would you want to use them? They just look like complicatedid
functions to me. – Alexis King