List/ChurchFold.bruijn


# MIT License, Copyright (c) 2025 Marvin Borner
# from Wikipedia, right-folded Church encoding

:import std/Logic .
:import std/Number/Ternary .

# empty list element
empty [[0]]

# returns true if a list is empty
empty? [0 [[false]] true]

# creates list with single element
singleton [[[1 2 0]]]

{}‣ singleton

:test (empty? ({}(+2))) (false)

# prepends an element to a list
cons [[[[1 3 (2 1 0)]]]]

…:… cons

# returns the head of a list or empty
head [0 [[1]] false]

^‣ head

:test (^((+1) : {}(+2))) ((+1))

# returns the tail of a list or empty
tail [[[2 [[[0 2 (1 4)]]] [1] [[0]]]]]

~‣ tail

:test (~((+1) : {}(+2))) ({}(+2))

# returns the length of a list in balanced ternary
length [0 [add (+1)] (+0)]

∀‣ length

:test (∀((+1) : {}(+2))) ((+2))
:test (∀empty) ((+0))

# appends two lists
append [[[[3 1 (2 1 0)]]]]

…++… append

:test ({}(+1) ++ empty) ({}(+1))
:test (empty ++ {}(+1)) ({}(+1))
:test (empty ++ empty) (empty)
:test (((+1) : ((+2) : {}(+3))) ++ {}(+4)) ((+1) : ((+2) : ((+3) : {}(+4))))

# maps each element to a function
map [[[[2 [[3 (5 1) 0]] 0]]]]

…<$>… map

:test (++‣ <$> ((+1) : ((+2) : {}(+3)))) ((+2) : ((+3) : {}(+4)))

# applies a right fold on a list
foldr [[[0 2 1]]]

:test ((foldr …+… (+0) ((+1) : ((+2) : {}(+3)))) =? (+6)) (true)
:test ((foldr …-… (+2) ((+1) : ((+2) : {}(+3)))) =? (+0)) (true)