Inductive and coinductive definitions of list

list.py

# Algebra f a = f a → a
# Fix f = ∀x. Algebra f x → x

# Coalgebra f a = a → f a
# Cofix f = ∃x. x × Coalgebra f x

# ListF a x = 1 + a × x
# List a = Fix (ListF a)
# Colist a = Cofix (ListF a)


# ... -> f (Fix f) -> Fix f
intro = lambda fmap: lambda ffixf: lambda alg: alg(fmap(lambda fixf: fixf(alg))(ffixf))

# ... -> Fix f -> f (Fix f)
elim = lambda fmap: lambda fixf: fixf(fmap(intro(fmap)))


# ... -> Cofix f -> f (Cofix f)
coelim = lambda fmap: lambda cofixf: fmap(lambda x: (x, cofixf[1]))(cofixf[1](cofixf[0]))

# ... -> f (Cofix f) -> Cofix f
cointro = lambda fmap: lambda fcofixf: (fcofixf, fmap(coelim(fmap)))


# ListF a x
listf_empty = lambda empty: lambda cons: empty

# a -> x -> ListF a x
listf_cons = lambda head: lambda tail: lambda empty: lambda cons: cons(head)(tail)

# (a -> b) -> ListF x a -> ListF x b
listf_map = lambda f: lambda listf: listf(listf_empty)(lambda head: lambda tail: listf_cons(head)(f(tail)))


# ListF a (List a) -> List a
list_intro = intro(listf_map)

# List a -> ListF a (List a)
list_elim = elim(listf_map)

# List a
list_empty = list_intro(listf_empty)

# a -> List a -> List a
list_cons = lambda head: lambda tail: list_intro(listf_cons(head)(tail))

# List a -> list[a]
list_to_python = lambda list: list_elim(list)([])(lambda head: lambda tail: [head, *list_to_python(tail)])


# Colist a -> ListF a (Colist a)
colist_elim = coelim(listf_map)

# ListF a (Colist a) -> Colist a
colist_intro = cointro(listf_map)

# Colist a
colist_empty = colist_intro(listf_empty)

# a -> Colist a -> Colist a
colist_cons = lambda head: lambda tail: colist_intro(listf_cons(head)(tail))

# Colist a -> list[a]
colist_to_python = lambda colist: colist_elim(colist)([])(lambda head: lambda tail: [head, *colist_to_python(tail)])


list = list_cons(1)(list_cons(2)(list_cons(3)(list_empty)))

colist = colist_cons(1)(colist_cons(2)(colist_cons(3)(colist_empty)))

print(list_to_python(list))

print(colist_to_python(colist))