Optional Static Typing

[Michael Hobbs]

I've just started learning about Haskell. I suggest looking at this for an
example.

A good intro: http://www.haskell.org/tutorial

I've always found that with Haskell, if I can get my program to
compile without error, it usually runs flawlessly. (Except for the
occasional off-by-one error. I don't know if that's due to the
fact that Haskell enforces pure functional programming, or if it's
due to Haskell's strict static typing, or the combination of the
two. But if anyone ever demanded that I wrote code that absolutely
positively has to work, no matter the cost, I would probably choose
Haskell.

Tying Haskell back to Python, if static type checking ever is
grafted on to Python, I would propose that it uses type inference,
a la Haskell or O'Caml, and raise an Error only when it detects a
truly unmistakable type error. This may be easier said than done,
however, given Python's dynamic nature. For example, a class's
method may be re-bound to any other function at runtime, which would
wreak havoc on any static type checker.

- Mike

 

[Donn Cave]

...which is exactly the point of the famous post by Robert ("Uncle Bob")
Martin on another artima blog,
http://www.artima.com/weblogs/viewpost.jsp?thread=4639 .

Wait a minute, isn't he same fellow whose precious
dependency inversion principle shows us the way to
support fully modular programming? What would he
say about unit testing to catch up with changes in
dependent modules, do you think? Do we have a
combinatorial explosion potential here?

Donn Cave, (e-mail address removed)

 

[Alex Martelli]

Wait a minute, isn't he same fellow whose precious
dependency inversion principle shows us the way to
support fully modular programming? What would he

Yep, just the same guy (also responsible for Dynamic Visitor, et al).

say about unit testing to catch up with changes in
dependent modules, do you think? Do we have a
combinatorial explosion potential here?

I can't do justice to all he has to say about these issues, and many
others related to Agile development methods -- you should really get his
book (he's written several, but, in my opinion, it's his masterpiece --
<http://www.amazon.com/exec/obidos/tg/detail/-/0135974445/002-8057003-10
74462?v=glance>), or, failing that, at least read his essays at
<http://www.objectmentor.com/resources/listArticles?key=author&author=Ro
bert%20C.%20Martin> (I would skip all of the silly 'craftsman'
fictionalization he's writing for 'Software Development', but I guess
_some_ people must be into that...).


Alex

 

[Alex Martelli]

Your proposition reminds me very much of Design by Contract, which is
a prominent feature of the Eiffel programming language. Considering
that Python is an interpreted language where type checking would
naturally occur at runtime, I think Design by Contract would be more
appropriate than static typing.

I entirely agree with this opinion.

In a function's contract, not only could it state that its parameter
must be an integer,

I'd like to be able to state something about the *INTERFACE* of the
parameter, to the rigorous exclusion of its *TYPE* (which is an
"implementation detail"). I doubt it's really feasible, but, in Haskell
terms, I'd love for such assertions to be always and necessarily about
_typeclasses_ rather than _types_...

but also that it must be > 50 and be divisible by
7. If a value is passed to the function that violates the contract,
it raises an exception.

In Eiffel, contract checking can be turned on or off based on a
compiler flag or a runtime switch.

I've always liked the (theoretical) idea that assertions (including of
course contracts) could be used as axioms used to optimize generated
code, rather than (necessarily) as a runtime burden. E.g. (and I don't
know of any implementation of this concept, mind you), inferring (e.g.
from such assertions) that x>=0, and that y<0, the compiler could simply
cut away a branch of dead code guarded by "if x<y:" (maybe with a
warning, in this case;-)...


Alex

 

[Scott David Daniels]

I've always found that with Haskell, if I can get my program to
compile without error, it usually runs flawlessly. (Except for the
occasional off-by-one error.

Then you need "Scott and Dave's Programming Language" -- SAD/PL.
By providing separate data types for even and odd numbers, you can
avoid off-by-one errors ;-)

--Tongue-in-cheek-ily-yours,
Scott David Daniels
(e-mail address removed)

 

[Robert Kern]

Will we be able to see it anytime soon?
I'm eagerly waiting for its release.

It's been "about a month away" for at least 4 months now. I don't know
what the holdup has been. I know that Michael has graduated and so he's
probably been busy with a new job.

