is there a framework or name for this pattern showing up in metalanguages: there is a "commutation" between e.g. representation of list of t, and list of representations of t: r (l t) <-> l (r t)
Conversation
this pattern pops up everywhere and seems to be related to things like loop transformations... basically talking about "intuitively these are the same, but you're going to have to do some work to translate manually"
1
also pops up in e.g. distributed computing. say machine A has input channel a, machine B has output channel b. there's a function f:a->b that can run on machine A or B. the same, conceptually, but impl is different.
1
not really sure where i'm going with this... just wondering if this rings a bell...
maybe a general idea of commutation of type constructors? something i don't know how to express in any language
Replying to
probably the thing that expresses why commutation works is the program you have to write, not something you can derive from some higher abstraction...