Simon Willerton said:
> Firstly, you can't apply WorksIn to r.

Right, that's why I used lowercase letters! I have to admit it's a bit subtile, so here's it explicitly:

\\[ worksIn = F(WorksIn) \\]
\\[ WorksIn = G(worksIn) \\]

Just as is the case with \\(F\\) there is more than one \\(G\\), one for every type of object we want to map. \\(G\\) is similar to javascript's typeof builtin when applied to objects, but javascript's typeof cannot return function types. I would have liked to write \\(G = F^{op}\\) but that doesn't seem right as \\(F\\) doesn't reach all the way to particular data records, but \\(G\\) does. I'm not quite sure and am probably slightly confused here, but it seems what the book calls 'instance' isn't what a programmer might call by that name.

I know that theoreticians don't want to touch data records directly, because they want to reason about things that hold irrespective of any concrete values. But programmers who "feel" the machine may want to understand things more bottom up.

It took me a long time to get the advantage of doing things completely abstract.