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

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.

By: danr

danr — Sun, 09 Dec 2012 10:41:30 +0000

Programming with type classes in Haskell is remniscent of programming in Prolog, which indeed does a proof seach.

Compare the Prolog membership predicate:

member(X,[X|Xs]).
member(X,[Y|Xs]) :- member(X,Xs)

with this rough Haskell type class implementation (using tuples instead of lists):

class Member x xs

instance Member x (x,xs)
instance Member x xs => Member x (y,xs)

Cheers!