λ -calculus : What is the most efficient in memory representation of functions?

Question

I would like to compare performance of function encoded (Church's / Scott's) vs classically encoded (assembler / C) data structures.

But before I do that I need to know how efficient is / can be function representation in memory. The function can be of course partially applied (aka closure).

I am interested in both the current encoding algorithm popular functional languages (Haskell, ML) use and also in the most efficient one that can be achieved.

---

Bonus point : Is there such encoding that maps function encoded integers to native integers (short, int etc in C). Is it even possible?

---

I value efficiency based on performance. In other words the more efficient the encoding is the less it influences performance of computation with functional data structures.

Answer 1

The thing is, there's really not much leeway in terms of function encoding. Here are the main options:

• Term rewriting: you store functions as their abstract syntax trees (or some encoding thereof. When you call a function, you manually traverse the syntax tree to replace its parameters with the argument. This is easy, but terribly inefficient in terms of time and space.

• Closures: you have some way of representing a function, maybe a syntax tree, more likely machine code. And in these functions, you refer to your arguments by reference in some way. It could be a pointer-offset, it could be an integer or De Bruijn index, it could be a name. Then you represent a function as a closure: the function "instructions" (tree, code, etc.) paired with a data structure containing all free variables of the function. When a function is actually applied, it somehow knows how to look up the free variables in its data structure, using environments, pointer arithmetic, etc.

I'm sure there are other options, but these are the basic ones, and I suspect almost every other option will be a variant of or optimization of the basic closure structure.

So, in terms of performance, closures almost universally perform better than term rewriting. Of the variations, which is better? That depends heavily on your language and architecture, but I suspect the "machine-code with a struct containing free vars" is the most efficient. It has everything the function needs (instructions and values) and nothing more, and calling doesn't end up doing large term traversals.

I am interested in both the current encoding algorithm popular functional languages (Haskell, ML) use

I'm not an expert, but I'm 99% most ML flavours use some variation of the closures I describe, albeit with some optimizations likely. See this for a (possibly out of date) perspective.

Haskell does something a bit more complicated because of lazy evaluation: it uses Spineless Tagless Graph Rewriting.

and also in the most efficient one that can be achieved.

What is most efficient? There is no implementation that will be most efficient across all inputs, so you get implementations that are efficient on average, but each will excel in different scenarios. So there's no definite ranking of most or least efficient.

There's no magic here. To store a function, you need to store its free values somehow, otherwise you're encoding less information than the function itself has. Maybe you can optimize away some of the free values with partial evaluation but that's risky for performance, and you have to be careful to ensure that this always halts.

And, maybe you can use some sort of compression, or clever algorithm to gain space efficiency. But then you're either trading time for space, or you're in the situation where you've optimized for some cases and slowed down for others.

You can optimize for the common case, but what the common case is can change on the language, area of application, etc. The type of code that's fast for a video game (number crunching, tight loops with large input) is probably different than what's fast for a compiler (tree traversals, worklists, etc.).

Bonus point : Is there such encoding that maps function encoded integers to native integers (short, int etc in C). Is it even possible?

No, this is not possible. The problem is that the lambda calculus does not let you introspect terms. When a function takes an argument with the same type as a Church-numeral, it needs to be able to call it, without examining the exact definition of that numeral. That's the thing with Church encodings: the only thing you can do with them is call them, and you can simulate everything useful with this, but not without a cost.

More importantly, the integers occupy every possible binary encoding. So if lambdas were represented as their integers, you'd have no way of representing non-church-numberal lambdas! Or, you'd introduce a flag to denote whether a lambda is a numeral or not, but then any efficiency you want is probably gone out the window.

EDIT: Since writing this, I've become aware of a third option for implementing higher-order functions: defunctionalization. Here, every function call turns into a big switch statement, depending on which lambda abstraction was given as the function. The tradeoff here is that it's a whole program transformation: you can't compile parts separately and then link together this way, since you need to have the complete set of lambda abstractions ahead of time.

Answer 2

Bonus point

You can map lambda functions to digits (as opposed to integers), which will speed up arithmetic immensely. Here is an example that implements base-16 arithmetic (it functions kind of like an odometer). Numbers are cons-lists of digits, least significant first. You can use a (much more verbose) base-256 version to map to byte values. I'm only providing support for adding. The other operations are left as an exercise for the reader.

It's handy if your LC interpreter / compiler maintains function identity like mine does (mine uses closures by default, which helps with this). The UI prints function names for known functions when "pretty" is checked.

You can compile and run this in my evaluator (I'll fix the SSL certificate soon) http://lambdamechanics.com/lcPresentation/evaluator.html by saving the source to a file, clicking "Choose File", and then clicking "Run" on example ex3, ex4, and/or ex5. Sorry for the rough UI, I haven't worked on this for quite a while.

Source:

# add hex numbers represented as lists of hex digits, least significant first

# booleans
t   = λa b . a
f   = λa b . b
and = λa b . a b f
or  = λa b . a t b

# Y combinator
Y = λg . (λx . g (x x)) λx . g (x x)
# use recursion
rec = λf . f (Y f)

#lists -- the evaluator pretty prints lists if these defs are present
cons    = λa b . λfun . fun a b
head    = λl . l λa b . a
tail    = λl . l λa b . b
nil     = λa b . b
null    = λl . l (λa b D . f) t
append  = rec λappend l1 l2 . l1 (λh t D . cons h (append t l2)) l2
reverse = λl . rec (λrev l res . l (λh t D . rev t (cons h res)) res) l nil

# hex digits. A number is a list of digits in least-significant-first order
0 = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . d0
1 = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . d1
2 = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . d2
3 = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . d3
4 = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . d4
5 = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . d5
6 = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . d6
7 = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . d7
8 = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . d8
9 = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . d9
A = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . dA
B = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . dB
C = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . dC
D = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . dD
E = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . dE
F = λd0 d1 d2 d3 d4 d5 d6 d7 d8 d9 dA dB dC dD dE dF . dF

is0 = λz . z t f f f f f f f f f f f f f f f
isF = λz . z f f f f f f f f f f f f f f f t

inc = λn . cons (n 1 2 3 4 5 6 7 8 9 A B C D E F 0) (is0 n)
dec = λn . cons (n F 0 1 2 3 4 5 6 7 8 9 A B C D E) (isF n)

# an addition table that returns the result plus overflow
#baseadd = λx y . x
#  (y (cons 0 f) (cons 1 f) (cons 2 f) (cons 3 f) (cons 4 f) (cons 5 f) (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f))
#  (y (cons 1 f) (cons 2 f) (cons 3 f) (cons 4 f) (cons 5 f) (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t))
#  (y (cons 2 f) (cons 3 f) (cons 4 f) (cons 5 f) (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t))
#  (y (cons 3 f) (cons 4 f) (cons 5 f) (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t))
#  (y (cons 4 f) (cons 5 f) (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t))
#  (y (cons 5 f) (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t))
#  (y (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t))
#  (y (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t))
#  (y (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t))
#  (y (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t))
#  (y (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t) (cons 9 t))
#  (y (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t) (cons 9 t) (cons A t))
#  (y (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t) (cons 9 t) (cons A t) (cons B t))
#  (y (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t) (cons 9 t) (cons A t) (cons B t) (cons C t))
#  (y (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t) (cons 9 t) (cons A t) (cons B t) (cons C t) (cons D t))
#  (y (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t) (cons 9 t) (cons A t) (cons B t) (cons C t) (cons D t) (cons E t))
#
# condensed form below:

baseadd = λx y . x (y (cons 0 f) (cons 1 f) (cons 2 f) (cons 3 f) (cons 4 f) (cons 5 f) (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f)) (y (cons 1 f) (cons 2 f) (cons 3 f) (cons 4 f) (cons 5 f) (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t)) (y (cons 2 f) (cons 3 f) (cons 4 f) (cons 5 f) (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t)) (y (cons 3 f) (cons 4 f) (cons 5 f) (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t)) (y (cons 4 f) (cons 5 f) (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t)) (y (cons 5 f) (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t)) (y (cons 6 f) (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t)) (y (cons 7 f) (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t)) (y (cons 8 f) (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t)) (y (cons 9 f) (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t)) (y (cons A f) (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t) (cons 9 t)) (y (cons B f) (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t) (cons 9 t) (cons A t)) (y (cons C f) (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t) (cons 9 t) (cons A t) (cons B t)) (y (cons D f) (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t) (cons 9 t) (cons A t) (cons B t) (cons C t)) (y (cons E f) (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t) (cons 9 t) (cons A t) (cons B t) (cons C t) (cons D t)) (y (cons F f) (cons 0 t) (cons 1 t) (cons 2 t) (cons 3 t) (cons 4 t) (cons 6 t) (cons 7 t) (cons 7 t) (cons 8 t) (cons 9 t) (cons A t) (cons B t) (cons C t) (cons D t) (cons E t))

fmt = λn . cons (head n) (cons (tail n) nil)
ex1 = fmt (baseadd 8 9)
ex2 = fmt (baseadd 3 4)

# add two numbers
#addc = rec λaddc a b ovf .
#  (null b)
#    ((null a)
#      # both are nil
#      nil
#      # only b is nil, reverse and recall
#      (addc b a ovf))
#    ((null a)
#      # only a is nil, account for overflow
#      (ovf
#        # overflow adds 1
#        ((baseadd (head b) 1)
#          # destructure result of baseadd
#          λdigit ovf2 .
#            ovf2
#              # secondary overflow adds 10, return [digit , 1]
#              (cons digit (cons 1 nil))
#              # no secondary overflow, return [digit]
#              (cons digit nil))
#        # no overflow, return b
#        b)
#      # neither a nor b is nil, optionally increment (head a) and add result to (head b)
#      ((ovf
#        # overflow, inc (head a)
#        (baseadd (head a) 1)
#        # no overflow, use (head a), f
#        (cons (head a) f))
#        # destructure result of optional inc
#        λnewA ovf1 .
#          (baseadd newA (head b))
#            # destructure result
#            λresult ovf2 .
#              (cons result (addc (tail a) (tail b) (or ovf1 ovf2)))))
#
# condensed form below:

addc = rec λaddc a b ovf . (null b) ((null a) nil (addc b a ovf)) ((null a) (ovf ((baseadd (head b) 1) λdigit ovf2 . ovf2 (cons digit (cons 1 nil)) (cons digit nil)) b) ((ovf (baseadd (head a) 1) (cons (head a) f)) λnewA ovf1 . (baseadd newA (head b)) λresult ovf2 . (cons result (addc (tail a) (tail b) (or ovf1 ovf2)))))

add = λa b . addc a b f

# friendlier reversed add for more human-redable input/output
# this lets you use (cons 1 (cons 0)) to represent 10.
radd = λa b . reverse (add (reverse a) (reverse b))

# 1 + 2
ex3   = radd (cons 1 nil) (cons 2 nil)

# 13 + 2
ex4   = radd (cons 1 (cons 3 nil)) (cons 2 nil)

# 1F + 2
ex5   = radd (cons 1 (cons F nil)) (cons 2 nil)