Mappers.idr

module Mappers

data Identity a = MkIdentity a

Functor Identity where
  map f (MkIdentity x) = MkIdentity (f x)

repapply : Nat -> (a -> a) -> (a -> a)
repapply Z f = id
repapply (S k) f = f . repapply k f

mapND : Functor f => (n: Nat) -> (a -> b) -> (repapply n f $ a) -> (repapply n f $ b)
mapND 0 g x = g x
mapND 1 g x = map g x
mapND (S k) g x = (map . mapND k) g x

Then I could do this:

Welcome to Idris 2.  Enjoy yourself!
1/1: Building Mappers (Mappers.idr)
Mappers> mapND 3 (+1) [[[1,2,3]]]
[[[2, 3, 4]]]
Mappers> mapND {f=Identity} 0 (+1) 123
124

Ooh, whoops, I shouldn't have specified {f=Identity} there, I think you can specify whatever you want! It's just that the type checker can't guess it for you, so you have to manually specify the implicit "forall Functor f." part.

mapND {f=List} 0 (+1) 123
124

Ok! Maybe this is a nicer/smaller version:

module Mappers

repapply : Nat -> (a -> a) -> (a -> a)
repapply Z f = id
repapply (S k) f = f . repapply k f

mapND : Functor f => (n: Nat) -> (a -> b) -> (repapply n f $ a) -> (repapply n f $ b)
mapND 0 g = g
mapND (S k) g = (map . mapND k) g