
Hi,all I'm studying `Algebra of Programming' written by Prof. Richard Bird. My question is for section 3.5 "Concatenation and currying > Exponentials". In page 74, he said ``` cat = (| curry ([outr, cons] . (id+id x apply) . (id+assocr) . distl) |) ``` where (| ... |) means banana operator. But I guess this left hand side `cat' is typo of `ccat` or `curry cat`? I think this is reasoned below. ----------------------------- cat . (alpha x id) = [outr, cons] . (id + id x cat) . phi <= page 73 start expr (maybe this is from equation (3.6)) = {- Theorem 3.1 precondition -} cat = apply . ( (| curry (h . G apply . phi |) x id) ----- (A) = {- on the other hand, exponential's universal property : g = curry f == apply . (g x id) = f -} cat = apply . ((curry cat) x id) ----- (B) = {- from (A) and (B) -} (curry cat) = (| curry (h . G apply . phi |) ----------------------------- This result is curry cat = (| curry ( [outr, cons] . (id + id x apply) . (id + assocr) . distl) |) not cat = rhs(above). How about this?
participants (1)
-
cutsea110