Church booleans and numbers in Elixir

functions_all_the_way.exs

#####################
# Basic combinators #
#####################

id = fn(x) -> x end

kestrel = fn (x) -> fn (y) -> x end end

starling =
  fn (x) ->
    fn (y) ->
      fn (z) ->
        x.(z).(y.(z))
      end
    end
  end
  
y = fn (h) ->
  (fn (f) ->
    f.(f)
  end).(fn (g) ->
    h.(fn (x) -> g.(g).(x) end)
  end)
end


############
# Booleans #
############

bool_true  = fn (a) -> fn (b) -> a end end
bool_false = fn (a) -> fn (b) -> b end end

bool_not = fn (p) -> p.(bool_false).(bool_true) end
bool_and = fn (a) -> fn (b) -> a.(b).(bool_false) end end
bool_or = fn (a) -> fn (b) -> a.(bool_true).(b) end end

bool_cond = fn (a) -> fn (b) -> fn (c) -> a.(b).(c) end end end

church_to_bool =
  fn (church_bool) ->
    church_bool.(true).(false)
  end

#########
# Pairs #
#########

pair =
  fn (a) ->
    fn (b) ->
      fn (c) -> c.(a).(b) end
    end
  end
  
first =
  fn (p) ->
    g = fn (x) -> fn (y) -> x end end
    p.(g)
  end

second =
  fn (p) ->
    g = fn (x) -> fn (y) -> y end end
    p.(g)
  end


############
# Numerals #
############

zero  = fn (f) -> fn (x) -> x end end
one   = fn (f) -> fn (x) -> x |> f.() end end
two   = fn (f) -> fn (x) -> x |> f.() |> f.() end end
three = fn (f) -> fn (x) -> x |> f.() |> f.() |> f.() end end

church_to_int =
  fn (n) ->
    n.(&(&1 + 1)).(0)
  end


succ =
  fn (n) ->
    fn (f) ->
      fn(x) ->
        f.(n.(f).(x))
      end
    end
  end
four = succ.(three)
five = succ.(four)

plus =
  fn (m) ->
    fn (n) ->
      fn (f) ->
        fn(x) ->
          m.(f).(n.(f).(x))
        end
      end
    end
  end
six = plus.(four).(two)
seven = succ.(six)
twenty = plus.(plus.(four).(five)).(plus.(six).(five))

zero_case = pair.(zero).(zero)
main_step =
  fn (p) ->
    pair.(second.(p)).(succ.(second.(p)))
  end
pred =
  fn (n) ->
    first.(n.(main_step).(zero_case))
  end

minus =
  fn (n) ->
    fn(m) ->
      m.(pred).(n)
    end
  end
  
mult =
  fn (n) ->
    fn (m) ->
      m.(plus.(n)).(zero)
    end
  end
one_hundred = mult.(twenty).(five)

power =
  fn (n) ->
    fn (m) ->
      m.(n)
    end
  end


# Predicates

is_zero =
  fn (n) ->
    n.(fn (_) -> bool_false end).(bool_true)
  end
  
num_eq =
  fn (n) ->
    fn (m) ->
      # bool_and.(is_zero.(minus.(n).(m))).(is_zero.(minus.(m).(n)))
      bool_and.(is_zero.((n).(pred).(m))).(is_zero.((m).(pred).(n)))
    end
  end

num_gt =
  fn (n) ->
    fn (m) ->
      bool_and.(is_zero.((n).(pred).(m))).(bool_not.(is_zero.((m).(pred).(n))))
    end
  end

num_lt =
  fn (n) ->
    fn (m) ->
      bool_and.(is_zero.((m).(pred).(n))).(bool_not.(is_zero.((n).(pred).(m))))
    end
  end

num_gt_eq =
  fn (n) ->
    fn (m) ->
      is_zero.((n).(pred).(m))
    end
  end

num_lt_eq =
  fn (n) ->
    fn (m) ->
      is_zero.((m).(pred).(n))
    end
  end

# Divide

divide =
  fn (n) ->
    fn (m) ->
      y.(fn (divide1) ->
        fn (current) ->
          num_gt_eq.(current).(m).(
            fn (_) -> succ.(divide1.(minus.(current).(m))) end
          ).(
            fn (_) -> zero end
          ).(zero)
        end
      end).(n)
    end
  end

reminder =
  fn (n) ->
    fn (m) ->
      y.(fn (reminder1) ->
        fn (current) ->
          num_gt_eq.(current).(m).(
            fn (_) -> reminder1.(minus.(current).(m)) end
          ).(
            fn (_) -> current end
          ).(zero)
        end
      end).(n)
    end
  end

# Factorial

proto_factorial = fn g ->
  fn (n) ->
    is_zero.(n).(fn (_) -> one end).(
      fn (_) ->
        mult.(n).(g.(pred.(n)))
      end
    ).(zero)
  end
end

factorial = y.(proto_factorial)