5 ms·

Though I don’t use it professionally, I believe purescript has proven that algebraic effects systems are very useful for granular effect handling. Things like

by rtpg 7y ago

Though I don’t use it professionally, I believe purescript has proven that algebraic effects systems are very useful for granular effect handling. Things like “this writes to the database”, “this makes an unbounded query”, “this requires a random number generator “, rather than a nebulous “oh this has I/O” is very powerful and useful for maintaining a system

pron 7y ago
> Things like “this writes to the database”, “this makes an unbounded query”, “this requires a random number generator “, rather than a nebulous “oh this has I/O” is very powerful and useful for maintaining a system 1. How do you know that? 2. Why? 3. Why is tracking the effects in the type system useful? Even if and where this is important, it could be easily achieved using something like Java's 20+-year-old security manager and with finer granularity (i.e. you can allow code to read or write certain files, connect to certain domains etc.) [1]. Just because you can do something in the type system, doesn't mean you should, as it may not be the best way. [1]: https://docs.oracle.com/en/java/javase/13/security/permissions-jdk1.html https://docs.oracle.com/en/java/javase/13/security/permissio...
- hopia 7y ago
  As for 3. Haskell already does it now with the IO monad. I can see how having something more specific for effects than the most generic IO type is the next step on an evolutionary path for languages with an advanced type system. The concern whether or not it is worthwhile then extends to the whole type system.
- IceDane 7y ago
  Because it is a way to force you think about how you structure your code. You necessarily pull out the pure parts and are explicit in handling all the impure parts. This also makes it very easy to test your code. Why is it done in the type system? Well, because the goal is to have guarantees at compile-time, and this happens to be something that can be expressed in a sufficiently powerful type system.
  - pron 7y ago
    > Well, because the goal is to have guarantees at compile-time No, that's no one's goal. The goal is to increase correctness as much as possible prior to shipping. BTW, reducing soundness guarantees is all the rage in FM research these days [1] precisely because soundness has a high cost, and it is rarely needed for non-simple, technical properties. [1]: https://dl.acm.org/doi/pdf/10.1145/3371078?download=true https://dl.acm.org/doi/pdf/10.1145/3371078?download=true
    - jbjohns 7y ago
      This strikes me as a pretty bizarre statement. The more checks I can put into the compiler, the less tests I have to write. Tests are also code and come with development and maintenance costs. Since a software project's costs correlate directly with lines of code, the less you can write to get the job done the better.
      - pron 7y ago
        Type checks done by the compiler and tests that you manually have to write are not the only two available techniques. Again, the goal is not to have the compiler do anything, but to produce software that's as correct as needed for the lowest cost.
    - Cladode 7y ago
      This comment is deeply misleading. O'Hearn's incorrectness logic that you cite in your [1] is perfectly sound. It just changes the meaning of Hoare triples from over-approximation to under-approximation. In brief: - Hoare logic soundly over-approximates - Incorrectness logic soundly under-approximates Sound under-approximation is extremely useful when you want to prove that a certain problem must arise in code, rather than may arise. The problem with logic based program verification has often been that your prover could not prove that a program was correct, but, due to over-approximation of traditional Hoare logic, the best you could learn from this failure was (simplifying a great deal) that something may go wrong. That is not particularly useful in practise, since often this is a false alert.
- rtpg 7y ago
  1. You create special effect types for each effect you want to track 2. One example: make sure that HTTP routes that are GET will at most just read the DB, not write 3. I actually don’t like that the type system is where this is going into. I want to have some form of static analysis, and this is providing it.
ppseafield 7y ago
Didn't the new Effect type remove this granularity?

by rtpg 7y ago

pron 7y ago

> Things like “this writes to the database”, “this makes an unbounded query”, “this requires a random number generator “, rather than a nebulous “oh this has I/O” is very powerful and useful for maintaining a system 1. How do you know that? 2. Why? 3. Why is tracking the effects in the type system useful? Even if and where this is important, it could be easily achieved using something like Java's 20+-year-old security manager and with finer granularity (i.e. you can allow code to read or write certain files, connect to certain domains etc.) [1]. Just because you can do something in the type system, doesn't mean you should, as it may not be the best way. [1]: https://docs.oracle.com/en/java/javase/13/security/permissions-jdk1.html https://docs.oracle.com/en/java/javase/13/security/permissio...

hopia 7y ago
As for 3. Haskell already does it now with the IO monad. I can see how having something more specific for effects than the most generic IO type is the next step on an evolutionary path for languages with an advanced type system. The concern whether or not it is worthwhile then extends to the whole type system.
IceDane 7y ago
Because it is a way to force you think about how you structure your code. You necessarily pull out the pure parts and are explicit in handling all the impure parts. This also makes it very easy to test your code. Why is it done in the type system? Well, because the goal is to have guarantees at compile-time, and this happens to be something that can be expressed in a sufficiently powerful type system.
- pron 7y ago
  > Well, because the goal is to have guarantees at compile-time No, that's no one's goal. The goal is to increase correctness as much as possible prior to shipping. BTW, reducing soundness guarantees is all the rage in FM research these days [1] precisely because soundness has a high cost, and it is rarely needed for non-simple, technical properties. [1]: https://dl.acm.org/doi/pdf/10.1145/3371078?download=true https://dl.acm.org/doi/pdf/10.1145/3371078?download=true
  - jbjohns 7y ago
    This strikes me as a pretty bizarre statement. The more checks I can put into the compiler, the less tests I have to write. Tests are also code and come with development and maintenance costs. Since a software project's costs correlate directly with lines of code, the less you can write to get the job done the better.
    - pron 7y ago
      Type checks done by the compiler and tests that you manually have to write are not the only two available techniques. Again, the goal is not to have the compiler do anything, but to produce software that's as correct as needed for the lowest cost.
  - Cladode 7y ago
    This comment is deeply misleading. O'Hearn's incorrectness logic that you cite in your [1] is perfectly sound. It just changes the meaning of Hoare triples from over-approximation to under-approximation. In brief: - Hoare logic soundly over-approximates - Incorrectness logic soundly under-approximates Sound under-approximation is extremely useful when you want to prove that a certain problem must arise in code, rather than may arise. The problem with logic based program verification has often been that your prover could not prove that a program was correct, but, due to over-approximation of traditional Hoare logic, the best you could learn from this failure was (simplifying a great deal) that something may go wrong. That is not particularly useful in practise, since often this is a false alert.
rtpg 7y ago
1. You create special effect types for each effect you want to track 2. One example: make sure that HTTP routes that are GET will at most just read the DB, not write 3. I actually don’t like that the type system is where this is going into. I want to have some form of static analysis, and this is providing it.

ppseafield 7y ago

Didn't the new Effect type remove this granularity?