Purer IO (probably works too)

README.md

This script simulates IO (print and input) in a pure functional manner using a coinductive data structure.

---

Python-compatible generator:

Generator yield send return = ∃state . state × (state → return + yield × (send → state))

With the point functor:

F yield send return state = return + yield × (send → state)

---

Generator needed for IO:

Generator yield send return = ∃state . state × (state → return + yield × state + (send → state))

With the point functor:

F yield send return state = return + yield × state + (send → state)

---

IO definition:

IO = Generator str str

io.py

# IO a = ∃s . s × (s → a + str × s + (str → s))


def io_run(io):
    state, interface = io

    result = None
    done = False

    def ret(value):
        nonlocal result, done
        result = value
        done = True

    def yld(p):
        nonlocal state
        str, state = p
        print(str)

    def snd(f):
        nonlocal state
        state = f(input())

    while True:
        interface(state)(ret)(yld)(snd)
        if done:
            return result


bind = lambda map: lambda join: lambda value: lambda function: join(map(function)(value))


then = lambda bind: lambda first: lambda second: bind(first)(lambda _: second)


io_get = (None, lambda state: lambda ret: lambda yld: lambda snd: snd(lambda s: s) if state is None else ret(state))


io_put = lambda str: (False, lambda state: lambda ret: lambda yld: lambda snd: ret(None) if state else yld((str, True)))


io_map = lambda function: lambda io: (io[0], lambda state: lambda ret: lambda yld: lambda snd: io[1](state)(lambda value: ret(function(value)))(yld)(snd))


io_id = lambda value: (value, lambda state: lambda ret: lambda yld: lambda snd: ret(state))


io_join = lambda io_io: ((io_io[0], None, None), lambda state: lambda ret: lambda yld: lambda snd: io_io[1](state[0])(lambda io: io[1](io[0])(ret)(lambda p: yld((p[0], (state[0], p[1], io[1]))))(lambda f: snd(lambda str: (state[0], f(str), io[1]))))(lambda p: yld((p[0], (p[1], None, None))))(lambda f: snd(lambda str: (f(str), None, None))) if state[2] is None else state[2](state[1])(ret)(lambda p: yld((p[0], (state[0], p[1], state[2]))))(lambda f: snd(lambda str: (state[0], f(str), state[2]))))


io_bind = bind(io_map)(io_join)


io_then = then(io_bind)


main = \
    io_then(io_put("What's your name?"))(
    io_bind(io_get)(lambda name:
    io_put(f"Hi, {name}!")
))


io_run(main)