3 ms·

I don't think an explicit effect system is required to implement most (maybe all?) of the optimizations. Actually I think these techniques are probably applica

I don't think an explicit effect system is required to implement most (maybe all?) of the optimizations. Actually I think these techniques are probably applicable to many strict, mostly-functional languages with few to no cycles or mutable references. In fact, they cite Lean as their inspiration for many of these techniques.

Someone 6y ago
I would think that, if the compiler can check that the annotations are correct, it also can generate them if none are given (one way to do that: ‘just’ generate any possible combination of annotations, check which are correct, and pick the minimal set. Of course, a production-level compiler would use a faster algorithm) If so, you still might have to annotate some library functions that are implemented outside the language, but that would be it. The annotations are there for the programmer as, without them, it would be hard to keep track of which of your functions are pure, which might throw, etc.
- Jweb_Guru 6y ago
  That's certainly not true in general (at least, if you want your compiler to provably halt) and it's really easy to point at counterexamples... for instance, Coq is capable of fully representing Peano arithmetic, and is dependently typed, so it follows that synthesizing its proof terms can require supplying proofs of arbitrary statements in PA, which is undecidable. But typechecking Coq proof terms is very much decidable, or at least if it isn't it's not because it includes PA. That being said, even if your standard for synthesis is "works in practice" rather than some halting-related criterion, it's still really easy to find type systems that don't qualify. There are also sometimes practical concerns around separate compilation--if you're relying on introspection and not just interfaces for typechecking, and someone just tells you what interface will be satisfied at runtime, you won't be able to repeat this kind of analysis; the same sorts of problems occur when you perform reflection.
  - Someone 6y ago
    I don’t follow that argument. I know that checking a proof almost always is a lot simpler than creating it (and certainly never harder), but when a programmer annotates a function, they don’t provide a proof that the property holds, they just make an assertion that the it holds, and the compiler has to check it. If the compiler can do such a check, and the number of possible annotations is finite, it can check each of them, thus computing the set of annotations that the function adheres to.
    - Jweb_Guru 6y ago
      Well, the problem is that the number of annotations is not finite, and often there are many valid signatures that would work for a function. Determining which ones make the whole program typecheck is not a decidable problem for most type systems, and even for those for which it is, this often requires sufficient amounts of global knowledge to make the problem totally intractable in practice. This is a problem you run into very quickly--for example, Hindley-Milner is only decidable because it will only infer "forall a" in prenex form (so its "most general" annotation is only most-general in that context). Type inference if you allow non-prenex quantification--even very mild non-prenex quantification--is undecidable, despite these being just as easy to typecheck as the prenex versions! Now, in practice programs are made up finite numbers of terms, so for some of these type systems you could certainly come up with some sort of semidecision procedure by iterating through every possible sequence of type annotations. But as this kind of brute force algorithm will not terminate if it can't find the right set of annotations, and in practice will not terminate within human lifespans even in most cases where the right set of annotations exist, I don't think people would be very happy with such a system. This is especially true if the only reason to find the annotations was to perform program optimizations, and not to enforce correctness. People are already wholly unwilling to give compilers unlimited amounts of time to do interprocedural analysis, which is mostly done in LLVM and such by just inlining everything. If having effect annotations were actually critical for being able to apply the optimizations from the paper (which, like I said earlier, I don't know that they are), this would pretty much be another instance of a global program rewrite too expensive for an optimizing compiler to perform in practice.
    - 6y ago

Someone 6y ago

I would think that, if the compiler can check that the annotations are correct, it also can generate them if none are given (one way to do that: ‘just’ generate any possible combination of annotations, check which are correct, and pick the minimal set. Of course, a production-level compiler would use a faster algorithm) If so, you still might have to annotate some library functions that are implemented outside the language, but that would be it. The annotations are there for the programmer as, without them, it would be hard to keep track of which of your functions are pure, which might throw, etc.

Jweb_Guru 6y ago
That's certainly not true in general (at least, if you want your compiler to provably halt) and it's really easy to point at counterexamples... for instance, Coq is capable of fully representing Peano arithmetic, and is dependently typed, so it follows that synthesizing its proof terms can require supplying proofs of arbitrary statements in PA, which is undecidable. But typechecking Coq proof terms is very much decidable, or at least if it isn't it's not because it includes PA. That being said, even if your standard for synthesis is "works in practice" rather than some halting-related criterion, it's still really easy to find type systems that don't qualify. There are also sometimes practical concerns around separate compilation--if you're relying on introspection and not just interfaces for typechecking, and someone just tells you what interface will be satisfied at runtime, you won't be able to repeat this kind of analysis; the same sorts of problems occur when you perform reflection.
- Someone 6y ago
  I don’t follow that argument. I know that checking a proof almost always is a lot simpler than creating it (and certainly never harder), but when a programmer annotates a function, they don’t provide a proof that the property holds, they just make an assertion that the it holds, and the compiler has to check it. If the compiler can do such a check, and the number of possible annotations is finite, it can check each of them, thus computing the set of annotations that the function adheres to.
  - Jweb_Guru 6y ago
    Well, the problem is that the number of annotations is not finite, and often there are many valid signatures that would work for a function. Determining which ones make the whole program typecheck is not a decidable problem for most type systems, and even for those for which it is, this often requires sufficient amounts of global knowledge to make the problem totally intractable in practice. This is a problem you run into very quickly--for example, Hindley-Milner is only decidable because it will only infer "forall a" in prenex form (so its "most general" annotation is only most-general in that context). Type inference if you allow non-prenex quantification--even very mild non-prenex quantification--is undecidable, despite these being just as easy to typecheck as the prenex versions! Now, in practice programs are made up finite numbers of terms, so for some of these type systems you could certainly come up with some sort of semidecision procedure by iterating through every possible sequence of type annotations. But as this kind of brute force algorithm will not terminate if it can't find the right set of annotations, and in practice will not terminate within human lifespans even in most cases where the right set of annotations exist, I don't think people would be very happy with such a system. This is especially true if the only reason to find the annotations was to perform program optimizations, and not to enforce correctness. People are already wholly unwilling to give compilers unlimited amounts of time to do interprocedural analysis, which is mostly done in LLVM and such by just inlining everything. If having effect annotations were actually critical for being able to apply the optimizations from the paper (which, like I said earlier, I don't know that they are), this would pretty much be another instance of a global program rewrite too expensive for an optimizing compiler to perform in practice.
  - 6y ago