Monadic transform

Stream: general

[Wojciech Nawrocki]

Hello, this question is more about functional programming than Lean proper, but I thought here is still a good place to ask. Is the following "monadic transformation" typeclass a known thing?

class MonadicTransform (tag : Type) (m : Type → Type) [Monad m] (α β : Type) where
  transform : α → m β

variable {tag : Type} {m : Type → Type} [Monad m] {α β : Type}

instance [MonadicTransform tag m α β] : MonadicTransform tag m (Array α) (Array β) where
  transform as := as.mapM (@MonadicTransform.transform tag m _ α β _)

instance [MonadicTransform tag m α α'] [MonadicTransform tag m β β'] : MonadicTransform tag m (α × β) (α' × β') where
  transform := fun (a, b) => do
    let a' ← MonadicTransform.transform tag a
    let b' ← MonadicTransform.transform tag b
    return (a', b')

-- and so on, according to type structure

The intended use case, btw, is to define instances that do something special for a couple of base types and then have that propagate to all types (which needs metaprogramming in general but tuple/list/array is a good start). It is tagged because one may have multiple transformations in the same monad in general, though maybe putting that in the type signature is a bad idea. An alternative would be a "typeclass schema" generated via a metaprogram rather than using tags.

[Markus Himmel]

I'm not sure if this is helpful, but if I understand your definition correctly, the mathematicians' name for your concept is "a morphism in the Kleisli category".

[Wojciech Nawrocki]

Oh duh, of course, and maybe the tuple instance is even the binary product, though I didn't check. Thanks!

[Chris B]

It feels like traversable but I might be misunderstanding your goal.

[Wojciech Nawrocki]

Oh great, that does look like what I want. Thanks!