Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
It was around the time I added car and cdr that I realised this wasn't about natural numbers anymore
from util import *
class Obj:
@constructor
def __init__(self, name):
pass
def __str__(self):
return str(self.name)
class Type(Obj):
@constructor
def __init__(self, name, base):
pass
def __str__(self):
return str(self.name)
class Fn:
@constructor
def __init__(self, dtype, rtype, name='', callback=None):
self.unique = id(self)
if callback is None:
self.callback = dtype.base
def __str__(self):
if self.name:
return '{}:{}->{}'.format(self.name, self.dtype, self.rtype)
else:
return '({}->{})'.format(self.dtype, self.rtype)
def __call__(self, arg):
return CalledFn(self, arg)
@accumulate(all)
def __eq__(self, other):
yield type(self) == type(other)
yield self.unique == other.unique
class CalledFn:
@constructor
def __init__(self, func, arg):
self.value = None #why is this needed
if isinstance(func.rtype, Obj):
self.name = '{}({})'.format(func.name, arg)
self.value = Obj(self.name)
elif isinstance(func.rtype, Fn):
self.name = '{}({})'.format(func.name, arg)
self.value = Fn(func.dtype, func.rtype, self.name, callback=self)
self.value.unique = func.unique
else:
raise NotImplementedError
def __call__(self, arg):
return self.value(arg)
def __str__(self):
return str(self.name)
@accumulate(all)
def __eq__(self, other):
if isinstance(other, CalledFn):
yield self.func == other.func
yield self.arg == other.arg
else:
yield self.value == other
def cdr(s):
return s.arg
def car(s):
return s.func.callback.arg
# The natural numbers (N)
#
# Constants:
# 0
# suc : N -> N
#
# Extras:
# add(N, N) -> N
# leq(N, N) -> bool
zero = Obj('0')
nattype = Type('N', zero)
suc = Fn(nattype, nattype, 'S')
add = lambda n, m: n if m == zero else add(suc(n), cdr(m))
def recurse(base, f, times=0):
for _ in range(times):
yield base
base = f(base)
one, two, three, four, five, six, seven, eight = recurse(suc(zero), suc, 8)
leq = lambda n, m: True if n == zero else \
False if m == zero else \
leq(cdr(n), cdr(m))
assert(zero == zero)
assert(suc == suc)
assert(suc(zero) == suc(zero) == one)
assert(zero != suc(zero))
assert(add(two, three) == add(four, one) == five)
assert(leq(three, five))
assert(leq(five, five))
assert(not leq(six, five))
print(nattype)
print(zero)
print(suc)
print(suc(zero))
print(suc(suc(zero)))
print(add(five, four))
print()
# Lists of natural numbers (List)
#
# Constants:
# empylist
# cons: N -> (List -> List)
#
# Extras:
# inlist(N, List) -> bool
# reverse(List) -> List
# minitem(List) -> N
# join(List, List) -> List
# remove(N, List) -> List
# sort(List) -> List
emptylist = Obj('[]')
listtype = Type('List', emptylist)
cons = Fn(nattype, Fn(listtype, listtype), 'cons')
inlist = lambda n, lst: \
False if lst == emptylist else \
True if n == car(lst) else \
inlist(n, cdr(lst))
reverse = lambda lst: \
emptylist if lst == emptylist else \
cons(car(lst))(cdr(lst))
minitem = lambda lst: \
None if lst == emptylist else \
car(lst) if cdr(lst) == emptylist else \
car(lst) if leq(car(lst), minitem(cdr(lst))) else \
minitem(cdr(lst))
join = lambda lsx, lsy: \
lsy if lsx == emptylist else \
join(cdr(reverse(lsx)), cons(car(reverse(lsx)))(lsy))
remove = lambda n, lst: \
cons(car(lst))(remove(n, cdr(lst))) if n != car(lst) else \
cdr(lst)
sort = lambda lst: \
emptylist if lst == emptylist else \
cons(minitem(lst))(sort(remove(minitem(lst), lst)))
assert(cons(one) == cons(one))
assert(cons(one)(emptylist) == cons(one)(emptylist))
assert(inlist(one, cons(one)(emptylist)))
firstfour = cons(one)(cons(two)(cons(three)(cons(four)(emptylist))))
revfour = cons(four)(cons(three)(cons(two)(cons(one)(emptylist))))
assert(car(firstfour) == one)
assert(inlist(one, firstfour))
assert(inlist(four, firstfour))
assert(not inlist(zero, firstfour))
assert(reverse(firstfour) == revfour)
assert(minitem(firstfour) == minitem(revfour) == one)
assert(join(cons(one)(cons(two)(emptylist)),
cons(three)(cons(four)(emptylist))) == firstfour)
assert(remove(three, firstfour) == cons(one)(cons(two)(cons(three)(emptylist))))
assert(sort(revfour) == firstfour)
print(listtype)
print(emptylist)
print(cons)
print(cons(emptylist))
print(cons(emptylist)(zero))
print(cons(cons(emptylist)(zero)))
print(cons(cons(emptylist)(zero))(suc(zero)))
@milesrout

This comment has been minimized.

Copy link

@milesrout milesrout commented Oct 4, 2016

def __eq__(self, other):
        return type(self) == type(other)

your an idiot

@louisswarren

This comment has been minimized.

Copy link
Owner Author

@louisswarren louisswarren commented Oct 5, 2016

I always liked functional LISP.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment