4 ms·

I would suggest that effects which are "directly" embedded are impure effects (w.r.t. our other thread). Essentially, without reifying them into values with typ

by tel 11y ago

I would suggest that effects which are "directly" embedded are impure effects (w.r.t. our other thread). Essentially, without reifying them into values with types it's harder to reason about them. A more interesting dividing line are things like computation effect typing in languages like Bauer and Pretnar's "Eff" or McBride's "Frank". http://www.eff-lang.org/ http://www.eff-lang.org/ http://homepages.inf.ed.ac.uk/slindley/papers/frankly-draft-march2014.pdf http://homepages.inf.ed.ac.uk/slindley/papers/frankly-draft-... But yes, if you consider other "practical, modern" languages, many retain impurity.

mafribe 11y ago
There are very different options. First, approaches like Eff take pure functional computation as a basis and layer effects like call/cc or concurrency on top of that. I think it's better to go the other way and take concurrency, or, if you want to start sequential, a lambda-calculus with jumps a la call/cc or lambda-mu, as a basis see pure functional computation as a restriction of the base calculus. Second, it's unclear that effects should be reflected in types for reasoning. That road leads to complicated typing systems without type inferences (see also dependent types). I think the following alternative is more appealing: stick with lightweight types (think Hindley-Milner), and leave reasoning to an external calculus (variants of Hoare logic).
- tel 11y ago
  That "analytic" style you suggest is really interesting, too. I'm not sure I have a dog in the ultimate race and I'd love to see both analytic and synthetic styles flourish, but from a mere terminology point of view I'd distinguish between the two languages in means of describing them as "pure" or not. I also really worry that external proofs will ultimately be neglected in practice. I suppose this is again a "UX of Types" thing, but I'm something of a believer that anything that you do not literally demand of the programmer will eventually be sacrificed.
  - mafribe 11y ago
    I'm not totally sure what you mean by "external proofs will ultimately be neglected".

by tel 11y ago

mafribe 11y ago

There are very different options. First, approaches like Eff take pure functional computation as a basis and layer effects like call/cc or concurrency on top of that. I think it's better to go the other way and take concurrency, or, if you want to start sequential, a lambda-calculus with jumps a la call/cc or lambda-mu, as a basis see pure functional computation as a restriction of the base calculus. Second, it's unclear that effects should be reflected in types for reasoning. That road leads to complicated typing systems without type inferences (see also dependent types). I think the following alternative is more appealing: stick with lightweight types (think Hindley-Milner), and leave reasoning to an external calculus (variants of Hoare logic).

tel 11y ago
That "analytic" style you suggest is really interesting, too. I'm not sure I have a dog in the ultimate race and I'd love to see both analytic and synthetic styles flourish, but from a mere terminology point of view I'd distinguish between the two languages in means of describing them as "pure" or not. I also really worry that external proofs will ultimately be neglected in practice. I suppose this is again a "UX of Types" thing, but I'm something of a believer that anything that you do not literally demand of the programmer will eventually be sacrificed.
- mafribe 11y ago
  I'm not totally sure what you mean by "external proofs will ultimately be neglected".