Why do we need inline, measure, and reflection?

[facundominguez]

When discussing Liquid Haskell with people unfamiliar with it, the question pops up of why do we need three separate mechanisms to put Haskell functions in the logic. The situation is puzzling, in particular, because reflection seems to be general enough to subsume the measure and inline forms.

This ticket is to collect an answer and to put it somewhere in the documentation.

---

I think of it as an historical artifact, where PLE is still not polished to use the reflection form everywhere. But I'd like to know what others think.

[AlecsFerra]

• inline: if they appear in some refinement the definition is inlined before constraint checking time
• measure: they are a way to tag constructors with refinement information, the function needs to be defined structurally for this reason, the refinement is added statically before verification/ple (I always think of them as a weaker version of prop but I might be biased 😂)
• reflection: the thing that actually allows you to use haskell in the refinements and with ple allows you to automate equational reasoning

Regarding the explaination I think the issue steems from the fact that the user should be exposed to this
as the compiler can figure out by itself if something can be a measure or no (otherwise there would be no error message if something is not defined structurally but it is annotated as a measure), I also cant find any reason to have inline

[AlecsFerra]

In my ple maximalist dreams there is no annotation at all, everything is reflected/measured and ple is on by default :)