Instantly share code, notes, and snippets.

Embed
What would you like to do?
Church booleans and numbers in Elixir
#####################
# 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment