How to represent a potentially infinite list of computation as an algebraic datatype

How to represent a potentially infinite list of computation as an algebraic datatype

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.

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

Enjoyed this question?

Check out more content on our blog or follow us on social media.

Browse more questions