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