Juggling existentials without unsafeCoerce

Question

Lately I have been playing with this type, which I understand to be an encoding of the free distributive functor (for tangential background on that, see this answer):

data Ev g a where
    Ev :: ((g x -> x) -> a) -> Ev g a

deriving instance Functor (Ev g)

The existential constructor ensures I can only consume an Ev g by supplying a polymorphic extractor forall x. g x -> x, and that the lift and lower functions of the free construction can be given compatible types:

runEv :: Ev g a -> (forall x. g x -> x) -> a
runEv (Ev s) f = s f

evert :: g a -> Ev g a
evert u = Ev $ \f -> f u

revert :: Distributive g => Ev g a -> g a
revert (Ev s) = s <$> distribute id

However, there is a difficulty upon trying to give Ev g a Distributive instance. Given that Ev g is ultimately just a function with a weird argument type, one might hope that just threading distribute for functions (which amounts to (??) :: Functor f => f (a -> b) -> a -> f b from lens, and doesn't inspect the argument type in any way) through the Ev wrapper:

instance Distributive (Ev g) where
    distribute = Ev . distribute . fmap (\(Ev s) -> s)

That, however, does not work:

Flap3.hs:95:53: error:
    • Couldn't match type ‘x’ with ‘x0’
      ‘x’ is a rigid type variable bound by
        a pattern with constructor:
          Ev :: forall (g :: * -> *) x a. ((g x -> x) -> a) -> Ev g a,
        in a lambda abstraction
        at Flap3.hs:95:44-47
      Expected type: (g x0 -> x0) -> a
        Actual type: (g x -> x) -> a
    • In the expression: s
      In the first argument of ‘fmap’, namely ‘(\ (Ev s) -> s)’
      In the second argument of ‘(.)’, namely ‘fmap (\ (Ev s) -> s)’
    • Relevant bindings include
        s :: (g x -> x) -> a (bound at Flap3.hs:95:47)
   |
95 |     distribute = Ev . distribute . fmap (\(Ev s) -> s) 
   |                                                     ^
Failed, no modules loaded.

GHC objects to rewrapping the existential, even though we do nothing untoward with it between unwrapping and rewrapping. The only way out I found was resorting to unsafeCoerce:

instance Distributive (Ev g) where
    distribute = Ev . distribute . fmap (\(Ev s) -> unsafeCoerce s)

Or, spelling it in a perhaps more cautious manner:

instance Distributive (Ev g) where
    distribute = eevee . distribute . fmap getEv
        where
        getEv :: Ev g a -> (g Any -> Any) -> a
        getEv (Ev s) = unsafeCoerce s
        eevee :: ((g Any -> Any) -> f a) -> Ev g (f a)
        eevee s = Ev (unsafeCoerce s)

Is it possible to get around this problem without unsafeCoerce? or there truly is no other way?

Additional remarks:

• I believe Ev is the most correct type I can give to the construction, though I would be happy to be proved wrong. All my attempts to shift the quantifiers elsewhere lead either to needing unsafeCoerce somewhere else or to evert and revert having types that don't allow them to be composed.

• This situation looks, at first glance, similar to the one described in this blog post by Sandy Maguire, which ends up sticking with unsafeCoerce as well.

---

The following take at giving Ev g a Representable instance might put the problem into sharper relief. As dfeuer notes, this isn't really supposed to be possible; unsurprisingly, I had to use unsafeCoerce again:

-- Cf. dfeuer's answer.
newtype Goop g = Goop { unGoop :: forall y. g y -> y }

instance Representable (Ev g) where
    type Rep (Ev g) = Goop g
    tabulate f = Ev $ \e -> f (Goop (goopify e))
        where
        goopify :: (g Any -> Any) -> g x -> x
        goopify = unsafeCoerce
    index (Ev s) = \(Goop e) -> s e

While goopify sure looks alarming, I think there is a case for it being safe here. The existential encoding means any e that gets passed to the wrapped function will necessarily be an extractor polymorphic on the element type, that gets specialised to Any merely because I asked for that to happen. That being so, forall x. g x -> x is a sensible type for e. This dance of specialising to Any only to promptly undo it with unsafeCoerce is needed because GHC forces me to get rid of the existential by making a choice. This is what happens if I leave out the unsafeCoerce in this case:

Flap4.hs:64:37: error:
    • Couldn't match type ‘y’ with ‘x0’
      ‘y’ is a rigid type variable bound by
        a type expected by the context:
          forall y. g y -> y
        at Flap4.hs:64:32-37
      Expected type: g y -> y
        Actual type: g x0 -> x0
    • In the first argument of ‘Goop’, namely ‘e’
      In the first argument of ‘f’, namely ‘(Goop e)’
      In the expression: f (Goop e)
    • Relevant bindings include
        e :: g x0 -> x0 (bound at Flap4.hs:64:24)
   |
64 |     tabulate f = Ev $ \e -> f (Goop e) 
   |                                     ^
Failed, no modules loaded.

---

Prolegomena needed to run the code here:

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Distributive
import Data.Functor.Rep
import Unsafe.Coerce
import GHC.Exts (Any)

-- A tangible distributive, for the sake of testing.
data Duo a = Duo { fstDuo :: a, sndDuo :: a }
    deriving (Show, Eq, Ord, Functor)

instance Distributive Duo where
    distribute u = Duo (fstDuo <$> u) (sndDuo <$> u)

Azotemia

"The existential constructor ensures I can only consume an Ev g by supplying a polymorphic extractor" Perhaps you could make that more explicit, like Ev :: ((forall x . g x -> x) -> a) -> Ev g a. Such definition makes the definition distribute wrapped = Ev (\f -> fmap (\(Ev z) -> z f) wrapped) compile for me, although it breaks the generic deriving of Functor for some reason. – Conventicle

@Conventicle The problem with doing it that way is that it stops revert from typechecking, as distribute id :: g (g a -> a) won't be polymorphic enough to map the wrapped function over it. – Azotemia

Is fmap (\(Ev s) -> s) really something sensible to do? The object you are fmap-ing over could contain many Ev (say, fmap = map), each with its own existentially quantified x. – Isoagglutinin

For reference, the foolproof, (almost-)certainly-correct free Distributive is Ev g a = (forall g'. Distributive g' => (forall x. g x -> g' x) -> g' a), but I don't think that helps in making your Ev work. – Parous

@Li-yaoXia I think it is sensible. x does not appear in a "strictly positive" position, so it seems that any such differences won't be observable. For instance [Ev (\e -> show . e $ Duo 1 2), Ev (\e -> e $ Duo "foo" "bar")] typechecks as Ev Duo String and works just fine. (Note that I must straighten out the result types of the suspensions to String.) – Azotemia

@Parous Yup -- that would be the final form, if my terminology is right. It does seem to be isomorphic to Ev: toEvFinal (Ev s) = EvFinal $ \n -> revert (Ev (s . (. n))) and fromEvFinal (EvFinal s) = s evert. – Azotemia

I think it's just as good to use @danidiaz's representation with unsafeCoerce in revert. This avoids using data to wrap a function. As you say, distribute id :: forall x. g (g x -> x) is insufficiently polymorphic, but you can do the same thing: specialize to x ~ Any and coerce under the fmap. – Faenza

@DanielWagner The xes are behind a function arrow, so the secretly wrapped values aren't really of x type; they merely dictate a specialisation of a polymorphic x. The customary trick is to encode existential quantification with universal quantification. If I understand it correctly, I have done it twice here, which would make it become universal again. – Azotemia

@Faenza Well-spotted! It seems another advantage of doing it this way is that it reduces the number of places unsafeCoerce is necessary, assuming there really is no way to get rid of it altogether. Auspiciously, neither the Distributive instance nor the Representable one requires a further unsafeCoerce. – Azotemia

@Conventicle Your intuition was sound after all. I thank both you and dfeuer for my self-answer here. – Azotemia

Answer 1

The suggestions by danidiaz and dfeuer have led me to a tidier encoding, though unsafeCoerce is still necessary:

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}

import Unsafe.Coerce
import GHC.Exts (Any)
import Data.Distributive
import Data.Functor.Rep

-- Px here stands for "polymorphic extractor".
newtype Px g = Px { runPx :: forall x. g x -> x }

newtype Ev g a = Ev { getEv :: Px g -> a }
    deriving Functor

runEv :: Ev g a -> (forall x. g x -> x) -> a
runEv s e = s `getEv` Px e

evert :: g a -> Ev g a
evert u = Ev $ \e -> e `runPx` u

revert :: Distributive g => Ev g a -> g a
revert (Ev s) = (\e -> s (mkPx e)) <$> distribute id
    where
    mkPx :: (g Any -> Any) -> Px g
    mkPx e = Px (unsafeCoerce e) 

instance Distributive (Ev g) where
    distribute = Ev . distribute . fmap getEv

instance Representable (Ev g) where
    type Rep (Ev g) = Px g
    tabulate = Ev 
    index = getEv

The x variable in my original formulation of Ev was, at heart, being universally quantified; I had merely disguised it as an existential behind a function arrow. While that encoding makes it possible to write revert without unsafeCoerce, it shifts the burden to the instance implementations. Directly using universal quantification is ultimately better in this case, as it keeps the magic concentrated in one place.

The unsafeCoerce trick here is essentially the same demonstrated with tabulate in the question: the x in distribute id :: Distributive g => g (g x -> x) is specialised to Any, and then the specialisation is immediately undone, under the fmap, with unsafeCoerce. I believe the trick is safe, as I have sufficient control over what is being fed to unsafeCoerce.

As for getting rid of unsafeCoerce, I truly can't see a way. Part of the problem is that it seems I would need some form of impredicative types, as the unsafeCoerce trick ultimately amounts to turning forall x. g (g x -> x) into g (forall x. g x -> x). For the sake of comparison, I can write a vaguely analogous, if much simpler, scenario using the subset of the impredicative types functionality that would fall under the scope of the mooted ExplicitImpredicativeTypes extension (see GHC ticket #14859 and links therein for discussion):

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE RankNTypes #-}

newtype Foo = Foo ([forall x. Num x => x] -> Int)

testFoo :: Applicative f => Foo -> f Int
testFoo (Foo f) = fmap @_ @[forall x. Num x => x] f 
    $ pure @_ @[forall x. Num x => x] [1,2,3]

GHCi> :set -XImpredicativeTypes 
GHCi> :set -XTypeApplications 
GHCi> testFoo @Maybe (Foo length)
Just 3

distribute id, however, is thornier than [1,2,3]. In id :: g x -> g x, the type variable I'd like to keep quantified appears in two places, with one of them being the second type argument to distribute (the (->) (g x) functor). To my untrained eye at least, that looks utterly intractable.

Azotemia

The only open question, I think, is whether distribute with something other than reader could somehow do the trick.... Seems unlikely, but I dunno how to demonstrate it's impossible. – Faenza

@Faenza At times, I have wondered if there might be an alternative encoding of the free distributive/representable that would allow for something different -- which sounds similarly unlikely. – Azotemia

Answer 2

Every Distributive functor can be made Representable, though we can't prove that in Haskell (I imagine it's not constructive). But one approach to addressing your problem is to just switch classes.

