Juggling existentials without unsafeCoerce
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.
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
!