[Types-sig] Compile-time or runtime checks?

Greg Stein gstein@lyra.org
Wed, 15 Dec 1999 03:51:11 -0800 (PST)


On Tue, 14 Dec 1999, Paul Prescod wrote:
>...
> I'm trying hard to separate the axes of: "I have some type declarations"
> and "I want a static type checker to gurantee that this code is totally
> type safe." This should be legal:

Agreed. Good separation.

> StringType
> def foo():
> 	a=eval( sys.argv[1] )
> 	return a
> 
> That means I want a runtime check. This should be illegal:
> 
> type-safe
> StringType
> def foo():
> 	a=eval( sys.argv[1] )
> 	return a
> 
> Here I've specifically asked for a compile time check and my code is not
> up to snuff.

Add the following in:

type-safe
StringType
def foo():
  a = eval(sys.argv[1]) ! StringType
  return a

Now you have a type-safe function. :-)  Of course, it might raise an
exception, but your types are clean. (heck, the eval could raise an
exception... type safety does not imply "no exceptions")

(yah yah.. I recognize the same could be done with an "assert" statement,
 but I think the inferencer would not be as pleased trying to deal with
 that, as with the type-assert operator)


Oh. That just made me think of something. "Exceptions which might be
raised" is technically part of a signature. I say punt that to V2 :-)
[ we could make some accomodation in the FuncObject to record a tuple of
  possible exceptions, and it would always contain (Exception,) in it for
  now... ]

Cheers,
-g

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