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.

  • $\begingroup$ You could take a look at the haskell list monad and how its implemented: schoolofhaskell.com/school/starting-with-haskell/… $\endgroup$
    – plshelp
    Aug 15 '20 at 16:10
  • $\begingroup$ @plshelp How would that help, given that I am working with tuples and not lists? In particular, the tuples contain expressions of different types. $\endgroup$
    – user65526
    Aug 15 '20 at 16:30
  • $\begingroup$ 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)). $\endgroup$ Aug 18 '20 at 14:21
  • $\begingroup$ 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? $\endgroup$
    – mniip
    Aug 22 '20 at 14:01
  • $\begingroup$ @mniip: Would you mind writing up your statement as an answer, since I am not sure what you mean? $\endgroup$
    – user65526
    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).

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.