Bananas, Lenses, Envelopes, and Barbed Wire --- Section 3

Apparently the paper gives all it's definitions in terms of the category CPO (Complete Partial Orders); not entirely sure what the difference is between a complete and an incomplete partial-order is, so the signifigance probably escapes me. Alot of this section is also reminisent of Piece's Introduction to Category Theory, so I should probably go back and reread that.

Functors: I remember functors being fun reading in Pierce. In this case we are interested in bifunctors and monofunctors; being types into types and functions into functions; and just functions into functions respectively. Both cases preserve id and compose.

Products: Standard category fare. We have the bifunctor (at least I assume it's a bifunctor, the paper dosn't say, but it meets the defn' above) || which takes two types and maps to the type of pairs of those two types (the paper's example: D||D' = {(d,d') | d <- D, d <- D'} --- I'm using <- instead of the 'element of' symbol, I really need to get a better blog editor, one I can type symbols into easily; (f||g)(x,x') = (f x, g x') ) and the expected projection and tupling combinators.

Sum: Interesting, latent-typing as a functor, or at least something that looks like latent-typing to me. Also interesting to note the use of bottom (_|_) to include undecidability.

 D|D'          = ({tag0}||D}) U ({tag1}||D'}) U {_|_}
(f|g) _|_      = _|_
(f|g) (tag0,x) = (tag0, f x)
(f|g) (tag1,x) = (tag1, g x)

Also worth noting the injection and selection operators:

i0 x = ({tag0},x)
i1 y = ({tag1},y)
f v g --- which applies f to arguments tagged 0,
                and g to arguments tagged 1.

Arrow: Some type of 'wrapping' function. The example given is (f -> g) h = g $ h $ f. This suggests some sort of injection into f -> g, but I'm not entirely sure how. Apparently this is related to curry, uncurry, and eval, but again I don't see the relationship.

Identity, Constants: Pretty much as expected. Lifting and Sectioning, will require a little more thought.

Interesting definition of a constant as a function of 1 -> A. 1 of course having only a single member void. Also given p::A->bool, and p? a = i0 a or i1 a if p a is true/false respectively, you have f v g $ p? modeling if p then f else g.

The rest of section 3 easily exceeds my grasp of category theory. We define a representation for categorical recursion, then move on to recursive types, specifically the least-fixed-point of a monofunctor. Three examples given are cons-lists, binary trees, and natural numbers.

Having covered to background theory, the paper moves on to definitions of our operators over arbitary data types. That will have to wait until I've recovered from section 3 ;).