[HN Gopher] First-Class I/O
___________________________________________________________________
First-Class I/O
Author : lukastyrychtr
Score : 43 points
Date : 2021-04-11 08:37 UTC (14 hours ago)
(HTM) web link (blog.sunfishcode.online)
(TXT) w3m dump (blog.sunfishcode.online)
| catern wrote:
| More about this can be found in the literature on using
| capabilities to provide/implement effect systems. For example:
|
| - "Capabilities: Effects for Free":
| https://www.cs.cmu.edu/~aldrich/papers/effects-icfem2018.pdf
|
| - "Effects as Capabilities: Effect Handlers and Lightweight
| Effect Polymorphism" https://dl.acm.org/doi/pdf/10.1145/3428194
|
| I think this is a quite effective approach and I hope it is used
| more. In some sense it's just good coding style, which lets you
| do effect-system-style reasoning in any language.
| refenestrator wrote:
| Can someone tell me a positive reason to do I/O with monads or
| try to make it pure-functional?
|
| It's always smelled like zealotry to me -- I/O is,
| definitionally, about creating a side-effect, and papering over
| that seems to add complexity and unnecessary concepts before
| eventually just calling the same libc functions anyways at the
| bottom of the stack.
| ilikebits wrote:
| Let's separate two related but distinct concepts here: (1)
| effect tracking, and (2) monadic IO.
|
| ---
|
| The concept you're asking about is called "effect tracking",
| and the argument for effect tracking is very similar to the
| argument for static types.
|
| In a world without static types, functions can be passed values
| of any type, and can return values of any type. Adding static
| types makes this code easier to reason about because we can
| statically enforce (i.e. enforce without needing any runtime
| checks) that functions only take values of a certain type or
| return values of a certain type. This makes reasoning about the
| code easier because it limits the possible things that a
| function can take or return, so instead of thinking about "what
| happens if I provide any kind of value to this function?", you
| can think "I know this function takes an integer, so I only
| need to worry about understanding how it behaves when provided
| something that is an integer".
|
| In a world without effect tracking (this is most programming
| languages today), functions can perform any side effect. Adding
| effect tracking makes this code easier to reason about because
| we can statically enforce which side effects a function does.
| For example, effect tracking makes it possible to express "this
| function takes a callback function as an argument, but that
| callback argument is not allowed to print anything".
| Alternatively, you can also look at a function and know for a
| fact that might do IO, or that it doesn't do IO. When you're
| debugging, this helps narrow down the scope of places that
| could be doing something wrong, because now you'll never have a
| function that _looks_ like it's doing something innocuous, but
| is secretly writing a log statement to a file, or pinging an
| API over the network, or drawing something to your GUI window.
|
| ---
|
| Monads are a way to _implement_ effect tracking within an
| existing type system, rather than inventing a separate,
| orthogonal "effect tracking system". This allows us to reuse a
| lot of the existing tools and theories that we understand about
| types and type theory, and apply them to how we do effect
| tracking.
|
| Exactly how this implementation works is another topic that
| gets a bit involved. But note: (1) there are ways to do effect
| tracking that are _not_ monads, or that do _not_ integrate with
| the type system that the language uses for values; and (2)
| monads have applications that are _not_ effect tracking.
| Sonata wrote:
| The important thing is that it separates the order of side-
| effects from the order of evaluation of expressions. This isn't
| a particularly important distinction in an imperative language,
| but in a functional language when you introduce things like
| laziness and memoization, the order in which expressions will
| be evaluated is not obvious.
|
| Because pure I/O preserves referential transparency, it gives
| the compiler far more ability the optimize the code by changing
| how, when and whether things are evaluated, while still being
| able to prove that it has not modified the external behaviour
| of the program.
|
| Haskell doesn't use pure I/O out of zealotry - without it,
| Haskell couldn't and be lazy-by-default and the compiled code
| would probably be much slower.
| Rerarom wrote:
| I once asked a FP enthusiast and the answer was it makes formal
| reasoning about the code easier.
| wallacoloo wrote:
| > A possible direction for future exploration would be to use the
| rustc driver API to create a custom static analysis tool that
| could recognize some form of syntax for this and then check that
| "explicit" functions don't accidentally call "non-explicit"
| functions without explicit overrides, much like unsafe.
|
| By "some form of syntax", it could be as simple as an attribute.
| Those are easily consumable by rustc plugins* or even proc-
| macros.
|
| #[explicit] fn my_explicit_fn() { ... }
|
| If traits could be implemented on functions, you could even pull
| it off with a proc-macro-derive: no need to use a custom rustc
| binary for that. Your proc-macro just scans all the function
| calls made within said function and then adds something like:
|
| unsafe impl Explicit for my_explicit_fn where
| fn_called_from_my_explicit_fn: Explicit,
| other_fn_called_from_my_explicit_fn: Explicit {}
|
| You'd need to enable the trivial trait bounds feature for
| something like the above to work.
|
| Cool ideas. I'd love to see rust become flexible enough that
| people are able to experiment with more things like this without
| having to hack at rustc's source code.
|
| * outdated terminology, but I think conceptually you still do
| this sort of thing with a plugin-like system.
| [deleted]
| ExcavateGrandMa wrote:
| WTH this syntax from hell... sounds even worst than cpp...
___________________________________________________________________
(page generated 2021-04-11 23:01 UTC)