Natural transformations never need to type switch

opaque.hs

{-# LANGUAGE RankNTypes, TypeApplications #-}

-- We give a constructive proof that any natural transformation that uses
-- a type switch in its implementation can also be implemented without the type switch,
-- as long as the domain functor is finitely Traversable (and the argument can easily
-- be modified to drop the finiteness property).

-- We do this by providing a function `opaquify` which takes an n.t. which may do 
-- type switches, and returns an equivalent n.t. which does not. 

import qualified Control.Monad.Trans.State as State
import qualified Data.Map as Map
import Control.Arrow (second)


-- `label` labels all the "locations" in a functor with distinct integers, and
-- returns a map to get back from the integers to the original values.
-- 
-- N.B.: if (f', dict) = label f, then fmap (dict Map.!) f' = f
--
-- Should be clear enough by examination, assuming I didn't make a mistake.

label :: (Traversable f) => f a -> (f Integer, Map.Map Integer a)
label f = second snd (State.runState (traverse (State.state . go) f) (0, Map.empty))
    where
    go x (l, dict) = (l, (l+1, Map.insert l x dict))


-- `opaquify` takes a natural transformation which might have been defined
-- using type switch, and returns an identical transformation implemented without
-- type switch. 
--
-- The reason I claim `opaquify t` doesn't use type switch is because it only
-- instantiates `t` at the single type `Integer`, so no type magic has a chance to be used.
-- In other words, a natural transformation is completely determined by its behavior
-- instantiated at Integer.
--
opaquify :: (Traversable f, Functor g) => (forall a. f a -> g a) -> f a -> g a
opaquify t f = fmap (dict Map.!) . t @Integer $ f'
    where
    (f', dict) = label f

-- Theorem: if t is a natural transformation, then opaquify t = t
--
-- opaquify t f = fmap (dict Map.!) . t @Integer $ f'
--              = t @a . fmap (dict Map.!) $ f'   -- by t natural
--              = t f                             -- by `label` property above