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

3
votes

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.

2
haskellexistential-type
If you type it as hide :: (forall a. f a -> g (q a)) -> Some f -> Some g, doesn't type checks but that might not be as general as you're looking for (you can't use it when q ~ Id, where type Id a = a for instance). – David Young
@DavidYoung I'll try that and see how I go; I wouldn't like it so much as a combinator to expose to users of my library, but it may well meet most of my internal needs (since to be sufficiently polymorphic in a, I'm usually just wrapping it something else polymorphic). – Ben
Also, I'm not sure if any of this would help out much with this problem, but this kinda thing reminds me a lot of this package I'm starting to develop for working with existentials (mostly focused on lists of existentials right now though): github.com/roboguy13/anylist. The stuff that's commented out at the bottom is probably most likely to apply to this (in particular, I'm thinking of the Existential instance of the polykinded Functor class), but it probably isn't functional yet (but I don't totally remember). – David Young

2 Answers

4
votes

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
2
votes

I'm not sure how useful this is for your larger use-case as you'd have to refactor all your existing operations to use continuation passing style, but continuations can be used to implement a hide that works for both of your examples and keeps b completely generic.

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

cast :: Phantom a -> (forall b. Phantom b -> r Phantom) -> r Phantom
cast Phantom f = f Phantom

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

alsoWorks :: Functor f => Some f -> Some f
alsoWorks = hide (\a f -> f $ fmap (\x -> [x]) a)

You can make it somewhat nicer by factoring out the CPS-conversion which allows you to more easily use existing functions like your original cast:

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

cps :: (f a -> g b) -> (f a -> (forall c. g c -> r) -> r)
cps f a c = c (f a)

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

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

alsoWorks :: Functor f => Some f -> Some f
alsoWorks = hide $ cps $ fmap (\x -> [x])