search

robrix / path

A lambda calculus to explore type-directed program synthesis.
BSD 3-Clause "New" or "Revised" License
83 stars 2 forks source link

IO effects #28

Open robrix opened 5 years ago

robrix commented 5 years ago

It would be nice if we could compile (cf #20) executables which can actually do something, which means we need some effect(s) modelling input/output, e.g. via stdin/stdout/stderr, the filesystem, and so on.

If we give a proper treatment of these effects like others, we can enable users to provide handlers for IO effects just like any others (e.g. to simulate a filesystem, batch reads, etc.).

cf #27 for algebraic & scoped effects

robrix commented 5 years ago

Note that I’m not proposing that we have a single monolithic IO effect as counterpart to the monolithic IO monad in Haskell; rather, we should have a variety of effects specifying different interactions, some of which can be interpreted by the runtime system (cf #29).