Inductive free IO monad

io.py

# Map f = (a -> b) -> f a -> f b

# Id f = a -> f a

# Join f = f (f a) -> f a

# Bind f = f a -> (a -> f b) -> f b

# Then f = f a -> f b -> f b


# Map f -> Join f -> Bind f
bind = lambda map: lambda join: lambda v: lambda f: join(map(f)(v))

# Bind f -> Then f
then = lambda bind: lambda first: lambda second: bind(first)(lambda _: second)


# IO a = Pure a | Inp (str -> IO a) | Out str (IO a)
# IO a = (a -> r) -> ((str -> r) -> r) -> (str -> r -> r) -> r

# a -> IO a
io_pure = lambda v: lambda pure: lambda inp: lambda out: pure(v)

# (str -> IO a) -> IO a
io_inp = lambda cons: lambda pure: lambda inp: lambda out: inp(lambda str: cons(str)(pure)(inp)(out))

# str -> IO a -> IO a
io_out = lambda str: lambda cont: lambda pure: lambda inp: lambda out: cont(out(str)(pure))(inp)(out)

# IO a -> a
io_run = lambda io: io(lambda v: v)(lambda cons: cons(input()))(lambda str: lambda cont: (print(str), cont)[1])

# Map IO
io_map = lambda f: lambda io: lambda pure: lambda inp: lambda out: io(lambda v: pure(f(v)))(inp)(out)

# Id IO
io_id = io_pure

# Join IO
io_join = lambda io_io: lambda pure: lambda inp: lambda out: io_io(lambda io: io(pure)(inp)(out))(inp)(out)

# Bind IO
io_bind = bind(io_map)(io_join)

# Then IO
io_then = then(io_bind)

# IO str
io_input = io_inp(io_pure)

# str -> IO None
io_print = lambda str: io_out(str)(io_pure(None))


# IO None
main = \
    io_then(io_print("What's your name?"))(
    io_bind(io_input)(lambda name:
    io_print(f"Hi, {name}!")
))

io_run(main)