PureFun

PureFun is designed by PSTF, where everything are functions.

It is based on Lambda calculus.

Core Principles

All values are functions: Booleans, numbers, pairs, and even control structures are defined as functions.

Evaluation Strategy: Use lazy evaluation (call-by-name or call-by-need) to avoid infinite recursion and enable conditional logic.

Syntax: Use a minimal Lisp-like syntax for clarity.

Key Constructs via Lambda Calculus

Logical Values and Conditional Branch

(define true (λ (x) (λ (y) x)))
(define false (λ (x) (λ (y) y)))
(define if (λ (cond) (λ (then) (λ (else) ((cond then) else)))))

In this case, the "if" evaluates into "then" if cond returns (λ (x) (λ (y) x) and "else" otherwise.

Pair

We uses the true and false defined in last section.

(define pair (λ (a) (λ (b) (λ (f) ((f a) b)))))
(define first (λ (p) (p true)))
(define second (λ (p) (p false)))

Church Numerals

(define zero (λ (f) (λ (x) x)))
(define one (λ (f) (λ (x) (f x))))
(define succ (λ (n) (λ (f) (λ (x) (f ((n f) x))))))
(define iszero (λ (n) ((n (λ (x) false)) true)))

Similarly, we can define that:

(define two (λ (f) (λ (x) (f (f x)))))
(define three (λ (f) (λ (x) (f (f (f x))))))
(define four (λ (f) (λ (x) (f (f (f (f x)))))))
...

And we can also define "add" and "multiply". In the Isomorphism Programming Language by same author, we stated that:

• a + 0 = a
• a + b' = (a + b)'
• a × 0 = 0
• a × b' = (a × b) + a

But where is subtraction and division? We also stated that:

• a + (-a) = 0
• a - b = a + (-b)
• a ÷ (1/a) = 0
• a ÷ b = a × (1/b)

But we can still define them by function composition.

Recursion (Y combinator)

(define Y (λ (f) ((λ (x) (f (x x))) (λ (x) (f (x x))))))

This allows the recursive functions like x₀ = (x!):

(define factorial (Y (λ (f) (λ (n)
  (((if (iszero n)) (λ () one)) (λ () ((mult n) (f (pred n))))))))

Where (pred n) is the last number of n.

Lazy Evaluation

Thunks: Delay evaluation by wrapping expressions in nullary functions (e.g., (λ () expr)).

Force Evaluation: Apply thunks to a dummy argument (e.g., unit defined as (λ (x) x)) when needed.

Example

x₀ = x!

(define pred ...) ; Predecessor function for Church numerals
(define mult ...) ; Multiplication function

(define factorial (Y (λ (f) (λ (n)
  (((if (iszero n))
    (λ () one))
    (λ () ((mult n) (f (pred n))))))))

Implementation Notes

• Interpreter: Would reduce expressions to normal form using lazy evaluation.
• Output: Convert Church numerals to integers via applied functions (e.g., (n (λ (x) (+ x 1)) 0) in a host language).
• Syntax: Use parentheses to denote function application: (f x).

Challenges

• Verbosity: Requires careful thunking to avoid eager evaluation.
• Performance: Church numerals are inefficient for large numbers.
• Readability: Advanced concepts like the Y combinator may hinder accessibility.

Idea for Extensions

• Lists: Represent as pairs (head and tail), with nil as a function.
• I/O: Use monads or imperative layers for side effects without breaking purity.

Conclusion

This language, rooted in lambda calculus, demonstrates how functions alone can express data and control flow. While impractical for real-world use, it highlights the theoretical power of functional programming. For a practical implementation, an interpreter would need to handle lazy evaluation and Church numeral conversion.