Let's say I want to define a potentially infinite list of computation as a data type. So that the computation could be
fun a -> a' =
Just a' || fun (a -> a')
|| fun (a -> b) >>= (fun b -> a')
|| fun (a -> b) >>= (fun b -> c ) >>= fun (c -> a')
|| ...
The point is that the function takes in input of type a and outputs type a', but in between, there could be an unbounded discrete number of intermediate computations, where each subsequent computation consumes the output of the previous computation.
I'm trying to visualize this as a data structure of some kind, but it does not quite look like a tree (or a an "imbalanced list.") And how does one account for the arbitrary number of types b,c,d,e... that represent the type of the intermediate output of the computation?
P.S. In the answer please write out what the datatype would be, as opposed to something like effectful list (a -> a') or some generic answer.
A free category over arr is a list of arrows arr a b where the output type b of each arrow matches the input type of the next arr b c.
data FreeCat (arr :: k -> k -> Type) (a :: k) (b :: k) where
Id :: FreeCat arr a a
(:>>>) :: arr a b -> FreeCat arr b c -> FreeCat arr a c
infixr 4 :>>>
One possible specialization of this type is with arr = Kleisli m, which lets you build a list of arrows of type a -> m b:
type FreeKleisli m = FreeCat (Kleisli m)
mkFreeKleisli4 :: (a -> m b) -> (b -> m c) -> (c -> m d) -> (d -> m e) -> FreeKleisli m a e
mkFreeKleisli4 f g h i = Kleisli f :>>> Kleisli g :>>> Kleisli h :>>> Kleisli i :>>> Id
A specialized version of FreeKleisli is:
data FreeKleisli m a b where
Id :: FreeKleisli m a a
(:>=>) :: (a -> m b) -> FreeKleisli m b c -> FreeKleisli m a c