Print

Print


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?

Lars Hellström