Skip to content

Instantly share code, notes, and snippets.

@cqfd
Created September 19, 2021 04:56
Show Gist options
  • Save cqfd/2aad2620db047ca91f92d64e742897d7 to your computer and use it in GitHub Desktop.
Save cqfd/2aad2620db047ca91f92d64e742897d7 to your computer and use it in GitHub Desktop.
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
@cqfd
Copy link
Author

cqfd commented Sep 19, 2021

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

@cqfd
Copy link
Author

cqfd commented Sep 19, 2021

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

@cqfd
Copy link
Author

cqfd commented Sep 19, 2021

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment