Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How can I apply an arbitrary function under an existential wrapper?

I'm trying to write a function (called hide here), which can apply a sufficiently polymorphic function inside an existential wrapper (or lift functions to work on wrappers with hidden types; hence "hide"):

{-# LANGUAGE GADTs
           , RankNTypes
  #-}

data Some f
  where Some :: f a -> Some f


hide :: (forall a. f a -> g b) -> Some f -> Some g
hide f (Some x) = Some (f x)


data Phantom a = Phantom

cast :: Phantom a -> Phantom b
cast Phantom = Phantom

works :: Some Phantom -> Some Phantom
works = hide cast


doesn't :: Functor f => Some f -> Some f
doesn't = hide (fmap $ \x -> [x])
{-
foo.hs:23:17:
    Couldn't match type ‘b0’ with ‘[a]’
      because type variable ‘a’ would escape its scope
    This (rigid, skolem) type variable is bound by
      a type expected by the context: f a -> f b0
      at foo.hs:23:11-33
    Expected type: f a -> f b0
      Actual type: f a -> f [a]
    In the first argument of ‘hide’, namely ‘(fmap $ \ x -> [x])’
    In the expression: hide (fmap $ \ x -> [x])
    In an equation for ‘doesn't’: doesn't = hide (fmap $ \ x -> [x])
Failed, modules loaded: none.
-}


but :: Functor f => Some f -> Some f
but = hide' (fmap $ \x -> [x])
  where hide' :: (forall a. f a -> g [a]) -> Some f -> Some g
        hide' f (Some x) = Some (f x)

So I pretty much understand why this is happening; works shows that hide does in fact work when the return type is completely unrelated to the input type, but in doesn't I'm calling hide with an argument of type a -> [a]. hide is supposed to get to "choose" the type a (RankNTypes), but b is ordinarily polymorphic. When b in fact depends on a, a could leak out.

But in the context where I'm actually calling it, a doesn't in fact leak out; I immediately wrap it up in Some. And in fact I can write an alternate hide' that accepts specifically a -> [a] functions and works with the exact same implementation, just a different type signature.

Is there any way I can type the implementation hide f (Some x) = Some (f x) so that it works more generally? Really I'm interested in lifting functions with type a -> q a, where q is some arbitrary type function; i.e. I expect the return type to depend on a, but I don't care how it does so. There probably are use cases where q a is a constant (i.e. the return type doesn't depend on a), but I imagine they'll be much rarer.

This example is pretty silly, obviously. In my real use case I have a GADT Schema a that roughly speaking represents types in an external type system; the phantom parameter gives a Haskell type that could be used to represent values in the external type system. I need that phantom parameter to keep everything type safe, but sometimes I construct Schemas based on runtime data, in which case I don't know what that parameter type is.

So I appear to need another type which is agnostic about the type parameter. Rather than make (yet) another parallel type, I was hoping to use a simple existential wrapper like Some to construct it from Schema, and be able to lift functions of type forall a. Schema a -> Schema b to Some Schema -> Some Schema. So if I have an XY problem and I'd be better of using some other means of passing around Schema a for unknown a, that would also solve my problem.

like image 940
Ben Avatar asked May 29 '26 10:05

Ben


1 Answers

As David Young says, you can write

hide' :: (forall a. f a -> g (q a)) -> Some f -> Some g
hide' f (Some x) = Some (f x)

does :: Functor f => Some f -> Some f
does = hide' (fmap (:[]))

but instead of making hide fmap-like, you can make it bind-like:

hide'' :: (forall a. f a -> Some g) -> Some f -> Some g
hide'' f (Some x) = f x

does :: Functor f => Some f -> Some f
does = hide'' (Some . fmap (:[]))

But this is a bit boilerplateable.

Or, more generally

elim :: (forall a. f a -> c) -> Some f -> c
elim f (Some x) = f x
like image 191
user3237465 Avatar answered May 31 '26 07:05

user3237465



Donate For Us

If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!