[Types-sig] Typesafe

[Paul Prescod]

Let's see if we can figure out this typesafe thing once and for all
because we've half-covered it a dozen times:

> > It is how you *turn on* regular type checking at compile time.
> 
> Isn't it also enabled by the presence of declarations?

No, I don't think so.

Case 1:

decl getprop as def( foo: URL, prop: String ) -> String
def getprop( foo, prop ):
  return WebDAVGetPropertyThatIKnowIsAString( foo, prop )

I declared the return type for *clients* of this function, not because I
want to check the body of the function itself. The function itself is
trivial. I know it works. I'm a Python programmer and I don't aways need
a compiler holding my hand as if I were an infant.

That isn't strictly speaking typesafe and a Java programmer would do
something like this:

decl getprop as def( foo: URL, prop: String ) -> String
def getprop( foo, prop ):
  return WebDAVGetPropertyThatIKnowIsAString( foo, prop ) isa String

But that's why I don't use Java. Sometimes I just know what a thing is
and I don't feel like telling the compiler. This is going to especially
be the case when I am calling reams and reams of non-type-safe code that
I happen to trust (e.g. Zope!). I don't want to cast every method call.

But then other times I write hundreds of lines of mission critical code
and I want a little help to guarantee that it does what I think:

typesafe def getprop( foo, prop ):
  10,000 lines
  return WebDAVGetPropertyThatIKnowIsAString( foo, prop ) isa String



Case 2:

decl getprop as def( foo: URL, prop: String ) -> String
def getprop( foo, prop ):
  j = someUntypeSafeFunction() + someOtherUntypesafeFunction()
  return "abc"

Does this code violate any of its declarations? No. Is it typesafe? No.
Is it legal? Yes. Python allows you to add random variables if you think
you know what you are doing.

But this is *not* legal:

typesafe def getprop( foo, prop ):
  j = someFunction() + someOtherFunction()
  return "abc"

Now I've asked the compiler to pretend I am an incompetent child (or a
Java programmer <wink>) and tell me when I have done anything dangerous.

---

Type declarations are you helping the compiler because it is too stupid
to figure out what is going on. typesafe declarations are about the
compile helping you because you might not be smart enough to figure out
what's going on.

Despite my tounge in cheek jabs at Java programmers, I think that
typesafety would be the norm in my own code, but it should not be the
default because Python is not Java. 

And one virtue of "typesafe" is that as a side effect it guarantees that
you stick to a Python subset that is directly compilable into (fairly)
idiomatic (and thus efficient) Java or C++. If you leave off the
typesafe then there may be some implicit runtime type checks going on
that will sap your speed.

 Paul Prescod