Comments for The Comonad.Reader

Comment on Abstracting with Applicatives by Edward Z. Yang

Edward Z. Yang — Sat, 29 Dec 2012 15:18:06 +0000

Cool post, reminds me about a similar observation I made about the writer monad (http://blog.ezyang.com/2012/10/generalizing-the-programmable-semicolon/); namely, that the tracing behaviour of writer is independent of the computational component.

Comment on Abstracting with Applicatives by Gershom Bazerman

Gershom Bazerman — Thu, 27 Dec 2012 17:45:23 +0000

Thanks for the comments — I’ve fixed the post appropriately. I came across “Sum” on my own, and I wasn’t familiar with the “Lift” specialization of it in transformers. Not surprised that Conor and Ross beat me to it!

As the edited post notes, we can’t actually add that Identity instance for Natural without overlapping too often with the Const instance. The poor typechecker can’t decide if it should send everything to Const, or Identity to anything.

Comment on Abstracting with Applicatives by Oliver Charles

Oliver Charles — Thu, 27 Dec 2012 16:53:09 +0000

In the example of the FailingWriter, you write ‘runFailingWriter $ …’, but don’t provide a definition of it. From the actual output, I don’t think you actually meant to write it, as the current output makes it seem that the definition would just be `id`. Or perhaps you meant to provide a definition that would yield a different output, perhaps (monoid, Maybe a), stripping away the newtype noise?

Comment on Abstracting with Applicatives by Sjoerd Visscher

Sjoerd Visscher — Thu, 27 Dec 2012 10:05:29 +0000

Great article!

I came across the Sum applicative for the first time just two days ago in this comment on Stack Overflow by Conor McBride [1]. There he notes Identity is the initial Applicative functor, so you can replace that last Natural instance with:

instance Applicative g => Natural Identity g where
eta (Identity x) = pure x

[1] http://stackoverflow.com/questions/14022791/what-is-control-applicative-lift-useful-for/14022871#comment19369023_14022871

Comment on Abstracting with Applicatives by Edward Kmett

Edward Kmett — Thu, 27 Dec 2012 01:52:27 +0000

Const c >>= f doesn’t work

return a >>= f = f a is a Monad law.

Consider:

return a >>= \ _ -> Const “hello”

But from that definition

return a >>= \ _ -> Const “hello” = Const “”

but

(\ _ -> Const “hello”) a = Const “hello”

Your proposal only works when mempty is the only value of your monoid. It works for Const (), but nothing else really.

Comment on Abstracting with Applicatives by Luke Palmer

Luke Palmer — Thu, 27 Dec 2012 01:46:22 +0000

Oh, I see. You couldn’t define bind in a way that is consistent with the Applicative instance (and we had Monoid c anyway so return wouldn’t have been a problem). Sloppy reading :-/

Comment on Abstracting with Applicatives by Luke Palmer

Luke Palmer — Thu, 27 Dec 2012 01:43:23 +0000

It seems to me that the reason that Const c is not a monad is because of return, not bind. Const c >>= f = Const c should do the trick.

Comment on Natural Deduction, Sequent Calculus and Type Classes by Riccardo

Riccardo — Fri, 21 Dec 2012 01:53:52 +0000

Not sure if this respects the implicit assumptions that you have in mind, but if you’re willing to change the syntax of your term language, you should be able to get more immediate correspondences between terms and the sequent calculus rules.

For instance, a term ‘let (y,z)=x in A’ corresponding to the AND-L rule, without requiring explicit substitution. This matches your intuitions about the pattern language, of course, but without relying on heavy pattern-based machinery.

IMP-L corresponds to the term ‘let r = (f A) in B’ where r and f are variables of the right type (f a function t(A) -> t(B), and r of type t(B)), etc.

You can define standard application as an abbreviation if you have local binding (which you should be able to get as term syntax for the CUT rule):

(A B) == let f = A in let r = (f B) in r

Details to be checked, of course, but back of the envelope, this might work.

Comment on Unnatural Transformations and Quantifiers by Alexandra

Alexandra — Thu, 13 Dec 2012 17:53:28 +0000

I really don’t like maths that much but it always fascinate me like magic. This site is very informative and useful for the maths students, so please keep updating.

Comment on Natural Deduction, Sequent Calculus and Type Classes by PhilipJF

PhilipJF — Mon, 10 Dec 2012 08:48:03 +0000

Another reason for the lack of the sequent calculus in programming languages, is that the elegance of the sequent calculus comes from having formula on the right of the turnstile (just like you can on the left). Just like you interpret the gamma on the left by “anding” all the formula together, you interpret the right as m-arry “or”. The “problem” with this is that if you do this you basically get the law of the excluded middle for free. Since ordinary functional programming is intuitionistic, this is a biy of a problem. Sequence calculus is only worth it if you have continuations.
Check out the work of Pierre-Louis Curien for some (classical) programming language work based in sequent calculus. I once implemented an interpretor (in Haskell) using Typed Higher Order Syntax and GADTS for the lambda mu mu tilde calculus, and found it to be actually relatively pleasant. Although, in practice I found it easiest to construct programs using the Hilbert style classical operators (S,K,I, and Peirce’s law), this was primarily because Haskell makes dealing with classical logic’s involutive negation a pain. Also, lambda mu mu tilde was meant as an intermediary language anyways–it has complex types because it is polarized (And focalized!) but this means you get both CBN and CBV function spaces.