Creating a large tuple from smaller tuples via a monad or applicative

Question

Suppose I have a term $a :\alpha$ of the Simply-Typed Lambda Calculus (in the following, $\alpha, \beta, \gamma$ stand for arbitrary types) and I want to lift it to a term

$\lambda x_{\beta}. \;(x, \, a)$

I could use a function $\lambda z_{\alpha}, x. \;(x,\, z)$.

Suppose we then form $(b, a) : \beta \times \alpha$, by applying $\lambda x_{\beta}. \;(x, \, a)$ to $\,b_{\beta}$.

We might want to add $c$ to the beginning of this to form $(c, b, a) : \gamma \times \beta \times \alpha$. We could do this (here $\pi_1$ and $\pi_2$ are projections)) by having a function $\lambda z'_{\beta \times \alpha}, z. \,(z,\, \pi_1 z',\, \pi_2 z')$. And again, we could cook up a function to form $(d,\, c,\, b,\, a)$ and $(e,\,d,\, c,\, b,\, a)$ (so on and so forth).

I could do things in the way above; however, I wondered whether there was a way of doing this kind of operation via an applicative or a monad. Then I could (ideally) use the operations of the monad or applicative, to lift term $a$ (perhaps into $\lambda x.\,(x, \, a)$, and then form these tuples $(b, a), (c, b, a), (d, c, b, a)$, etc, by the operations of the monad or applicative.

If you know a way of doing this I would be very interested.

Answer 1

(Note, this requires a more sophisticated type theory such as System Fω to encode)

This idea is captured by the concept of an indexed monad (and in turn indexed applicative/functor).

Using Haskell as lingua franca, we talk about a typeclass:

class IxMonad (m :: n -> n -> * -> *) where                    
  ireturn :: a -> m i i a
  ibind :: m i j a -> (a -> m j k b) -> m i k b
  {- alternatively, if it's an IxFunctor, the categorical version:
  ireturn :: a -> m i i a
  ijoin :: m i j (m j k a) -> m i k a
  -}

An action m i j a makes a connection "from" an index i "to" an index j, and wraps some type a. Actions can be composed only if the respective indices "line up". Sort of like how horizontal oidification turns a monoid into a category: morphisms can be composed only if their endpoint objects "line up".

Analogous definitions of an indexed functor and an indexed applicative can be made:

class IxFunctor (m :: n -> n -> * -> *) where
  ifmap :: (a -> b) -> m i j a -> m i j b

class IxApplicative (m :: n -> n -> * -> *) where
  ipure :: a -> m i i a
  iap :: m i j (a -> b) -> m j k a -> m i k b
  {- alternatively, if it's an IxFunctor, the categorical version:
  iunit :: () -> m i i ()
  iprod :: (m i j a, m j k b) -> m i k (a, b)
  -}

Say we wanted to "output" entries of some type, while keeping a type-theoretic witness of how many entries there are, we could define an indexed writer monad.

Here's definitions of natural numbers used to track length, and a length-indexed "log" datatype:

data N = Z | S N

data Vec (n :: N) (a :: *) where
  Nil :: Vec 'Z a
  Cons :: a -> Vec n a -> Vec ('S n) a

In an indexed monad, the usual intuition is that the indices i/j describe the "state" of the system: an action brings the system from "state i" to "state j". Here we'll be using the index to track how many entries we've written to the "log", and for completely technical reasons (to do with making the typechecker happy in an easy way), the left index will be the output log length, and the right index will be the input log length:

type family Add (n :: N) (m :: N) :: N where
  Add 'Z m = m
  Add ('S n) m = 'S (Add n m)

data IxWriter w i j a where
  IxWriter :: Vec k w -> a -> IxWriter w (Add k i) i a

instance IxMonad (IxWriter w) where
  ireturn x = IxWriter Nil x
  ibind (IxWriter xs x) f = case f x of
    IxWriter fs y -> iwappend xs fs y
    where
      iwcons :: w -> IxWriter w i j a -> IxWriter w ('S i) j a
      iwcons p (IxWriter qs z) = IxWriter (Cons p qs) z

      iwappend :: Vec k1 w -> Vec k2 w -> a -> IxWriter w (Add k1 (Add k2 i)) i a
      iwappend (Cons p ps) qs z = iwcons p $ iwappend ps qs z
      iwappend Nil qs z = IxWriter qs z

Then we can define the "logging" action, and an interpreter for our effect:

itell :: Vec k w -> IxWriter w (Add k i) i ()
itell ps = IxWriter ps ()

runIxWriter :: IxWriter w i 'Z a -> (Vec i w, a)
runIxWriter (IxWriter Nil x) = (Nil, x)
runIxWriter (IxWriter (Cons p ps) x) = case runIxWriter (IxWriter ps x) of
  (qs, r) -> (Cons p qs, r)

With this we can keep track of exactly how many entries we've logged:

case runIxWriter $
  itell (Cons 1 Nil) `ibind` \_ -> itell (Cons 2 Nil) `ibind` \_ -> itell (Cons 3 Nil)
of (Cons a (Cons b (Cons c Nil)), x) -> (a, b, c, x)
{- pattern match is valid and complete because we
   statically know it's a Vec ('S ('S ('S 'Z))) Integer -}

Here we used the graded monoid of finite sequences (and thus all our logs are of the same type). In theory we could have used any monoid graded by any other monoid, (for example the monoid of heterogeneous lists, graded by the monoid of lists of types -- if we wanted to be able to talk about heterogeneous tuples)