## LATEX-L@LISTSERV.UNI-HEIDELBERG.DE

#### View:

 Message: [ First | Previous | Next | Last ] By Topic: [ First | Previous | Next | Last ] By Author: [ First | Previous | Next | Last ] Font: Proportional Font

Subject:

Re: Church booleans

From:

Date:

Wed, 12 Oct 2011 17:29:58 +0100

Content-Type:

text/plain

Parts/Attachments:

 text/plain (71 lines)
 On 12/10/2011 15:52, Lars Hellström wrote: > Last week, I was reading up a bit on lambda calculus (a subject with > which I suspect there are list members far more familiar than I am). One > thing that caught my eye was the definitions of True and False, using > the so-called Church booleans > > True = \lambda xy . x > False = \lambda xy . y > > These may look strange, but turn out to be two objects that are very > familiar to us: \use_i:nn and \use_ii:nn respectively (or \@firstoftwo > and \@secondoftwo, for those who still think in 2e terms (like me)). > Indeed, putting my mind in LaTeX mode made the lambda calculus concepts > much easier to digest. > > But with such thinking comes also the converse association: might LaTeX > programming benefit from borrowing concepts from lambda calculus? In > particular: might the Church booleans be useful as general-purpose > booleans in LaTeX3?!? > > (A rather early thought then was that Frank's generation probably knows > all about lambda calculus and therefore must have thought about this > already. But I don't recall having seen it discussed anywhere.) > > One thing that is really nice about the Church booleans is how they > support the logical operations. One can define > > \cs_new:Npn \and:nnTF #1 #2 { #1 {#2} {\use_ii:nn} } > \cs_new:Npn \or:nnTF #1 #2 { #1 {\use_i:nn} {#2} } > \cs_new:Npn \not:nTF #1 { #1 {\use_ii:nn} {\use_i:nn} } > > and go > > \cs_set_eq:NN \foo_a_bool \use_i:nn > \cs_set_eq:NN \foo_b_bool \use_ii:nn > \or:nnTF { > \and:nnTF { \foo_a_bool } { \foo_b_bool } > } { > \not:nTF { \foo_b_bool } > } {True} {False} > > to get the correct result True. These \and:, \or:, and \not: can even > operate on general \...:TF constructions, and they work correctly > regardless of whether the \...:TF is expandable or needs to be executed! > (Like e.g. \regex_match:nnTF.) This is already much nicer than what one > can easily get from the primitive \if... \fi conditionals. Using this > for LaTeX3 booleans would also have the interesting property that > "predicates" and TF forms become the exact same thing! > > I can imagine that a downside of using this would be that it suggests a > coding style that could be considered "too exotic". It sometimes seems > that l3 tries to make things look very much like they would in a > traditional imperative programming language, even though what goes on > under the hood can be quite different. A concept like Church booleans > rather furthers functional idioms of programming, where a lot of the > "data" you pass around is also "functions" (or partially applied > functions), that can be applied with little or no syntactic framing in > the source code. > > Now I wonder: Would it be useful? (I think it would.) Would there still > be time to change? Does it seem worth it? One obvious question is how easy would it be to support predicate decision making in such as scheme:   \bool_if:nTF     { \l_my_first_bool && ( \l_my_second_bool && !\l_my_third_bool ) } which is one of the reasons for the approach currently taken. -- Joseph Wright