Last active
January 24, 2019 09:21
-
-
Save KingoftheHomeless/e8a32db638a67f0223081283bc97fe34 to your computer and use it in GitHub Desktop.
The Cofree Traversable
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE GADTs, RankNTypes, DeriveFunctor, DeriveFoldable, StandaloneDeriving, ScopedTypeVariables #-} | |
module CofreeTraversable where | |
import Control.Applicative | |
import Data.Traversable | |
import Data.Functor.Identity | |
import Data.Functor.Compose | |
import Data.Coerce | |
import Unsafe.Coerce | |
{- | |
The Cofree Traversable of 'f' is a functor 'CFT f' such that | |
- There exists the natural transformation 'CFT f ~> f' | |
- Given a natural transformation 't ~> f', where 't' is Traversable, | |
you can get a traversable homomorphism 't ~> CFT f' | |
A traversable homomorphism, which I just made up, is a natural transformation | |
(Traversable f, Traversable g) => (forall x. f x -> g x) | |
such that for all ta, f: | |
nat <$> traverse f ta == traverse f (nat ta) | |
Intuitively, this means that the natural transformation preserves the elements of the traversable and their order. | |
A potential use for this construction is to (in practice) create a "local" Traversable instance for a particular value of a functor 'f a' | |
by using fromTraversal (converting it back using fromCFT when needed.) | |
-} | |
type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t | |
-- Final Encoding -- | |
data CFTFinal f a where | |
CFTFinal :: Traversable t => (forall x. t x -> f x) -> t a -> CFTFinal f a | |
deriving instance Functor (CFTFinal f) | |
deriving instance Foldable (CFTFinal f) | |
instance Traversable (CFTFinal f) where | |
traverse f (CFTFinal nat ta) = CFTFinal nat <$> traverse f ta | |
toCFTFinal :: Traversable f => f a -> CFTFinal f a | |
toCFTFinal = CFTFinal id | |
fromCFTFinal :: CFTFinal f a -> f a | |
fromCFTFinal (CFTFinal nat ta) = nat ta | |
-- fromTraversalFinal is forced to use some other representation of the Cofree Traversable. Is there some way to fix that? | |
-- 'tr' does not need to be a legal traversal for the resulting 'CFTFinal f' to be a legal traversable, but if it is, you | |
-- get some nice properties, like: | |
-- fromCFTFinal . fromTraversalFinal tr == id | |
fromTraversalFinal :: (forall b. Traversal (f a) (f b) a b) -> f a -> CFTFinal f a | |
fromTraversalFinal tr ta = CFTFinal fromCFTBazaar (fromTraversalBazaar tr ta) | |
-- Given a natural transformation from a traversable 't' to 'f', you get a traversable homomorphism from 't' to 'CFTFinal f' | |
unfoldCFTFinal :: Traversable t => (forall x. t x -> f x) -> t a -> CFTFinal f a | |
unfoldCFTFinal = CFTFinal | |
hoistCFTFinal :: (forall x. f x -> g x) -> CFTFinal f a -> CFTFinal g a | |
hoistCFTFinal nat (CFTFinal nat' ta) = CFTFinal (nat . nat') ta | |
-- FunList encoding -- | |
data FunList a b t | |
= Done t | |
| More a (FunList a b (b -> t)) | |
deriving (Functor) | |
fpure :: a -> FunList a b b | |
fpure a = More a (Done id) | |
fextract :: FunList a a t -> t | |
fextract (Done t) = t | |
fextract (More a r) = fextract r a | |
instance Applicative (FunList a b) where | |
pure = Done | |
Done f <*> fa = fmap f fa | |
More a r <*> fa = More a (liftA2 flip r fa) | |
newtype CFTFunList f a = CFTFunList { runCFTFunList :: forall b. FunList a b (f b) } | |
instance Functor (CFTFunList f) where | |
fmap = fmapDefault | |
instance Foldable (CFTFunList f) where | |
foldMap = foldMapDefault | |
endof :: FunList a b (b -> r b) -> FunList a b (EndoF r b) | |
endof = coerce | |
unendof :: forall a r b. (FunList a b (EndoF r b)) -> FunList a b (b -> r b) | |
unendof = coerce | |
newtype EndoF f a = EndoF { runEndoF :: a -> f a } | |
-- This instance is a convoluted mess, but shows that a Traversable instance really is possible without unsafeCoerce for this representation. | |
-- Of course, you can use the same method CFTBazaar uses instead. | |
instance Traversable (CFTFunList f) where | |
traverse (f :: a -> g b) ft = go CFTFunList (runCFTFunList ft) | |
where | |
-- Pattern matching on (forall x. FunList a x (t x)) instantiates the x | |
-- to (some ambiguous) variable, rather than preserving the quantification. | |
-- These functions are a workaround for that. | |
_done :: FunList x y t -> t | |
_done ~(Done t) = t | |
_more :: FunList x y t -> FunList x y (y -> t) | |
_more ~(More _ r) = r | |
go :: ((forall x. FunList b x (r x)) -> h b) -> (forall x. FunList a x (r x)) -> g (h b) | |
go t g = case g of | |
Done _ -> pure (t (Done (_done g))) | |
More a _ -> liftA2 (\a' f' -> (coerce f') a') (f a) (go (\r -> EndoF $ \x -> t (More x (unendof r))) (endof (_more g))) | |
fromCFTFunList :: CFTFunList f a -> f a | |
fromCFTFunList cft = fextract (runCFTFunList cft) | |
toCFTFunList :: Traversable f => f a -> CFTFunList f a | |
toCFTFunList ta = CFTFunList (traverse fpure ta) | |
-- | Given a natural transformation from a traversable 't' to 'f', you get a traversable homomorphism from 't' to 'CFTFunList f' | |
unfoldCFTFunList :: Traversable t => (forall x. t x -> f x) -> t a -> CFTFunList f a | |
unfoldCFTFunList nat ta = CFTFunList (nat <$> traverse fpure ta) | |
hoistCFTFunList :: (forall x. f x -> g x) -> CFTFunList f a -> CFTFunList g a | |
hoistCFTFunList nat (CFTFunList ft) = CFTFunList (fmap nat ft) | |
-- Bazaar encoding -- | |
newtype Bazaar a b t = Bazaar { runBazaar :: forall f. Applicative f => (a -> f b) -> f t } | |
deriving (Functor) | |
bpure :: a -> Bazaar a b b | |
bpure a = Bazaar (\c -> c a) | |
bextract :: Bazaar a a t -> t | |
bextract baz = runIdentity (runBazaar baz Identity) | |
instance Applicative (Bazaar a b) where | |
pure a = Bazaar $ \_ -> pure a | |
ff <*> fa = Bazaar $ \c -> runBazaar ff c <*> runBazaar fa c | |
newtype CFTBazaar f a = CFTBazaar { runCFTBazaar :: forall g b. Applicative g => (a -> g b) -> g (f b) } | |
deriving (Functor) | |
instance Foldable (CFTBazaar f) where | |
foldMap (f :: a -> m) bz = getConst (runCFTBazaar bz (coerce f :: a -> Const m b)) | |
instance Traversable (CFTBazaar f) where | |
traverse (f :: a -> g b) bz = conversion $ getCompose $ runCFTBazaar bz (Compose . fmap bpure . f) | |
where | |
conversion :: (forall x. g (Bazaar b x (f x))) -> g (CFTBazaar f b) | |
conversion (g :: g (Bazaar b x (f x))) = (unsafeCoerce :: Bazaar b x (f x) -> CFTBazaar f b) <$> g | |
-- Lack of impredicative types makes unsafeCoerce necessary. | |
-- I'm 90% sure that parametricity means that the unsafeCoerce is safe in this context, even with GADTs, | |
-- since GADTs can't use type-specialized constructors for a fmap. | |
-- It would be nice not to need it though. | |
toCFTBazaar :: Traversable f => f a -> CFTBazaar f a | |
toCFTBazaar fa = CFTBazaar (`traverse` fa) | |
fromCFTBazaar :: CFTBazaar f a -> f a | |
fromCFTBazaar baz = runIdentity (runCFTBazaar baz Identity) | |
fromTraversalBazaar :: (forall b. Traversal (f a) (f b) a b) -> f a -> CFTBazaar f a | |
fromTraversalBazaar tr ta = CFTBazaar (`tr` ta) | |
-- Given a natural transformation from a traversable 't' to 'f', you get a traversable homomorphism from 't' to 'CFTBazaar f' | |
unfoldCFTBazaar :: Traversable t => (forall x. t x -> f x) -> t a -> CFTBazaar f a | |
unfoldCFTBazaar nat ta = CFTBazaar $ \c -> nat <$> traverse c ta | |
hoistCFTBazaar :: (forall x. f x -> g x) -> CFTBazaar f a -> CFTBazaar g a | |
hoistCFTBazaar nat bz = CFTBazaar $ \c -> nat <$> runCFTBazaar bz c |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment