Skip to content

Instantly share code, notes, and snippets.

@luqui
Last active May 23, 2020 08:09
Show Gist options
  • Save luqui/cd4dffc6908c7eeace3da91ec470327f to your computer and use it in GitHub Desktop.
Save luqui/cd4dffc6908c7eeace3da91ec470327f to your computer and use it in GitHub Desktop.
Natural transformations never need to type switch
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment