4 ms·

That's not how I read gp, exactly. What he is saying sounds more like taking the AST of a program, desugaring at much as possible, and then re-sugaring it in su

by alloyed 12y ago

That's not how I read gp, exactly. What he is saying sounds more like taking the AST of a program, desugaring at much as possible, and then re-sugaring it in such a way as to produce a consistently styled codebase, sort of like gofmt but more opinionated and linter-like.

shriramkmurthi 12y ago
What he wrote is "statements that are semantically absolutely identical but differ in just the 'sugar'". I was just quoting him back. Of course, one can always construct various hacky approximations to this, and maybe that's what he intended, even if it isn't what he wrote; I couldn't possibly tell.
- Dylan16807 12y ago
  The 'absolutely' should have hinted that 'semantically' wasn't the full extent of what he meant. Focus your quote onto "differ in just the 'sugar'" and you see exactly what he meant. He didn't misspeak. Sugar is a very specific term.
  - shriramkmurthi 12y ago
    I'm not actually unclear on the meaning of these words. There happen to be multiple possible interpretations of what the OP wrote, some demanding problematic things and others impossible ones. As I said in my reply to @JadeNB, we have unambiguous terminology for all this. Would have helped to have used it. As for the meaning of "sugar", I _think_ I have some inkling about what it means. We're in a discussion thread about a document on desugaring. I happen to be its author.
    - Dylan16807 12y ago
      Glad you have a very solid understanding of sugar. But that means you're being intentionally obtuse when you invoke the halting problem and discuss the entire set of programs that produce the same results. I think from https://news.ycombinator.com/item?id=8294806 https://news.ycombinator.com/item?id=8294806 that the core of your argument is about it being difficult to tease out sufficiently complex sugar, but to be honest I've almost never seen complex sugar. Most of this stuff, especially when PeterisP talks about being idiomatic, is simple transformations that you can do easily in either direction. You don't need a magical sugaring oracle, you need a language-specific sugaring oracle. And if you have a language where the sugar isn't decidable, I'd argue something has gone wrong.
      - shriramkmurthi 12y ago
        1. Then you haven't seen very much sugar. Take a look at the transformations used in Racket, for instance. Entire parts of the language that would be built into other languages are seamlessly expressed through extremely sophisticated sugar. You can "argue" all you want, but it's a perfectly sensible language definition approach, and it works superbly, without any clear indication of anything having "gone wrong". 2. I don't know what it means for "sugar" to be or not be "decidable": that sentence isn't even type-correct. But even guessing at what you might mean, making something language-specific isn't going to help you, assuming a typical Turing-complete language, if the underlying problem is not decidable. (I don't even know what a language-independent "magical sugaring oracle" might be, because any "sugaring" procedure would have to be defined relative to some language that it works on. Except, maybe, in the "magical" case, about which I don't know very much, I'm afraid.) Of course you can approximate it – you can always approximate anything you want – but you're then solving a different problem. It's fine perfectly to define that as the problem you want solved. But it helps to be clear about what one wants, and the OP was not.
        Dylan16807 12y ago
        By 'decidable' I meant that you can write an always-correct, always-halting algorithm for taking a desugared program in the language and transforming it into an 'idiomatic' sugared form. Then you have a nice bidirectional idempotent transform. (The 'gone wrong' was more in the definition of 'sugar' but I don't want to argue that, just ignore that line.) Most languages have a fixed set of simple sugar. There is no approximation needed; you can make a 100% perfect sugar/desugar mechanism. I'm glad you agree that it should be language-specific. That way we can discuss the typical language where the language itself is Turing-complete but the sugar-related transformations are not even close to Turing-complete. The original statement discussed having an ability to transform code into an idiomatic form as a 'language feature'. This means it's intertwined with the design of the sugar itself, and it's up to the language designers to make it feasible. When you discuss all the ways a program could arrive at the same result, you are going far beyond the realm of the finite sugars that apply to a specific language. The Halting Problem is not relevant.
- JadeNB 12y ago
  I think that this is (quite) a bit like claiming (verified) compiler optimisations are impossible because they, too, have to re-write any given expression only to a semantically identical one. One wants to detect only pairs of statements that are semantically identical; this does not require detecting all such pairs.
  - shriramkmurthi 12y ago
    Look, the OP could have been precise. We have terminology that makes all these things very exact. That's why terms like "soundness", "completeness", etc. were invented. The OP wrote something that is ambiguous. I was pointing out why it's tricky. You're welcome to interpret it in a way that makes it less tricky. However, what you're asking for still requires a pretty strong decision procedure if you want something that is actually of use on non-trivial examples. If you have expressions that are nested, then you need to be able to reason about all possible contexts; if you have state, you need to reason about all possible states. Maybe you have lots of experience with this kind of reasoning and have gotten used to it, but I find the necessary underlying proofs (whether human or automated) pretty heavy going.

by alloyed 12y ago

shriramkmurthi 12y ago

What he wrote is "statements that are semantically absolutely identical but differ in just the 'sugar'". I was just quoting him back. Of course, one can always construct various hacky approximations to this, and maybe that's what he intended, even if it isn't what he wrote; I couldn't possibly tell.

Dylan16807 12y ago
The 'absolutely' should have hinted that 'semantically' wasn't the full extent of what he meant. Focus your quote onto "differ in just the 'sugar'" and you see exactly what he meant. He didn't misspeak. Sugar is a very specific term.
- shriramkmurthi 12y ago
  I'm not actually unclear on the meaning of these words. There happen to be multiple possible interpretations of what the OP wrote, some demanding problematic things and others impossible ones. As I said in my reply to @JadeNB, we have unambiguous terminology for all this. Would have helped to have used it. As for the meaning of "sugar", I _think_ I have some inkling about what it means. We're in a discussion thread about a document on desugaring. I happen to be its author.
  - Dylan16807 12y ago
    Glad you have a very solid understanding of sugar. But that means you're being intentionally obtuse when you invoke the halting problem and discuss the entire set of programs that produce the same results. I think from https://news.ycombinator.com/item?id=8294806 https://news.ycombinator.com/item?id=8294806 that the core of your argument is about it being difficult to tease out sufficiently complex sugar, but to be honest I've almost never seen complex sugar. Most of this stuff, especially when PeterisP talks about being idiomatic, is simple transformations that you can do easily in either direction. You don't need a magical sugaring oracle, you need a language-specific sugaring oracle. And if you have a language where the sugar isn't decidable, I'd argue something has gone wrong.
    - shriramkmurthi 12y ago
      1. Then you haven't seen very much sugar. Take a look at the transformations used in Racket, for instance. Entire parts of the language that would be built into other languages are seamlessly expressed through extremely sophisticated sugar. You can "argue" all you want, but it's a perfectly sensible language definition approach, and it works superbly, without any clear indication of anything having "gone wrong". 2. I don't know what it means for "sugar" to be or not be "decidable": that sentence isn't even type-correct. But even guessing at what you might mean, making something language-specific isn't going to help you, assuming a typical Turing-complete language, if the underlying problem is not decidable. (I don't even know what a language-independent "magical sugaring oracle" might be, because any "sugaring" procedure would have to be defined relative to some language that it works on. Except, maybe, in the "magical" case, about which I don't know very much, I'm afraid.) Of course you can approximate it – you can always approximate anything you want – but you're then solving a different problem. It's fine perfectly to define that as the problem you want solved. But it helps to be clear about what one wants, and the OP was not.
      - Dylan16807 12y ago
        By 'decidable' I meant that you can write an always-correct, always-halting algorithm for taking a desugared program in the language and transforming it into an 'idiomatic' sugared form. Then you have a nice bidirectional idempotent transform. (The 'gone wrong' was more in the definition of 'sugar' but I don't want to argue that, just ignore that line.) Most languages have a fixed set of simple sugar. There is no approximation needed; you can make a 100% perfect sugar/desugar mechanism. I'm glad you agree that it should be language-specific. That way we can discuss the typical language where the language itself is Turing-complete but the sugar-related transformations are not even close to Turing-complete. The original statement discussed having an ability to transform code into an idiomatic form as a 'language feature'. This means it's intertwined with the design of the sugar itself, and it's up to the language designers to make it feasible. When you discuss all the ways a program could arrive at the same result, you are going far beyond the realm of the finite sugars that apply to a specific language. The Halting Problem is not relevant.
JadeNB 12y ago
I think that this is (quite) a bit like claiming (verified) compiler optimisations are impossible because they, too, have to re-write any given expression only to a semantically identical one. One wants to detect only pairs of statements that are semantically identical; this does not require detecting all such pairs.
- shriramkmurthi 12y ago
  Look, the OP could have been precise. We have terminology that makes all these things very exact. That's why terms like "soundness", "completeness", etc. were invented. The OP wrote something that is ambiguous. I was pointing out why it's tricky. You're welcome to interpret it in a way that makes it less tricky. However, what you're asking for still requires a pretty strong decision procedure if you want something that is actually of use on non-trivial examples. If you have expressions that are nested, then you need to be able to reason about all possible contexts; if you have state, you need to reason about all possible states. Maybe you have lots of experience with this kind of reasoning and have gotten used to it, but I find the necessary underlying proofs (whether human or automated) pretty heavy going.