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

From: Anton van Straaten <anton>
Date: Mon Feb 26 20:20:47 2007

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
Received on Mon Feb 26 2007 - 20:16:12 UTC