Skip to content

Instantly share code, notes, and snippets.

@mattmight

mattmight/pythedral.py

Created December 2, 2014 22:48
Show Gist options
  • Save mattmight/453590fd5681495f1f92 to your computer and use it in GitHub Desktop.
Save mattmight/453590fd5681495f1f92 to your computer and use it in GitHub Desktop.
Download ZIP
Church Python
Raw
pythedral.py
# Void
VOID = lambda void: void
# Booleans / Conditionals
IF = lambda c: lambda t: lambda f: c(t)(f)
TRUE = lambda t: lambda f: t
FALSE = lambda t: lambda f: f
print (IF (TRUE) ("true") ("false"))
print (IF (FALSE) ("true") ("false"))
TRUE = lambda t: lambda f: t()
FALSE = lambda t: lambda f: f()
print (IF (TRUE) (lambda: "true") (lambda: "false"))
print (IF (FALSE) (lambda: "true") (lambda: "false"))
# Numerals
ZERO = lambda f: lambda z: z
SUCC = lambda n: lambda f: lambda z: (f(n(f)(z)))
SUM = (lambda a: lambda b: lambda f: lambda z:
a(f)(b(f)(z)))
MUL = (lambda a: lambda b: lambda f: lambda z:
a(lambda z:b(f)(z))(z))
natify = lambda n: n (lambda x: x + 1) (0)
print (natify(ZERO))
print (natify(SUCC(ZERO)))
print (natify(SUCC(SUCC(ZERO))))
ONE = SUCC(ZERO)
TWO = SUCC(ONE)
FOUR = SUM(TWO)(TWO)
SIXTEEN = MUL(FOUR)(FOUR)
print (natify(FOUR))
print (natify(SIXTEEN))
# Pairs
PAIR = lambda l: lambda r: lambda f: f(l)(r)
LEFT = lambda p: p(lambda l: lambda r: l)
RIGHT = lambda p: p(lambda l: lambda r: r)
print (LEFT (PAIR ("left") ("right")))
print (RIGHT (PAIR ("left") ("right")))
# Lists
NIL = lambda oncons: lambda onnil: onnil(VOID)
CONS = (lambda hd: lambda tl:
lambda oncons: lambda onnil:
oncons(hd)(tl))
CONSP = lambda l: l (lambda hd: lambda tl: TRUE) (lambda void: FALSE)
NILP = lambda l: l (lambda hd: lambda tl: FALSE) (lambda void: TRUE)
HEAD = lambda l: l (lambda hd: lambda tl: hd) (VOID)
TAIL = lambda l: l (lambda hd: lambda tl: tl) (VOID)
print (IF (CONSP(NIL)) (lambda: "cons") (lambda: "nil"))
print (IF (CONSP(CONS(10)(20))) (lambda: "cons") (lambda: "nil"))
print (HEAD (CONS ("head") ("tail")))
print (TAIL (CONS ("head") ("tail")))
# Non-termination
U = lambda f: f(f)
# Omega = U(U) # Stack over-flow from infinite loop
# Factorial
fact = U(lambda h: lambda n: 1 if n <= 0 else n * (U(h))(n-1))
print (fact(5))
# Y combinator
# Y(F) = x such that x = F(x)
# Y(F) = x such that x = F(Y(F))
# Y(F) = F(Y(F))
# Y = lambda F: F(Y(F)) # works for call-by-name
Y = lambda F: F(lambda x: Y(F)(x))
fact = Y(lambda f: lambda n: 1 if n <= 0 else n * f(n-1))
print (fact(6))
Y = U(lambda h: lambda F: F(lambda x: U(h)(F)(x)))
fact = Y(lambda f: lambda n: 1 if n <= 0 else n * f(n-1))
print (fact(7))
Y = (lambda h: lambda F: F(lambda x: h(h)(F)(x)))(lambda h: lambda F: F(lambda x: h(h)(F)(x)))
fact = Y(lambda f: lambda n: 1 if n <= 0 else n * f(n-1))
print (fact(8))
R1 = (((lambda f: (((f)((lambda f: ((lambda z: (((f)(((f)(((f)(((f)(((f)(z)))))))))))))))))))((((((lambda y: ((lambda F: (((F)((lambda x: (((((((y)(y)))(F)))(x)))))))))))((lambda y: ((lambda F: (((F)((lambda x: (((((((y)(y)))(F)))(x)))))))))))))((lambda f: ((lambda n: ((((((((((((lambda n: (((((n)((lambda _: ((lambda t: ((lambda f: (((f)((lambda void: (void)))))))))))))((lambda t: ((lambda f: (((t)((lambda void: (void)))))))))))))((((((lambda n: ((lambda m: (((((m)((lambda n: ((lambda f: ((lambda z: (((((((n)((lambda g: ((lambda h: (((h)(((g)(f)))))))))))((lambda u: (z)))))((lambda u: (u)))))))))))))(n)))))))(n)))((lambda f: ((lambda z: (z)))))))))((lambda _: ((((lambda n: (((((n)((lambda _: ((lambda t: ((lambda f: (((f)((lambda void: (void)))))))))))))((lambda t: ((lambda f: (((t)((lambda void: (void)))))))))))))((((((lambda n: ((lambda m: (((((m)((lambda n: ((lambda f: ((lambda z: (((((((n)((lambda g: ((lambda h: (((h)(((g)(f)))))))))))((lambda u: (z)))))((lambda u: (u)))))))))))))(n)))))))((lambda f: ((lambda z: (z)))))))(n)))))))))((lambda _: ((lambda t: ((lambda f: (((f)((lambda void: (void)))))))))))))((lambda _: ((lambda f: ((lambda z: (((f)(z)))))))))))((lambda _: ((((((lambda n: ((lambda m: ((lambda f: ((lambda z: (((((m)(((n)(f)))))(z)))))))))))(n)))(((f)((((((lambda n: ((lambda m: (((((m)((lambda n: ((lambda f: ((lambda z: (((((((n)((lambda g: ((lambda h: (((h)(((g)(f)))))))))))((lambda u: (z)))))((lambda u: (u)))))))))))))(n)))))))(n)))((lambda f: ((lambda z: (((f)(z))))))))))))))))))))))))
print (natify(R1))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment