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

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.

• @plshelp How would that help, given that I am working with tuples and not lists? In particular, the tuples contain expressions of different types. Aug 15 '20 at 16:30
• Either your language must have an operation that extends tuples, or you must model extendable tuples via existing structures. (For example, (c, (b, a)) instead of (c, b, a)). Aug 18 '20 at 14:21
• This sounds like an indexed analogue of a writer monad, if we have a graded monoid such as that of sequences of specific length, and make an indexed monad out of it? Aug 22 '20 at 14:01
• @mniip: Would you mind writing up your statement as an answer, since I am not sure what you mean? Aug 22 '20 at 15:22

(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).

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

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

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)