[PRL] values and expressions

[Richard Cobbe]

On Sun, Oct 23, 2005 at 12:07:43PM -0400, Dave Herman wrote:
> >From the (operational) semanticist's perspective, if your values aren't
> >also expressions, then you need to define a whole new set of type rules
> >to handle pseudo-expressions---that is, expression ASTs that have values
> >at the leaves rather than expressions.  Otherwise, subject reduction
> >won't work; you won't even be able to state the theorem.
> 
> Sure, though in practice I don't know how much harder that has to be.

In the cases I've seen, it just requires you to write 2n+k type rules
for expressions, where n is the number of original expression type
rules, and k is the number of type rules you need to type your values.
Not hard, just really annoying, because n of those type rules are going
to be almost exact copies of the existing ones.

(And I slightly mis-spoke originally.  If you don't do this, you'll
still be able to state the subject reduction theorem, but the type
judgment in the theorem's conclusion will be trivially underivable,
because the "expression" won't pattern-match against any of your rules.)

> >From the perspective of desigining the language that the programmers
> >will actually use, it's hard to say.  I'd personally be annoyed with a
> >language in which values were not expressions, because it would feel
> >like an artificial distinction for no real reason that would possibly
> >get in the way of writing the kind of code that I like to write.  How
> >serious a problem this would actually be, though, would depend heavily
> >on circumstances.  In some applications, I might grumble about it, but
> >be able to write the program anyway with only minimal additional effort.
> 
> I think in my case it's not a big deal. Lemme describe what I'm doing.
> 
> I'm looking at an embedded language of regular expressions, where 
> expressions are things like "match this character" and union and 
> concatenation. The values are matched characters or matched strings.
> 
> You could express matched values as a subset of expressions, but then in 
> the reduction rules there's no way to distinguish a rule that says 
> "please match this character" from a rule that says "I just matched this 
> character." So I want to distinguish expressions and values to 
> disambiguate the reduction rules.

I think I basically see what you mean.  I'm not sure, though, why you
have a rule that says "I just matched this character" -- why should the
rules care about what you've already done?

In any case, my first reaction is to say that this is an unfortunate
consequence of your AST design.  It's awfully convenient, in general, to
have your value representations be a subset of your expression
representations, so I'd probably try to refactor the AST to tag the
"match this char" and "matched that char" nodes in some way that would
allow me to lump them together in one set of expressions.  But you
almost certainly have other competing design goals, so I can't say for
sure what the right solution is without looking at the system in detail.

In any case, so far as I know, you won't get into any problems by
keeping the sets of expressions and values disjoint, so long as you're
consistent about that distinction throughout the system.  (That is, you
do the right thing for, e.g., your type rules and your context
definitions, as I described above.)

Richard