IO (inductive Free)

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

# TakeAfter 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 -> TakeAfter f
take_after = lambda bind: lambda first: lambda second: bind(first)(lambda _: second)


# Free f a = a + f (Free f a) = (a -> r) -> (f r -> r) -> r

# a -> Free f a
free_pure = lambda v: lambda pure: lambda bind: pure(v)

# Map f -> f (Free f a) -> Free f a
free_dirty = lambda f_map: lambda f_free: lambda pure: lambda dirty: dirty(f_map(lambda free: free(pure)(dirty))(f_free))

# Map (Free f)
free_map = lambda f: lambda free: lambda pure: lambda dirty: free(lambda v: pure(f(v)))(dirty)

# Id (Free f)
free_id = free_pure

# Map f -> Join (Free f)
free_join = lambda f_map: lambda free_free: free_free(lambda free: free)(free_dirty(f_map))


# IOF x = (str -> x) + str * x = ((str -> x) -> r) -> (str -> x -> r) -> r

# (str -> x) -> IOF x
iof_inp = lambda cons: lambda inp: lambda out: inp(cons)

# str -> x -> IOF x
iof_out = lambda str: lambda cont: lambda inp: lambda out: out(str)(cont)

# Map IOF
iof_map = lambda f: lambda iof: lambda inp: lambda out: iof(lambda cons: inp(lambda str: f(cons(str))))(lambda str: lambda cont: out(str)(f(cont)))


# IO = Free IOF

# a -> IO a
io_pure = free_pure

# IOF (IO a) -> IO a
io_dirty = free_dirty(iof_map)

# (str -> IO a) -> IO a
io_inp = lambda cons: io_dirty(iof_inp(cons))

# str -> IO a -> IO a
io_out = lambda str: lambda cont: io_dirty(iof_out(str)(cont))

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

# Map IO
io_map = free_map

# Id IO
io_id = io_pure

# Join IO
io_join = free_join(iof_map)

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

# TakeAfter IO
io_take_after = take_after(io_bind)

# IO str
io_input = io_inp(io_pure)

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


main = \
    io_take_after(io_print("What's your name?"))(
    io_bind(io_input)(lambda name:
    io_print(f"Hi, {name}!")
))
# main = io_dirty(iof_out("What's your name?")(io_dirty(iof_inp(lambda name: io_dirty(iof_out(f"Hi, {name}!")(io_pure(None)))))))

io_run(main)