3 ms·

I didn't see this addressed in the article: Do these annotations have force? I've run into plenty of annotations that lie - how can I trust that code that's an

I didn't see this addressed in the article: Do these annotations have force? I've run into plenty of annotations that lie - how can I trust that code that's annotated as being side-effect-free actually is?

kqr 11y ago
> Not only do these type systems allow you to annotate things as "doing side effects"; they specifically disallow doing side effects unless you have annotated the thing as such. Just below the "Controlled Side Effects" heading.
lmm 11y ago
Any practical language will have escape hatches, but it's the equivalent of doing a cast (indeed it sometimes literally is doing a cast) - it sticks out in code review, compilers have options to warn or ban them altogether.
adrusi 11y ago
Maybe the author, presumably well versed in type systems, assumed that the use of effect typing was implied. If you're not familiar go check it out, but I'll give a synopsis. If you're familiar with `unsafe' in Rust, it's a specific case of effect typing. You can annotate a function with an effect (useful examples: unsafe, impure, throws exceptions) and then if another function calls that function, then it needs to also be annotated with that effect, or else the compiler emits and error. Usually there will also be an escape hatch where you can assert to the compiler that you know, in a way that it can't statically prove, that a certain call to, say, an impure function, still doesn't have side effects. Code that appears within these escape hatches needs to be heavily tested in order for effect typing to be useful. For the above examples of effect types, the compiler will also consider certain non-function-call constructs to have an effect annotation. Dereferencing an arbitrary integer as a pointer, for example, would effectively have an "unsafe" annotation. I believe Nim has a generalized implementation of effect typing.

kqr 11y ago

> Not only do these type systems allow you to annotate things as "doing side effects"; they specifically disallow doing side effects unless you have annotated the thing as such. Just below the "Controlled Side Effects" heading.

lmm 11y ago

Any practical language will have escape hatches, but it's the equivalent of doing a cast (indeed it sometimes literally is doing a cast) - it sticks out in code review, compilers have options to warn or ban them altogether.

adrusi 11y ago

Maybe the author, presumably well versed in type systems, assumed that the use of effect typing was implied. If you're not familiar go check it out, but I'll give a synopsis. If you're familiar with `unsafe' in Rust, it's a specific case of effect typing. You can annotate a function with an effect (useful examples: unsafe, impure, throws exceptions) and then if another function calls that function, then it needs to also be annotated with that effect, or else the compiler emits and error. Usually there will also be an escape hatch where you can assert to the compiler that you know, in a way that it can't statically prove, that a certain call to, say, an impure function, still doesn't have side effects. Code that appears within these escape hatches needs to be heavily tested in order for effect typing to be useful. For the above examples of effect types, the compiler will also consider certain non-function-call constructs to have an effect annotation. Dereferencing an arbitrary integer as a pointer, for example, would effectively have an "unsafe" annotation. I believe Nim has a generalized implementation of effect typing.