Type system algebra - use of derivation

Question

I remember a web page describing interesting techniques in relation with some functional-programming task. The problem is that I can't remember what it was.

It had a binary tree node (Tree left, Tree right, Data d) as an example, which could be described as Tree*Tree*Data, or Tree^2*Data. Then when deriving for example by Tree, we get 2*Tree*Data.

Could you point me to what this is used for?

Answer 1

Sounds like a Zipper.

To follow up: the mantra for this sort of thing is that "the derivative of a type is its one-hole context". The idea being that if you want to represent a binary tree with one spot where you would like to do an insertion, well the data structure for that is precisely a path from the hole up to the root of the tree and at each node going up you have to remember whether you came from the left or the right as well as the data at that node as well as it's subtree that you didn't come from. well that's precisely the tuple of 2 (aka left/right) * Data * Tree.