Lambda Calculus - Functional condition

Lambda Calculus

If you have never heard about lambda calculus, here is a quick definition found on Wikipedia:

Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution.

Basically, this is the syntax:

An expression is also a variable.

For example, here is the identity function from mathematics:

Lambda Calculus
        
identity = λx.x
        
      

A more concrete example is its usage to represent types. In the following example:

JavaScript
        
function upper(str) {
  return str.toUpperCase()
}
        
      

has the type:

Lambda Calculus
        
t' = λ t . t

// We can reduce it to infer the return type
t' = λ string . string
t' = string

// The result type is `string`
        
      

Let's define booleans

Lambda Calculus
        
true = λx.λy.x
false = λx.λy.y
        
      

Define the conditional operator

Lambda Calculus
        
if = λb.λt.λf.b t f
        
      

Define the logical operators

Lambda Calculus
        
and = λbb'. if b b' false
or = λbb'. if b true b'
not = λb.if b false true
        
      

Example

I decided to use OCaml for this example because it has partial application and a nice REPL.
Since the conditional and logical operators are already in the language, I will prepend them with an underscore.

Translate definitions into OCaml

OCaml
        
let _true x y = x;;
(* - : 'a -> 'b -> 'a =  *)

let _false x y = y;;
(* - : 'a -> 'b -> 'b =  *)
        
      

Note that it's similar to how an identity function works.

OCaml
        
let _if b t f = b t f;;
(* - : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c =  *)
        
      

For the sake of simplicity, I won't declare all the operators for now. We can already evaluate some simple conditions.

OCaml
        
(* This is my condition, for now it's a constant `true` *)
let myCond = _true;;

_if myCond 1 0;;
(* - : int = 1 *)

(* and if my condition is `false` *)
let myCond2 = _false;;

_if myCond2 1 0;;
(* - : int = 0 *)
        
      

Conclusion

To be honest, I don't know why you would use this in real life code. There is no need to redefine the built-in condition mechanism.

Thanks to Danny Willems for introducing me to this.

Contact me

Say hello: sven.sauleau@xtuc.fr.

Ping me on Twitter: @svensauleau.

© XTUC SAS
N° SIRET : 821 797 891 00016, RCS Strasbourg TI 821 797 891