--
Robert Kern
(e-mail address removed)

"In the fields of hell where the grass grows high
Are the graves of dreams allowed to die."
-- Richard Harter

 

[Ville Vainio]

Alex> I've always liked the (theoretical) idea that assertions
Alex> (including of course contracts) could be used as axioms used
Alex> to optimize generated code, rather than (necessarily) as a
Alex> runtime burden. E.g. (and I don't know of any
Alex> implementation of this concept, mind you), inferring (e.g.
Alex> from such assertions) that x>=0, and that y<0, the compiler
Alex> could simply cut away a branch of dead code guarded by "if
Alex> x<y:" (maybe with a warning, in this case;-)...

I realize that your example is theoretical, but efficiency impact of
such optimizations would be dwarfed (speedwise) by optimization on
type, so that "if x < y" yields native object code for integer
comparison. Also, to get real benefits the functions called would need
to be inline-expanded so that the implications of x < y are taken in
account deeper in the call chain; a programmer that does

def f(x,y):
assert x > y
if x < y:
blah(y,x)

needs a slap on the wrists anyway. Doing "if x < y" in blah() would
make sense, but then there would need to be a special version of
blah()...

I could think of one worthwhile example as well:

def foo(l):
assert issorted(l)
if "hi" in l: # in does a bsearch because the list is sorted
blah()

but things like this probably belong to languages like Lisp where the
user gets to expand and mess with the compiler.

 

[Robin Becker]

Scott David Daniels wrote:
.....

Then you need "Scott and Dave's Programming Language" -- SAD/PL.
By providing separate data types for even and odd numbers, you can
avoid off-by-one errors ;-)

mmmhhh off by two-licious

 

[Ryan Paul]

Adding Optional Static Typing to Python looks like a quite complex
thing, but useful too:
http://www.artima.com/weblogs/viewpost.jsp?thread=85551

I wrote a blog post this morning in which I briefly argue using DbC and
predicate based argument constraints instead of static typing. Take a look
if you are interested. It also contains a link to a wiki page where I have
been producing a more refined specification complete with good examples:

http://www.cixar.com/segphault/pytype.html

I would appreciate some feedback, I want to know what other python
programmers think about DbC and arg constraints.

-- SegPhault

 

[Ville Vainio]

Ryan> I wrote a blog post this morning in which I briefly argue
Ryan> using DbC and predicate based argument constraints instead
Ryan> of static typing. Take a look

I took a look. The first impression is that there is too much stuff to
be added to the language, for a relatively unproven methodology (DbC).

Yes, observe the herecy in my argument; I'm indeed referring to DbC as
being an unproven way to write software. Eiffel never really made it,
and explicit preconditions/postconditions haven't really appeared in
other languages either. I'm not sure I'd like to see Python (which is
not an academic language) take the risk of bloating the language
definition with it. Let Ruby, or Boo, or whatever have a go before
Python. And yes, I've read my OOSC, and my code has its share of
asserts.

Type declarations, on the other hand, are as mainstream as one can
get. Being optional, they would not brutally murder the spirit of all
the good that is Python, contrary to the doom and gloom people have
been painting here and elsewhere. The implementation of CPython would
become more complex, but I trust the people that are implementing it
enough to not be overly concerned.

 

[Jacek Generowicz]

I've always liked the (theoretical) idea that assertions (including of
course contracts) could be used as axioms used to optimize generated
code, rather than (necessarily) as a runtime burden. E.g. (and I don't
know of any implementation of this concept, mind you), inferring (e.g.
from such assertions) that x>=0, and that y<0, the compiler could simply
cut away a branch of dead code guarded by "if x<y:" (maybe with a
warning, in this case;-)...

A few months ago, a troll challenged the denizens of comp.lang.lisp to
write a Lisp implementation of some some code which he posted in C++,
which would be competitive in terms of speed with his C++
version. The c.l.lers duly obliged, and, IIRC, it so happened that the
improvement that made the Lisp version overtake the C++ one was the
declaration of some variable to be of type "floating point number in
the range 0 to two Pi".

Of course, in CL type declarations are not contracts, but promises to
the compiler ... but it's still an examlpe of a situation where more
specific type information allowed the compiler to produce more
efficient code, in practice.