Bulat Ziganshin wrote:
Thursday, October 19, 2006, 5:54:06 PM, you wrote:
I propose that haskell' include a standard syntax for invariants that the programmer wants to express.
The intent is not to have standardized checks on the invariants, its just to supply a common way to specify invariants to that the various strategies for checking them can all work from the same data. For example, one tool might use the invariants to generate QuickCheck properties
seems that it should be a sort of annotation, yes? so we again need to define common annotation syntax and you can add this as one more possible usage to annotations-proposal page
It does seem to fit as an annotation. What I am worried about, however, is that if there is no 'official' way to annotate the invariants, then the tool writers will come up with their own slightly incompatible invariant annotations, which would be a shame. This actually seems to be a common issue with annotations. Some of the other proposals are looking to use annotations to specify language extensions that are in effect, and they will also need an 'official' syntax if they want all the compilers to recognize them in the same way. Writing the invariants using a common annotation syntax is great idea though! In fact its better than what I originally had in mind because some tools that use the invariants may need additional information that isn't contained in the common invariant syntax. For instance, I expect any purely static checking of the invariants will probably need help from the developer at various points in a function to complete the proof. When you talk about the "annotations-proposal page", you are referring to the trac ticket right? http://hackage.haskell.org/trac/haskell-prime/ticket/88 Should I apply for an account on trac and modify the ticket?