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…

Accepted Answer

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.

Juggling existentials without unsafeCoerce

Solution

Problem

Related problems