search

msp-strath / ask

being a particular fragment of Haskell, extended to a proof system
19 stars 1 forks source link

Layout Style Police Hang Tough? #3

Closed pigworker closed 3 years ago

pigworker commented 3 years ago

In #2, I was bothered by the possible consequences for layout of changing prove to proven. One of the options under consideration was to ban the "where-horizontal", as in

prove a & b by AndI where prove a ?
                          prove b ?

Not only because of the prove/proven thing, I am increasingly in favour of this option and am minded to go with it.

The proposed law is this:

Between a layout herald and its end of line, if there are any tokens other than whitespace or comments, the first of them must be {.

So if you want to indent after where you must take a new line, which is what we usually do and teach.

This move also mandates compliance with Hancock's Layout Law:

Ensure that your use of layout yields code invariant under alpha-equivalence.

And that means we might actually offer alpha-conversion as a transducer service. When we scope-check the input, we could note requests for renaming, then use the new name when generating the output.

Moreover, it opens the way to displaying proofs in a proportional font. Indeed, it might not be at all daft to consider multiple rendering options for ask output: what if we generated vaguely sensible html for the passive buffer (as well as stashing the raw text that you get when you click Accept)? We could even attach mouse-event-handlers to various regions (e.g., when you mouse-over a ?, it might illuminate the hypotheses in scope for it).

pigworker commented 3 years ago

Now I come to think about it, we don't need to reject the where-horizontal. In fact, we should embrace it.

pigworker commented 3 years ago 
prove a & b by AndI where prove a ?

now yields

prove a & b by AndI where {prove a ?;
                           prove b ?}

The where-horizontal is tolerated on input but shoved into braces when output. Correspondingly prove → proven doesn't break anything and we can do stuff like alpha-conversion. Issue closed.