Xref: utzoo comp.object:3438 comp.lang.misc:7703 comp.lang.eiffel:1567
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!crdgw1!uunet!mcsun!ukc!mucs!cs.man.ac.uk!mario
From: mario@cs.man.ac.uk (Mario Wolczko)
Newsgroups: comp.object,comp.lang.misc,comp.lang.eiffel
Subject: Re: A Hard Problem for Static Type Systems
Message-ID: <2479@m1.cs.man.ac.uk>
Date: 1 May 91 18:19:34 GMT
References: <1991Apr20.010347.28984@leland.Stanford.EDU> <554@eiffel.UUCP> <1991Apr26.203642.17387@leland.Stanford.EDU> <556@eiffel.UUCP> <1146@tetrauk.UUCP>
Sender: news@cs.man.ac.uk
Reply-To: mario@cs.man.ac.uk (Mario Wolczko)
Followup-To: comp.object
Organization: Department of Computer Science, University of Manchester
Lines: 41

In article <1146@tetrauk.UUCP>, rick@tetrauk.UUCP (Rick Jones) writes:
> Fact:	A program is type-safe if no feature is ever called on an object which
> 	does not support that feature.

[description of GTA with example deleted]

> supertype of A.  However, var's implicit type is also a supertype of A.
> Provided no object is ever attached to var which is a supertype of var's
> IMPLICIT type, then the system is type-safe.  

> This analysis is statically feasible, and is what GTA sets out to do.
  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Nonsense.  It is easy to construct a program which is type-safe by
your definition but cannot be verified as type-correct by static
analysis.  If you could verify all such programs, you would have
solved the Halting Problem.

Consider this program in a dynamically-typed language:
	var X;
	if predicate1
	then X := L1;  /* L1 is an object that has feature F */
	else X := L2;  /* L2 is an object that does not have feature F */
	fi
	X.F;

There is no way at compile time to tell whether this program is
type-safe or not.  Predicate1 could invoke an artbirary amount of
computation, but always result in "true".  It could be based on user
input (isodd(readnum())), which cannot be foreseen.

There will always be programs that are type-safe, but cannot be
verified as type-safe by a static type system.

Mario Wolczko

   ______      Dept. of Computer Science   Internet:      mario@cs.man.ac.uk
 /~      ~\    The University              uucp:      mcsun!ukc!man.cs!mario
(    __    )   Manchester M13 9PL          JANET:         mario@uk.ac.man.cs
 `-':  :`-'    U.K.                        Tel: +44-61-275 6146  (FAX: 6236)
____;  ;_____________the mushroom project___________________________________