data Free f a
= Pure a
| Free (Free f (f a)) deriving Functor
-- f (a -> b) -> a -> f b
(??) :: Functor f => f (a -> b) -> a -> f b
fab ?? a = fmap ($ a) fab -- Copied fro Control.Lens
instance Functor f => Applicative (Free f) where
pure = Pure
Pure g <*> x = g <$> x
Free g <*> x = Free $ ((??) <$> g) <*> x
This is similar to the Free monad, but reversed. Is it the free Applicative or something? It seems similar to one of the proposals of bound.
You can view the normal free monad as a kind of tree structure. If you use the functor f a = (a, a) then it actually is just a binary tree. Notably, this tree is not necessarily balanced.
If you use the same functor f a = (a, a) in your free-like structure then you get a classic nested data type encoding of perfect binary trees.
If you consider f = State s then your free-like structure is a stateful computation where you have to specify the exact number of put and get operations that you will use before hand. In the normal free monad you can use a different number of these operations based on the intermediate results of the operations.
For example you can write this program with Free, but not with your free-like structure:
countdown :: Free (State Int) ()
countdown = do
x <- get
when (x > 0) $ do
put (x - 1)
countdown
In this program the number of get and put operations depends on the value of the state you start with.
I guess what I’m looking for a connection with concepts I already have, like the Free monad and List. Does it show up anywhere else? Is it special case of a more complicated pattern? Is it usable for more than just variable names? I feel like if I get an answer to one of these, I’ll be able to understand it at a much deeper level than just knowing how it works for a few types.
Trees are not just a particular example. Basically all free monads are trees. For example you could write the countdown example like this:
import Numeric.Natural
import Control.Monad
data Tree a = Fork Natural [Tree a] | Leaf a deriving Functor
instance Applicative Tree where
pure = Leaf
(<*>) = ap
instance Monad Tree where
Leaf x >>= k = k x
Fork n xs >>= k = Fork n (map (>>= k) xs)
get :: Tree Natural
get = Fork 0 (map Leaf [0..])
put :: Natural -> Tree ()
put n = Fork (1 + n) [Leaf ()]
countdown :: Tree ()
countdown = do
x <- get
when (x > 0) $ do
put (x - 1)
countdown
You lose some type safety and performing the get operation now takes exponential time, but this essentially contains all the same information.
This is just the free monad on EnvT [] I guess my construction is just not that common, and doesn’t really have a deep meaning in category theory.
I used a similar structure to make the free traversal. I think that Traversal' one defined here is within Haskell 1998 specification.
applyF :: Functor f => f (a -> b) -> a -> f b
applyF f x = fmap ($ x) f
data Traversal' a b x t
= End x t
| Step (Traversal' a b (a,x) (b -> t)) deriving Functor
instance Bifunctor (Traversal' a b) where
first f (End x t) = End (f x) t
first f (Step f') = Step $ first (fmap f) f'
bimap f g = first f . fmap g
getTraversal' :: Traversal' a b (a,x) t -> (a,Traversal' a b x t)
getTraversal' (End (a,b) c) = (a, End b c)
getTraversal' (Step f) = case getTraversal' f of
(a,b) -> (a, Step b)
instance (x ~ ()) => Applicative (Traversal' a b x) where
pure x = End () x
End () f <*> c = fmap f c
Step f <*> c = Step $ first (a,) ((flip <$> x) <*> c) where
(a,x) = getTraversal' f
type Traversal s t a b = s -> Traversal' a b () t
type TraversalR s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
fromRank :: TraversalR s t a b -> Traversal s t a b
fromRank f s = f traversal s where
traversal :: a -> Traversal' a b () b
traversal a = Step $ End (a,()) id
withA :: forall f a b x t. Applicative f => (a -> f b) -> Traversal' a b x t -> f t
withA _ (End _ t) = pure t
withA f (Step tr) =
let (a, rest) = getTraversal' tr
in withA f rest <*> f a
toRank :: Traversal s t a b -> TraversalR s t a b
toRank f g s = withA g (f s)
It’s obviously really inneficient though, so it would be a poor substitute for the RankNType implementation of Traversal used by optics
I don’t really see how that structure is related to the other structures discussed in this thread.
The way I thought of it was this.
data Free0 f a = Pure0 a | Free0 (Free0 f (f a)) -- Original Free
data Free1 g f a = Pure1 (g a) | Free1 (Free1 g f (f a)) -- Compose with another functor
data Free2 g f f' a a' = Pure2 (g a a') | Free2 (Free2 g f f' (f a) (f' a')) -- Add another type parameter
type Traversal' a b x t = Free2 (,) ((,) a) ((->) b) x t
I thought Free2 and Free were very similar, and the Traversal' defined above could be implemented as a special case of Free2.
Here’s some playing around in a gist (I called it Gree).
It shows that to come from regular Free / have a Monad instance: you need to be able to peek under layers.
Yet another very related variant would be the following pairing:
data Spine f i o where
Z :: Spine f x x
S :: Spine f i (f o) -> Spine f i o
data Spree f z where
Spree :: Spine f i o -> i -> Spree f o
Same but different:
type Compositions :: Nat -> (Type -> Type) -> Type -> Type
type family Compositions n f x where
Compositions 0 f x = x
Compositions n f x = f (Compositions (n - 1) f x)
data Snee f z where
Snee :: SNat n -> Compositions n f x -> Snee f x
^ one fun thing about this one is that it’s on display that join follows addition of the nat.
…However, all these representations are generally a pain to work with 
.
TLDR, I gave up because there wasn’t anything particularly interesting that I could find.
Cool, that’s interesting to look at, but I guess I was wondering if there was some deeper way of thinking about this structure than just SNat n -> Compositions n f x -> Snee f x. I’m coming to terms with the fact that it’s not particularly special/important.
Side notes:
Adjunction f g requires f to be isomorphic to (c,) for some c. This also means that Gree f a is isomorphic to Free f a, (ignoring bottoms), as they are both ([c],a). As such, I that case isn’t that interesting. They are all a pain to work with though 
.
Here was my original use case:
data Reduction a b = End b | Step (Reduction a (Expr a -> b)) deriving Functor
Which is slightly annoying to work with, as it doesn’t permit analysis, but if I ever need that, I’ll just change it to Maybe. This is HOAS, but I think Gree is also similar to Bird and Paterson, Part 1 from here
Just mentioning it of a datatype defined similar to Gree that I’d seen before.