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.

]]>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

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.

]]>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.

]]>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. ]]>