> I believe the encoding was inspired by this paper
Just to add some tangential color here: even if you don't intend to use this encoding in production, it can be a fruitful intermediate step in refactoring! I just recently ran into a situation in Java where I had some tightly-coupled concerns for which HKTs were the obvious way out. Since Java doesn't have HKTs, I applied the HKT encoding to get the hard part out of the way, and then discovered a simplification that brought me back into the realm of idiomatic Java. I would not have found the final solution had I not pathed through HKTs -- I actually thought it would be impossible to do this decoupling properly at first!
More color: the paper itself describes this approach as an application of defunctionalization. I use defunctionalization a lot, too, to write an obvious recursive solution and then mechanically transform it into an iterative one. So it's nice to know how to apply it at the type level, too ;)
Just to add some tangential color here: even if you don't intend to use this encoding in production, it can be a fruitful intermediate step in refactoring! I just recently ran into a situation in Java where I had some tightly-coupled concerns for which HKTs were the obvious way out. Since Java doesn't have HKTs, I applied the HKT encoding to get the hard part out of the way, and then discovered a simplification that brought me back into the realm of idiomatic Java. I would not have found the final solution had I not pathed through HKTs -- I actually thought it would be impossible to do this decoupling properly at first!
More color: the paper itself describes this approach as an application of defunctionalization. I use defunctionalization a lot, too, to write an obvious recursive solution and then mechanically transform it into an iterative one. So it's nice to know how to apply it at the type level, too ;)