[r6rs-discuss] [Formal] Allow compilers to reject obvious violations

[Anton van Straaten]

Joe Marshall wrote:
> On 2/24/07, Anton van Straaten <anton at appsolutions.com> wrote:
> 
>> Joe Marshall wrote:
>> > On 2/24/07, John Cowan <cowan at ccil.org> wrote:
>> >
>> >> Matthias Felleisen scripsit:
>> >>
>> >> >  1. When an implementation is allowed to reject a program without
>> >> > running it, it comes with a filter also known as a type system.
>> >>
>> >> I think that rather stretches the definition of "type system".
>> >
>> >
>> > It doesn't, actually, if you use the terminology of the static type
>> > community.  A `type system' would encompass any system that
>> > performs analysis on the program without actually attempting to
>> > execute it.
>>
>> This assumes that you actually have "a program".  Type theorists don't
>> usually refer to syntax errors as type errors.
> 
> 
> Type theorists have their own unique way of looking at the world.

Undoubtedly, but since you were referring to the terminology of the 
static type community, my response was intended in the same context.

>> John Cowan's proposed text (if (foo)) can be rejected as not being a
>> valid program without involving a type system, so even without using a
>> stretchy definition of "type system", it doesn't contradict Matthias'
>> statement.
> 
> 
> I disagree.  You can't make a judgement about (if (foo)) without at least
> assigning some interpretation to the token `if'.

I'm a little confused by this.  Ignoring, for the moment, Lisp/Scheme's 
unique approach to syntax, it is certainly possible to identify an 
expression such as (if (foo)) as being a syntax error without coming to 
any conclusion about the type of the term that it was intended to 
represent.

RnRS defines 'if' as syntax which requires at least a <consequent> 
clause.  Lacking such a clause, it's not possible to talk about that 
'if' as a valid term, so it's not meaningful to talk about the term's 
type.  I suppose one could argue that if one is willing to accord it 
provisional status as a term, that it's not possible to give such a term 
a type, and therefore this is a type error.  That seems perverse to me, 
and it's not something I've noticed the static type community doing.

So am I missing something?  (Matthias suggested "see Reynolds and all 
the literature that follows".  I'll get right on that, but it may take 
me a few more hours to finish it all.)

Anton