newtype Evv f a = Evv
  {unEvv :: forall g. Representable g
         => (forall x. f x -> g x) -> g a}

instance Functor (Evv g) where
  fmap f (Evv q) = Evv $ \g -> fmap f (q g)

evert :: g a -> Evv g a
evert ga = Evv $ \f -> f ga

revert :: Representable g => Evv g a -> g a
revert (Evv f) = f id

newtype Goop f = Goop
  {unGoop :: forall x. f x -> x}

instance Distributive (Evv g) where
  collect = collectRep

instance Representable (Evv g) where
  type Rep (Evv g) = Goop g
  tabulate f = Evv $ \g -> fmap (\rg -> f (Goop $ \fx -> index (g fx) rg)) $ tabulate id
  index (Evv g) (Goop z) = runIdentity $ g (Identity . z)

I haven't yet tried this with Distributive directly (as HTNW suggests), but I wouldn't be surprised if it were simply impossible for some reason.

Warning: I have not proven that this is actually the free Representable!

Faenza

This is not the same type? – Retake

This raises a relevant point: what I'm trying to do might perhaps be described as an attempt to conjure the representation for Distributive in Haskell. My type is, in spirit, Goop g -> a, though the quantifiers make a mess of it all. I have just attempted to write Representable (Ev g) for my type, with Rep (Ev g) = Goop g, and guess what: I needed unsafeCoerce for writing tabulate. It seems to work, though I'm slightly less certain of the soundness of this instance. – Azotemia

@AndrásKovács It is a different encoding, which sans the change of constraint is, as far as I can tell, isomorphic to mine. – Azotemia

@Azotemia I don't see how the original Ev g is representable. For many choices of g, Ev g a can contain anywhere from zero to infinite number of as, e.g. if g = []. – Retake

@AndrásKovács If g ~ [], Ev g a will contain no (observable) as, because strictly speaking there are no [a] -> a functions. – Azotemia

@Azotemia I was thinking about strong sigma types, but I think you're right in the current case with the weird weak existential elimination. – Retake

@duplode, for what it's worth, my type is just a convoluted version of the one danidiaz suggests: newtype Ev g a = Ev ((forall x . g x -> x) -> a). What you won't like is that revert sure seems to need a Representable constraint. – Faenza