[PRL] values and expressions

[David Herman]

> 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.

Sure, that's a good point. You could partly alleviate this to some  
degree by describing a single type of contexts that accept a union of  
expressions or values in the hole, and then just proving the theorems  
once. But you're still having to split each case into two sub-cases,  
and now you can't even factor those out into separate lemmas. So your  
point still stands.

There's a part of me that still feels like it's a hack to force the  
values to be a subset of expressions when sometimes they just aren't.  
OTOH, in a reduction system, where everything is "dumb syntax," maybe  
it makes sense to think of values as expressions since they are terms  
anyways.

> 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?

Fair enough. I can show you the details in person. Sorry for the  
ambiguity; I was just looking for general points about the  
ramifications of distinguishing values from expressions (though  
specifically in the context of reduction semantics).

> 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.

Yes, I'll probably do that.

> 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.)

I might point out that we're just talking about regexps here--  
there's no type system. But hey, it could happen. Maybe somebody'll  
want to come along and, I don't know, make them Turing-complete. Not  
that anyone would ever wanna do that (*cough*)...

Dave