tag:blogger.com,1999:blog-8068466035875589791.post2815069037555256820..comments2018-12-11T06:56:49.690-08:00Comments on Semantic Domain: A Computational Lambda Calculus for Applicative FunctorsNeelakantan Krishnaswaminoreply@blogger.comBlogger4125tag:blogger.com,1999:blog-8068466035875589791.post-64147235806220772692016-05-15T20:28:40.283-07:002016-05-15T20:28:40.283-07:00Excellent post! Thanks.
Question: Do you happen t...Excellent post! Thanks.<br /><br />Question: Do you happen to know of any generalization that need not require the functor to be an endo- one.<br /><br />TnanksUnknownhttps://www.blogger.com/profile/09023526063016882361noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-7051006505604534552013-05-01T20:04:42.165-07:002013-05-01T20:04:42.165-07:00This comment has been removed by the author.Arseniy Alekseyevhttps://www.blogger.com/profile/12270557237981980754noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-37183577239038821612012-08-23T05:08:30.919-07:002012-08-23T05:08:30.919-07:00Your suggestion is likely to work type-theoretical...Your suggestion is likely to work type-theoretically, and is close to the syntax that McBride and Patterson proposed. <br /><br />However, it's not clear to me that the two systems are equivalent, at least in the simply-typed case. I can see how to send A -F→ B to F(A) → B and then use the encoding you suggest. But I don't see how we would show the other direction of equivalence in the simply-typed case, though -- I don't see how to translate F(b), where b is a base type, to a type in the "applicative arrow" langauge. However, if you have F-style polymorphism, then I think it's equivalently powerful -- F(A) can pretty clearly be encoded as ∀α. (A -F→ α) → α. <br /><br />More on your other questions later...Neel Krishnaswamihttps://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-83473851912279499702012-08-23T02:07:05.454-07:002012-08-23T02:07:05.454-07:00Let me begin with a minor point: how dare you writ...Let me begin with a minor point: how dare you write "Delta; Gamma"? Delta is immediately next to Gamma in the greek alphabet, and writing them in reverse order is just *perverse*.<br /><br />Would it be possible to give a presentation centered not on a "let" binding, but on a lambda-inspired abstraction form? I'm thinking of introducing in your logic an applicative arrow (A -F-> B), along with elimination and introduction terms (a @F b) and (lamF x. a), such that (let val u = a in b) would desugar into ((lamF x. b) @F a).<br /><br />I'm under the impression that the eta-reduction rule for such a system would be more natural -- the current "let val" form has this annoying likeness with sum types that the elimination rule must come up with an arbitrary result type C. But it may also very well not work at all (your system has a feeling of modal logic that are usually formulated in let-style, there must be a reason).<br /><br />Finally, I miss a more detailed comparison with "monads": "applicative functors are more general" is well-known, but could you explicitly point out the difference between lax monoidal endomorphism and an endormorphism that is only a monoid? How would you change your type theory to capture one for monads?gaschehttps://www.blogger.com/profile/06100241581708586136noreply@blogger.com