User-Agent: Mozilla/5.0 (Windows NT 6.1; rv:7.0.1) Gecko/20110929
            Thunderbird/7.0.1
MIME-Version: 1.0
References: <4E95A9C2.6020607@residenset.net>
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
Message-ID:  <4E95C086.7060806@morningstar2.co.uk>
Date:         Wed, 12 Oct 2011 17:29:58 +0100
Reply-To: Mailing list for the LaTeX3 project
              <LATEX-L@listserv.uni-heidelberg.de>
Sender: Mailing list for the LaTeX3 project <LATEX-L@listserv.uni-heidelberg.de>
From: Joseph Wright <joseph.wright@MORNINGSTAR2.CO.UK>
Subject: Re: Church booleans
To: LATEX-L@listserv.uni-heidelberg.de
In-Reply-To:  <4E95A9C2.6020607@residenset.net>
Precedence: list
Status: R

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