[Types-sig] Optionality and performance

[Greg Stein]

I'm not sure what point your're making here -- it seems to be different
than my issue.

On Sun, 19 Dec 1999, Paul Prescod wrote:
> Greg Stein wrote:
> > > Optionality of type checking is not about it being enabled or disabled.
> > > Even when it is enabled, type checking any particular method must be
> > > optional. This whole discussion should presume "enabled". But
> > > optionality is still important.
> > 
> > I'm assuming that we type-check a module at a time -- that we don't have
> > the kind of fine-grained checking you're assuming. If a person doesn't
> > want find-grained checking, then they just shouldn't add type annotations
> > there.
> 
> Here's the issue I tried to address in RFC 1.0 under the term "safety
> declarations".
> 
> def foo() -> String:
> 	# 10,000 lines of code
> 	return str( abc )
> 
> This function is guaranteed to meet its type signature if it completes,

I agree. Although, I would state that it is only guaranteed if the
type-checking is enabled when you compile the *module*. Specifically: the
presence of the return type means that the type-checker will verify the
return value as matching that type. This process is enabled when the
type-checker is enabled; the checking is *not* done if the type-checking
is not enabled.

You enable/disable compile-time, static type checking on a *module* basis,
when you compile the module. Given two declarations:

  def foo():
    ...
  def bar() -> String:
    ...

The foo() function will always pass the type-checker because it assumes
"-> any" as the return value, which is satisfied by whatever foo() might
return.

The bar() function passes IFF it only returns strings (and doesn't fall
off the end of the function, which implies a "return None").

> but it is not necessarily type-safe in the Java sense. Anywhere within
> it, an integer could be added to a string or a ".foo" invoked on a
> float. 

Sure...

> For ERR it is important to be able to say that this function is
> type-safe if there is some important reason that it really should not
> fail. The type system can't guarantee termination but it can at least
> ensure that TypeError and AttributeError will never be triggered by this
> code. For a big part of our target audience, this assertion is the
> reason for the exercise.

Absolutely.

> For OPT it is important to be able to say: "I need this code to run like
> a bat out of hell and I believe that there are no string lookups or
> runtime type checks required. Please verify that for me." So we need
> 
> "decl type-safe foo"
> 
> or something like that.

I'm saying we don't declare a need for type-safety. I'm saying that
type-safety checking is preconditioned on two things:

  1) type-checking is enabled when the module is compiled
  2) type annotations are present

So: when the compilation process is occurring and type-checking is
enabled, then it will verify as many types as possible.

Now, maybe it is desirable to have a second switch that says "foo.bar()
should fail if you cannot ensure foo has a bar method taking no
parameters." I'm presuming that without this switch, the type-checker
could assume that anything of type "any" would have any method that is
used.

Just to clarify since I think we missed each other:

1) the process of type-checking is an aspect of the compilation process
   and is enabled/disabled at the module level
2) a basic level of type checking states "check whatever you know about"
3) a stricter level of type checking states "all types must be done and
   verified correct."

Cheers,
-g

-- 
Greg Stein, http://www.lyra.org/