[Haskell-cafe] Origins of '$'

[Hans Aberg]

On 7 Dec 2008, at 11:34, Luke Palmer wrote:

> On Sun, Dec 7, 2008 at 3:05 AM, Hans Aberg <haberg at math.su.se> wrote:
> One can define operators
>  a ^ b := b(a)          -- Application in inverse.
>  (a * b)(x) := b(a(x))  -- Function composition in inverse.
>  (a + b)(x) := a(x) * b(x)
>  O(x) := I              -- Constant function returning identity.
>  I(x) := x              -- Identity.
> and use them to define lambda calculus (suffices with the first  
> four; Church reverses the order of "*").
>
> The simple elegance of writing this encoding just increased my  
> already infinite love of Haskell by another cardinality.
>
> a .^ b = b a
> (a .* b) x = b (a x)
> (a .+ b) x = a x .* b x
> o x = i
> i x = x
>
> toNat x = x (+1) 0
> fromNat n = foldr (.) id . replicate n

I have some more notes on this that you might translate, if possible  
(see below).

If one implements integers this way, time complexity of the operators  
will be of high order, but it is in fact due to representing n in  
effect as 1+...+1. If one represents them, using these operators, in  
a positional notation system, that should be fixed, though there is a  
lot of other overhead.

   Hans


Associativity: a*(b*c) = (a*b)*c, a+(b+c) = (a+b)+c

RHS Relations:
   a^O = I, a^I = a
   a^(b * c) = (a^b)^c
   a^(b + c) = a^b * a^c
   a*(b + c) = a*b + a*c

LHS Relations:
   I * a = a, O + a = a, O * a = I ^ a
   c functor (i.e., c(a*b) = c(a)*c(b), c(I) = I) =>
     (a*b)^c = a^c * b^c
     (a+b)*c = a*c + b*c
     I^c = I

If n in Natural, f: A -> A an endo-function, define
   f^n := I,              if n = 0
          f * ... * f,    if n > 1
          |-n times-|
The natural number functionals, corresponding to Church's number
functionals, are then defined by
   \bar n(f) := f^k
If S(x) := x + 1 (regular integer addition), then
   \bar n(S)(0) = n

Also write (following Hancock)
   log_x b := \lambda x b
Then
   log_x I = O
   log_x x = I
   log_x(a * b) = log_x a + log_x b
   log_x(a ^ b) = (log_x a) * b,    x not free in b.