metafunction pre-conditions require using non-terminal-with-underscore names in contracts about redex HOT 5 CLOSED

The runtime behavior of this example is as expected. I agree that the actual error you get is terrible, however.

I have considered making it a syntax error to write something like Γ in a "term" position unless there was a binding for it, so you could get a syntax error. The trouble with that is that people often like to use x for both a non-terminal and for a literal.

The trouble with the other interpretation of the nonterminals (making them binding in contracts), is that a contract like this one:

(define-metafunction stlc
  same-constructor : e e -> #t or #f
  [(same-constructor (λ (x_1 : t_1) e_1)
                     (λ (x_2 : t_2) e_2))
   #t]
  [(same-constructor (e_1 e_2) (e_3 e_4))
   #t]
  [(same-constructor x_1 x_2)
   #t]
  [(same-constructor e_1 e_2) #f])

would be not at all what you want (it would be like the current redex writing e_1 twice in the contract).

Do you have any ideas on how to improve the situation?

from redex.

Ah, that's a good point. In fact, I realize now that I use that feature in several of my contracts.

Making unbound non-terminals in term position an error seems almost like a good idea; perhaps making this the default and adding an optional argument to allow specified non-terminals to also be literals would be a good compromise. Given that x seems like the most common instance of this, any non-terminal defined as variable-not-otherwise-mentioned could default to being treated this way.

Otherwise, perhaps documenting this more clearly in define-metafunction would be good enough. My first throught was to look at the documentation and see if I missed some hint about the behavior of #:pre, but there aren't even examples of using it in the documentation.

from redex.

from redex.

Maybe so. I suppose we could make the current behavior the default, and opt-in to the additional checking? But if it's ad-hoc-ness you worry about, maybe not.

My first ad hoc thought was to bind non-terminals from the domain of the contract when a #:pre is given, and bind them in the co-domain when #:post is given, and document this behavior carefully. This would result in contracts and pre/post conditions being more readable, I think. But.. it might be subtley confusing behavior.

As for pull requests, I'll try get around to that today. There have been a handleful of typos I've been meaning to fix in the docs anyway.

from redex.

Sounds like confusing behavior to me.

I think there's nothing to be done here with this PR anymore, so I'm going to close it. If you want to re-open, please do so.

from redex.