Python from Wise Guy's Viewpoint

[prunesquallor]

You *did* notice that it is C++, which hasn't type inference (and
a lousy typesystem? So what Brian is saying that this is so easy
he can even to it with hands tied on his back and standing on his
head.

I did in fact notice that. It's *supposed* to be easy. It's
*supposed* to be something simple and useful.

As I mentioned earlier in this thread, the two things I object to in a
static type system are these:

1) The rejection of code I know to be useful, yet the system is
unable to prove correct.

2) The requirement that I decorate my program with type
information to give the type checker hints to enable it
to check things that are, to me, obviously correct.

These are personal preferences, but they are shared by many of my
fellow lisp hackers. To my knowledge, not one of my fellow lisp
hackers would mind a static type checker that noticed code fragments
that could be proven to never produce anything but an error provided
that said type checker never need hints and is never wrong. Many lisp
systems already have a weak form of this: try compiling a program that
invokes CAR on 2 arguments or attempts to use a literal string as a
function.

Being unable to prove code correct is the same thing as being able to
prove it incorrect. This makes three classes of code:

1) provably type safe for all inputs
2) provably erroneous for all inputs
3) neither of the above

Both dynamic and static type systems behave the same way for classes 1
and 2 except that static systems reject the code in section 2 upon
compilation while dynamic systems reject it upon execution. It is
section 3 that is under debate.

We can categorize class 3 by partitioning the inputs. Some inputs
can be shown to always produce a type error, some can be shown to
*never* produce a type error, and some are undecidable. All the class
3 programs contain inputs in at least two of these partitions.

The question remains over what to do with class 3 programs. Of course
what we do may depend on how often a class 3 program is encountered,
what the risk might be of running one, and possibly the compile time
cost of detecting one.

Those of us that are suspicious of static typing believe that there
are a large enough number of class 3 programs that they will be
regularly or frequently encountered. We believe that a large number
of these class 3 programs will have inputs that cannot be decided by a
static type checker but are nonetheless `obviously' correct. (By
obvious I mean fairly apparent with perhaps a little thought, but
certainly nothing so convoluted as to require serious reasoning.)

Static type check aficionados seem to believe that the number of class
3 programs is vanishingly small and they are encountered rarely. They
appear to believe that any program that is `obviously' correct can be
shown to be correct by a static type checking system. Conversely,
they seem to believe that programs that a static type checker find
undecidable will be extraordinarily convoluted and contrived, or
simply useless curiosities.

Some people in the static type check camp are making blanket
statements like:

Matthias Blume
Typical "Gödel" statements tend to be pretty contrived.

...the sane programs that are taken away are in most cases at
least questionable (they will be mostly of the sort: There is a
type error in some execution branch, but this branch will never be
reached)

... given a good type system, there are few if any practial
programs that would be wrongly rejected.

Matthias Blume
`...humans do not write such programs, at least not
intentionally...'


No one has offered any empirical evidence one way or another, but the
static type people have said `if class 3 programs are so ubiquitous,
then it should be easy to demonstrate one'. I'll buy that. Some of
the people in here have offered programs that take user input as an
example. No sane person claims to read the future, so any statically
typed check program would have to perform a runtime check.

But this is shooting fish in a barrel, so I'll give you a pass on it.

I (and Don Geddis) happen to believe that there are a huge number of
perfectly normal, boring, pedestrian programs that will stymie a
static type checker. I've been offering a few that I hope are small
enough to illustrate the problem and not so contrived as to fall into
the `pointless' class.

The first program I wrote (a CPS lookup routine) generally confuses
wimp-ass static type checking like in Java.

Stephan Bevan showed that SML/NJ had no problem showing it was type
safe without giving a single type declaration. I find this to be
very cool.

I offered my `black hole' program and got these responses:

Remi Vanicat <[email protected]>
`I don't see how this function can be useful...'

Jesse Tov <[email protected]>
`we don't need functions with those types.'

Dirk Thierbach <[email protected]>
`recursive types are very often a result of a real typing error.'

"Marshall Spight" <[email protected]>
`I don't believe the feature this function illustrates could be
useful.'

Will this the response for any program that does, in fact, fool a
number of static type checkers?

Marshall Spight wrote:
`I'm trying to see if anyone can come up with a program
that is small, useful, and not provably typesafe.'

to which Joachim Durchholz <[email protected]> replied:
``Matthias' and my position is that such a program doesn't exist
(and cannot even exist)''


This appears to be getting very close to arguing that static type
checkers never reject useful programs because, by definition, a
program rejected by a static type checker is useless.

Another one was a CPS routine that traverses two trees in a lazy
manner and determins if they have the same fringe. The point was not
to find out if this could be done in SML or Haskell. I know it can.
The point was to find out if the static type checker could determine
the type safety of the program.

There is a deliberate reason I did not create a `lazy cons'
abstraction. I wanted to see if the type checker, with no help
whatsover, could determine that the type of the lambda abstractions
that are *implementing* the lazy consing.

Re-writing the program in C++ with huge amounts of type decorations
and eliminating the lambdas by introducing parameterized classes does
not demonstrate the power of static type checking.

Re-writing the program in a lazy language also does nothing to
demonstrate the power of static type checking.

 

[Ed Avis]

Let's take as our ideal what a dynamic type system (say, a program in
Lisp) would report upon executing the program. The question is, can
your type inference system make exactly the same conclusions at
compile time, and predict all (and only!) the type errors that the
dynamic type system would report at run time?

The answer is no.

Indeed not. But if you were using a statically typed language you'd
write the program in a slightly different style, one that does let
type errors be found at compile time. For example instead of a
function that takes 'either an integer, or a string' with that checked
at run time, you'd have to be more explicit:

data T = TI Integer | TS String

f :: T -> Bool
f (TI i) = ...
f (TS s) = ...

The question is whether having to change your program in this way is
so horribly cramping that it negates the advantages from having errors
found earlier. In my experience I haven't found that to be the case.

- Hmm, I wonder if I might make an analogy between type checking and
syntax checking. In the language Tcl almost everything, including
code, is a string, and the 'if' statement is just something that takes
three strings and evaluates the first, followed by either the second
or third. The syntax of these strings is not checked at compile time.
You can write code like

if $cond { puts "hello" ( } else { puts "goodbye" }

and the syntax error in the 'hello' branch won't be found unless you
run a test case setting $cond true.

The question is, can a static syntax checking system make exactly the
same conclusions at compile time, and predict all and only the syntax
errors that Tcl would report at run time?

The answer is no.

Should we then conclude that compile-time syntax checking is not worth
having?

 

[Ed Avis]

As I mentioned earlier in this thread, the two things I object to in a
static type system are these:

1) The rejection of code I know to be useful, yet the system is
unable to prove correct.

This has never happened to me with Haskell, and I don't think it has
ever happened with C. With C++ I have often felt as though the type
system was being picky and getting in the way, but this was usually a
case of me finding it difficult to make my intentions clear to the
compiler - which is also a disadvantage of static typing, of course.
Languages like Haskell and ML don't tend to suffer that problem,
because the type system is a bit more understandable than C++ and will
infer things it's not told explicitly.

2) The requirement that I decorate my program with type
information to give the type checker hints to enable it
to check things that are, to me, obviously correct.

This is why type inference as used in the above-mentioned languages
and many others is so useful. You can still add explicit type
declarations where you want to, either to help find out where you have
made a mistake (analogously to putting in extra assertions to narrow
down the point where something goes wrong at run time) and to act as
documentation (which, unlike comments, is automatically checked by the
compiler to make sure it's up to date).

To my knowledge, not one of my fellow lisp hackers would mind a
static type checker that noticed code fragments that could be proven
to never produce anything but an error provided that said type
checker never need hints and is never wrong.

I believe this is what you get with standard Haskell (though some
language extensions may require explicit type annotations in some
places). Certainly the type checker is never wrong: it never flags a
type error in a correct program, and never gives the all-clear for a
program containing a type error.

But of course, the checker is checking Haskell programs, not Lisp
programs. Nobody is suggesting to use some form of full compile-time
type checking on Common Lisp, nor could such a thing exist.

[later]

This appears to be getting very close to arguing that static type
checkers never reject useful programs because, by definition, a
program rejected by a static type checker is useless.

Absolutely true - in a statically typed language! In Lisp or a
dynamically typed language, obviously not true - except that the
statement doesn't really make any sense for Lisp, because one cannot
write a full static type checker for that language.

 

[Pascal Costanza]

As an example of the kind of "overloading" (or type dispatch, if you want)
you cannot express in dynamically typed lagnuages: in Haskell, you can
naturally define functions which are overloaded on their return type, i.e.
you don't need any value at all at runtime to do the "dispatch". For
example, consider an overloaded function fromString, that produces values of
potentially arbitrary types from strings.

Wrong.

(defmethod from-string-expansion (to-type string)
(if (or (subtypep to-type 'sequence)
(subtypep to-type 'character)
(eq to-type t))
`(coerce ,string ',to-type)
`(coerce (read-from-string ,string) ',to-type)))

(defmacro set-from-string (x string &environment env)
(multiple-value-bind
(bound localp declarations)
(variable-information x env)
(declare (ignore bound localp))
(let ((type (or (cdr (assoc 'type declarations)) t)))
`(setf ,x ,(from-string-expansion type string)))))


Session transcript:


? (let (x)
(declare (integer x))
(set-from-string x "4711")
(print x))

4711

? (let (x)
(declare (string x))
(set-from-string x "0815")
(print x))

"0815"

? (defmethod from-string-expansion ((to-type (eql 'symbol)) string)
`(intern ,string))
#<standard-method from-string-expansion ((eql symbol) t)>

? (let (x)
(declare (symbol x))
(set-from-string x "TEST")
(print x))

test


The macro delegates the decision which conversion function to use to the
generic function FROM-STRING-EXPANSION, but this is all executed at
compile time (as required for a compiled implementation of Common Lisp).

Pascal


P.S.: This is not ANSI Common Lisp, but uses a feature as defined in Guy
Steele's book "Common Lisp, The Language - 2nd Edition" (->
VARIABLE-INFORMATION). The code above works in Macintosh Common Lisp.

 

[Dirk Thierbach]

Dirk Thierbach wrote:

Sidenote: The code above has a bug. Here is the correct version:

(defun f (x)
(if (< x 200)
(* x 2)
(progn
(cerror "Type another number"
"You have typed a wrong number")
(print '>)
(f (read)))))

(Noone spotted this bug before. All transliterations I have seen so far
have silently corrected this bug.

Because all people who did transliterations guessed what the program
does, instead of testing it directly. I don't have a Lisp system here,
so I couldn't try it out.

It is interesting to note that it probably weren't the type systems
that corrected it.)

While doing the transliteration, I actually had quite a few attempts
that didn't work, and all of them had type errors. Once the typing
was right, everything worked. (And I had to put the continuation in,
because, as I said, non-local control transfers don't translate
one-to-one.)

I think you have a restricted view of what "type" means.

Maybe. It sure would help if you'd tell me your view instead of having
me guess For me, a type is a certain class of values, and a static
type is given by a limited language describing such classes. A
dynamic type is a tag that is associated with a value. Arbitrary
classes of values (like "all reals less than 200") are not a type.

Here is the same program written in a "type-friendly" way.

I'm not sure what's "type-friendly" about it. It uses a dynamic check
with a mix of dynamic type checking and value checking, yes. (I guess
"(real * 200)" means "a real number below 200", does it?)

(Again, in standard ANSI Common Lisp. Note that the type is defined
inside of f and not visible to the outside.)

You do not define any type, you do a dynamic check.

(defun f (x)
(check-type x (real * 200))
(* x 2))
[...]
You have used CPS - that's a nice solution. However, you obviously
needed to make the type declaration for f :: Integer -> IO (Integer)

In this case, you're right, but I am not sure if you know the reason
for it (I usually make type annotations for the same reason you
write unit tests, i.e. almost everwhere unless the function is
trivial) So why do I have to make it here? Is the type annotation for
cerror also necessary?

What you actually did is: you have assigned a "broad" type statically,
and then you revert to a manual dynamic check to make the fine-grained
distinction.

If you mean by "broad" type the static integer type, yes. I have to
assign some type. If I don't want to restrict it to integers, I assign
a more general type (like the Number type I used in the other example).

Dynamic type checks either can be dropped because static type
checking makes them unnecessary, or they translate to similar dynamic
checks in the other language.

Since you cannot statically verify that a user-supplied value is less
than 200, this check becomes a dynamic check (what else should it
translate to?)

In both Lisp versions, you have exactly one place where you check the
(single) type.

You have one place where you do the dynamic check, I have one place where
I do the dynamic check. The static type is only there because there
has to be a type. It really doesn't matter which one I use statically.
The static type check does not play any role for the dynamic check.

A static type system cannot provide this kind of granularity.

I am sorry, but this is nonsense (and it isn't really useful either).

This is like saying "I don't write unit tests in Lisp, because I have
a single place inside my program where I can check everything that
can go wrong."

I regard the distinction between dynamic type errors and runtime errors
to be an artificial one, and in fact a red herring. I would rather call
the former type _exceptions_.

Fine with me. I would go further and say that without dynamic
type checking, there are in fact only exceptions.

Both (correct) code snippets I have provided are considerably smaller
than your solution and both are more general. And my second solution
still provides a way to correct a wrong parameter at runtime at no
additional cost. I regard this a feature, not a problem.

I would debate both points, but this is about static typing, not about
comparisons a la "in my language I can write programs that are
two lines shorter than yours."

P.S.: Please always remember the original setting of this thread. The
original original questions was something along the lines of "why on
earth would one not want a static type system?"

The answer to this is of course "You use what you like best. End of
story."

What I wanted to do was to show that the claim "There are things that
are easy to do in a dynamically typed language, but one cannot do them
conveniently in a statically typed language, because they won't
typecheck. Hence, statically typed languages are less expressive" is
wrong in all but very very rare situations. Of course the amount of
convenience with which you can do something varies from language to
language, and with the available libraries, but static typing (if done
properly) is never a show-stopper.

Yes, you can clearly tell from my postings that I prefer dynamic typing
over static typing.

And that's fine with me. What I am a bit allergic to is making
unjustified general claims about static typing (or any other things,
for that matter) that are just not true.

But why on earth should anyone want to prove that their own preferred
_personal_ style is generally superior to all others?

I don't know. As far as I am concerned, this thread was never about
"superiority", and I said so several times.

- Dirk

 

[Pascal Costanza]

- Hmm, I wonder if I might make an analogy between type checking and
syntax checking. In the language Tcl almost everything, including
code, is a string, and the 'if' statement is just something that takes
three strings and evaluates the first, followed by either the second
or third. The syntax of these strings is not checked at compile time.
You can write code like

if $cond { puts "hello" ( } else { puts "goodbye" }

and the syntax error in the 'hello' branch won't be found unless you
run a test case setting $cond true.

The question is, can a static syntax checking system make exactly the
same conclusions at compile time, and predict all and only the syntax
errors that Tcl would report at run time?

The answer is no.

Should we then conclude that compile-time syntax checking is not worth
having?

No. Syntax errors make the program fail, regardless whether this is
checked at compile-time or at runtime.

A type "error" detected at compile-time doesn't imply that the program
will fail.


Pascal

 

[Joachim Durchholz]

As I mentioned earlier in this thread, the two things I object to in a
static type system are these:

1) The rejection of code I know to be useful, yet the system is
unable to prove correct.

Er... for static type systems, it's just "type-correct". General
correctness isn't very well-defined and not what current main-stream
type systems are designed for anyway.

2) The requirement that I decorate my program with type
information to give the type checker hints to enable it
to check things that are, to me, obviously correct.

I'd agree with these points, and restate that both are addressed by
Hindley-Milner type systems.

1) Most useful code is type-correct. The code that isn't uses quite
advanced types, but these are borderline cases like "black-hole" above.
Besides, I don't know of any borderline case that cannot be written
using different techniques.

2) Decorating programs with type annotations is an absolute exception.
The only case where types are declared are those where you define a new
type (i.e. record types).

These are personal preferences, but they are shared by many of my
fellow lisp hackers. To my knowledge, not one of my fellow lisp
hackers would mind a static type checker that noticed code fragments
that could be proven to never produce anything but an error provided
that said type checker never need hints and is never wrong.

A HM checker flags some usages as "wrong" that would work in Lisp -
black-hole is an example.
I'm not sure that such usage serves a good purpose.

> Many lisp
systems already have a weak form of this: try compiling a program that
invokes CAR on 2 arguments or attempts to use a literal string as a
function.

That's exceedingly weak indeed.
Distinguishing square from nonsquare matrices goes a bit beyond the
standard usage of HM type systems, but it is possible.

Being unable to prove code correct is the same thing as being able to
prove it incorrect.

This true for HM typing but not true for inference systems in general.
But probably you wanted to say something else anyway.

> This makes three classes of code:

1) provably type safe for all inputs
2) provably erroneous for all inputs
3) neither of the above
>
Both dynamic and static type systems behave the same way for classes 1
and 2 except that static systems reject the code in section 2 upon
compilation while dynamic systems reject it upon execution. It is
section 3 that is under debate.

Agreed.
Programs in class 2 are rarely encountered and quickly fixed, so I'm not
sure that this category is very interesting.

We can categorize class 3 by partitioning the inputs. Some inputs
can be shown to always produce a type error, some can be shown to
*never* produce a type error, and some are undecidable. All the class
3 programs contain inputs in at least two of these partitions.

The question remains over what to do with class 3 programs. Of course
what we do may depend on how often a class 3 program is encountered,
what the risk might be of running one, and possibly the compile time
cost of detecting one.

There's also the question how to decide whether a program is in class 1
or class 3.

Those of us that are suspicious of static typing believe that there
are a large enough number of class 3 programs that they will be
regularly or frequently encountered. We believe that a large number
of these class 3 programs will have inputs that cannot be decided by a
static type checker but are nonetheless `obviously' correct.

This belief is ill-founded. Just take a dynamically-typed program and
annotate every parameter with all the types that you expect it to take
on. Exclude possibilities if you hit a contradiction. Get suspicious if,
for some parameter, there is /no/ type left
You'll find that most programs will type readily.
(HM typing indeed starts with allowing all types for all names, then
excluding all types that lead to a contradiction somewhere. The actual
wording of the algorithm is somewhat different, but that's the gist of it.)

> (By
obvious I mean fairly apparent with perhaps a little thought, but
certainly nothing so convoluted as to require serious reasoning.)

Static type check aficionados seem to believe that the number of class
3 programs is vanishingly small and they are encountered rarely. They
appear to believe that any program that is `obviously' correct can be
shown to be correct by a static type checking system. Conversely,
they seem to believe that programs that a static type checker find
undecidable will be extraordinarily convoluted and contrived, or
simply useless curiosities.

Some people in the static type check camp are making blanket
statements like:

Matthias Blume
Typical "Gödel" statements tend to be pretty contrived.

...the sane programs that are taken away are in most cases at
least questionable (they will be mostly of the sort: There is a
type error in some execution branch, but this branch will never be
reached)

... given a good type system, there are few if any practial
programs that would be wrongly rejected.

Matthias Blume
`...humans do not write such programs, at least not
intentionally...'

No one has offered any empirical evidence one way or another, but the
static type people have said `if class 3 programs are so ubiquitous,
then it should be easy to demonstrate one'. I'll buy that. Some of
the people in here have offered programs that take user input as an
example. No sane person claims to read the future, so any statically
typed check program would have to perform a runtime check.

But this is shooting fish in a barrel, so I'll give you a pass on it.

I (and Don Geddis) happen to believe that there are a huge number of
perfectly normal, boring, pedestrian programs that will stymie a
static type checker. I've been offering a few that I hope are small
enough to illustrate the problem and not so contrived as to fall into
the `pointless' class.

The first program I wrote (a CPS lookup routine) generally confuses
wimp-ass static type checking like in Java.

Stephan Bevan showed that SML/NJ had no problem showing it was type
safe without giving a single type declaration. I find this to be
very cool.

I offered my `black hole' program and got these responses:

Remi Vanicat <[email protected]>
`I don't see how this function can be useful...'

Jesse Tov <[email protected]>
`we don't need functions with those types.'

Dirk Thierbach <[email protected]>
`recursive types are very often a result of a real typing error.'

"Marshall Spight" <[email protected]>
`I don't believe the feature this function illustrates could be
useful.'

Will this the response for any program that does, in fact, fool a
number of static type checkers?

Marshall Spight wrote:
`I'm trying to see if anyone can come up with a program
that is small, useful, and not provably typesafe.'

to which Joachim Durchholz <[email protected]> replied:
``Matthias' and my position is that such a program doesn't exist
(and cannot even exist)''

Sorry, you're mixing up topics here - that was about correctness in
general, not about type correctness (which is a subset of general
correctness for the vast majority of type systems).

This appears to be getting very close to arguing that static type
checkers never reject useful programs because, by definition, a
program rejected by a static type checker is useless.

That's a misunderstanding, partly due to conflation of correctness and
type correctness, partly because people using a good static type checker
don't feel constrained by that type checking because "you just don't do
that" (similarly to "you just don't do some special things in Lisp",
like abusing MOP mechanisms etc.)

Regards,
Jo

 

[Joachim Durchholz]

You're completely wrong, which can be easily demonstrated.

The fact that it terminates isn't the interesting part. Any inference
procedure can also "always terminate" simply by having a timeout, and reporting
"no proof" if it can't find one in time.

Now you are completely wrong.
Of course you can make any type checker terminate by such draconian
measures, but such a type system would be near-useless: code may
suddenly become incorrect if compiled on a smaller machine.

There are better ways of doing this, like cutting down on the size of
some intermediate result during type checking (such as C++, where
template nesting depth or something similar is cut off at a relatively
small, fixed number IIRC).
Standard type systems don't have, need or want such cut-offs though

So what's interesting is whether the conclusions are correct.

Let's take as our ideal what a dynamic type system (say, a program in Lisp)
would report upon executing the program. The question is, can your type
inference system make exactly the same conclusions at compile time, and predict
all (and only!) the type errors that the dynamic type system would report at
run time?

The answer is no.

Not precisely.
The next question, however, is whether the programs where the answers
differ are interesting.
There's also a narrow and a broad sense here: obviously, it's not
possible to type check all Lisp idioms, but are we allowed to present
alternative idioms that do type check and serve the same purpose?

[Snipping the parts that are getting ad hominem-ish :-( ]

Regards,
Jo

 

[Pascal Costanza]

Maybe. It sure would help if you'd tell me your view instead of having
me guess For me, a type is a certain class of values, and a static
type is given by a limited language describing such classes. A
dynamic type is a tag that is associated with a value. Arbitrary
classes of values (like "all reals less than 200") are not a type.

What are "non-arbitrary classes of values"?

According to your criteria, (real * 200) is
- a certain class of values
- given in a limited language describing that class

I would be interesting to see a convincing definition of the term "type"
that precludes (real * 200), and similar type specifications.

Most of your other comments depend on this, so I don't comment on them
in detail.

(Maybe it helps to explain that CHECK-TYPE doesn't check a value per se.
(check-type 5 (real * 200)) doesn't work. CHECK-TYPE checks a property
of the variable it is being passed.)

The answer to this is of course "You use what you like best. End of
story."

Fine. (Really.)

What I wanted to do was to show that the claim "There are things that
are easy to do in a dynamically typed language, but one cannot do them
conveniently in a statically typed language, because they won't
typecheck. Hence, statically typed languages are less expressive" is
wrong in all but very very rare situations. Of course the amount of
convenience with which you can do something varies from language to
language, and with the available libraries, but static typing (if done
properly) is never a show-stopper.

"very rare situations"
"never a show-stopper"

How do you know?

If you are only talking about your personal experiences, that's fine,
but you should say so.

And that's fine with me. What I am a bit allergic to is making
unjustified general claims about static typing (or any other things,
for that matter) that are just not true.

The only claim I make is that static type systems need to reject
well-behaved programs. That's an objective truth.

This implies that there is a trade-off involved. That's also an
objective truth.

You choose to downplay the importance of dynamic type checking. All I
hear is that you (and many others) say that the disadvantages of static
typing are negligible. However, I haven't found any convincing arguments
for that claim. This claim is simply repeated again and again and again,
ad infinitum. But how do you actually _justify_ that claim?

"It doesn't matter in practice." is not a valid response! Why do think
it doesn't matter in practice? "That's my personal experience." is not a
valid response either. The claim suggests to be valid for a much broader
scale than just your personal experience. Why do you think your personal
experience translates well (or should translate well) to other people?

If it's a personal, subjective choice, that's fine with me. Great! Go
on, use what helps you most.

But I am interested in the question why you (or others) think that
almost all software should be developed like that. This is a very strong
claim, and definitely deserves more justification than "well, I guess
that's better".

I have chosen to illustrate examples in which a dynamic approach might
be considerably better. I am decidedly not trying to downplay static
typing. It can be a rational choice to use a statically typed language
in specific cases. But the claim that static typing is almost always the
better choice is irrational if it is not based on empirical evidence.

Again, to make this absolutely clear, it is my personal experience that
dynamic type checking is in many situations superior to static type
checking. But I don't ask anyone to unconditionally use dynamically
typed languages.


Pascal

 

[prunesquallor]

This true for HM typing but not true for inference systems in
general. But probably you wanted to say something else anyway.

Um, yeah. I did:

Being unable to prove code correct is *not* the same thing as being
able to prove it incorrect.

 

[prunesquallor]

There's also a narrow and a broad sense here: obviously, it's not
possible to type check all Lisp idioms, but are we allowed to present
alternative idioms that do type check and serve the same purpose?

I don't have a problem with this, but I don't want to split hairs on
what constitutes an `idiom' vs. what constitutes a complete rewrite.

Presumably, an alternative idiom would involve only *local* changes,
not global ones, and could be performed incrementally, i.e., each
use of an idiom could be independently replaced and thus reduce the
the the type checking errors.

If a change involves pervasive edits, say, for instance, editing all
callers of some function to pass an extra argument, or wrapping a
conditional branch around all uses of an object, that would not be
an alternative idiom.

 

[Pascal Costanza]

The next question, however, is whether the programs where the answers
differ are interesting.
There's also a narrow and a broad sense here: obviously, it's not
possible to type check all Lisp idioms, but are we allowed to present
alternative idioms that do type check and serve the same purpose?

No, and that's exactly the point. "We" can write completely idiomatic
and well-behaved Lisp code that works, can be understood and maintained
by other Lispers, and provides various useful additional behavior at
runtime.

Why should we rewrite it just to make a static type checker happy?
That's redundant work with no obvious advantages.

Why should we, on the other hand, accept statically type-checked code
that does less than our straightforward solutions?

We could _additionally_, if we wanted to, write our code in a style that
is acceptable by a static type checker whithout switching the language.
We could add a full-blown static type checker to our language and ask
for a different coding style for those parts of the code that would use
it. See Qi and ACL2 for two real-world examples.

This is the gist of unrestricted expressive power: we objectively have
more options! A language that forces your code to adhere to a static
type system has less options!

You may probably not care about the loss of options. You might even
think it's an advantage to have less options. But you objectively have
less options to write well-behaved code!


Pascal

 

[Joachim Durchholz]

I don't have a problem with this, but I don't want to split hairs on
what constitutes an `idiom' vs. what constitutes a complete rewrite.

When it comes to comparing whether static types are "getting in the
way", even a complete rewrite would be OK according to my book.
Sticking to the original code will, of course, make a more compelling
case - not because that is better, but because it's better understood.

If a change involves pervasive edits, say, for instance, editing all
callers of some function to pass an extra argument, or wrapping a
conditional branch around all uses of an object, that would not be
an alternative idiom.

If you mean that Lisp has a point if it can process an arbitrary number
of parameters in one line of code, while a non-Lisp would need an extra
handler for each parameter: then I agree.
Though that isn't usually needed for currying languages. (I know of a
single instance in the standard Haskell libraries where it's needed -
and in that case, it's about taking apart tuples of various arities, not
about taking apart parameter lists which is usually a snap.)

Regards,
Jo

 

[Tomasz Zielonka]

Brian McNamara! napisa³:

(e-mail address removed) once said:

Finally, an example that I don't think you can type in Haskell.
You score a point for that.

If we have a static type system which admits infinite types, then we
can assign black-hole a type. So it's still typeable, just not in any
common language I can name offhand.

You are making things a bit too complicated. I think you can write
blackHole in Haskell:

blackHole :: a
blackHole = error "black-hole"

*BH> :t blackHole 1 2 3 'a' "ho" (blackHole, 1.2)
blackHole 1 2 3 'a' "ho" (blackHole, 1.2) :: forall t. t

*BH> blackHole 1 2 3 'a' "ho" (blackHole, 1.2)
*** Exception: black-hole

*BH> let _ = blackHole 1 2 3 'a' "ho" (blackHole, 1.2) in "abcdef"
"abcdef"

Best regards,
Tom

 

[Dirk Thierbach]

You're completely wrong, which can be easily demonstrated.

Unfortunately, I can *prove* that the HM-type inference always terminates,
without any timeout, by induction on the length of the expression.

The fact that it terminates isn't the interesting part. Any
inference procedure can also "always terminate" simply by having a
timeout, and reporting "no proof" if it can't find one in time.

Yes, you can do that. But it's not done during HM-type inference.

Let's take as our ideal what a dynamic type system (say, a program
in Lisp) would report upon executing the program. The question is,
can your type inference system make exactly the same conclusions at
compile time, and predict all (and only!) the type errors that the
dynamic type system would report at run time?

The answer is no.

Right. It cannot, because that question is not decidable.

That's one obvious case, so even you know that your claim of a "provable
mismatch" is incorrect.

It's still a provable mismatch. Only that part of the code never gets
executed, so you don't have a dynamic type error. I would consider a
program which has a branch that contains an error, but fortunately
never executes that branch pretty bogus. I don't see any advantage
in admitting such a program. It's a bad program, and you should either
correct the error in the dead branch, or remove the dead branch
completely if it isn't going to be executed anyway.

There are programs that will never have run-time
errors, but your static type inference will claim a type error.

Yes. But these programs will have problems, even without a run-time error.
Rewrite them to increase the quality of your software.

For example:
(defun foo (x)
(check-type x (integer 0 10))
(+ 1 x) )
(defun fib (n)
(check-type n (integer 0 *))
(if (< n 2)
1
(+ (fib (- n 1)) (fib (- n 2))) ))
(print (foo (fib 5)))

This program prints "9", and causes no run-time type errors. Will
it be successfully type-checked at compile time by a static system?
Almost certainly the answer is no.

It will be successfully type checked, because the static type system
does not allow you to express assumptions about value ranges of types.
These things have to be checked dynamically, as in your program. So the
type system "doesn't get in the way": It admits the program.

Unfortunately, the only way to figure this out is to actually
compute the fifth Fibonacci number, which surely no static type
inference system is going to do.

Yes. That's why you cannot express such restrictions statically.

Do you now accept that your static type inference systems do NOT partition
all programs into "either a provable [type] mismatch, or a provable [type]
non-mismatch"?

No. But you probably don't understand what I mean with that. A provable
type mismatch means that the program contains a location where it can
be statically verified that executing the location will cause trouble.
It cannot statically check that this location will be indeed executed,
so it might (wrongly) reject the program. But this rejection is acceptable,
because the program is bogus. On the other hand, if there is no static
type mismatch, that doesn't mean that the program will not crash because
of runtime errors (division by zero, or dynamically checked restrictions).

Finally, to get back to the point of the dynamic typing fans:
realizing that type inference is not perfect, we're annoyed to be
restricted to writing only programs that can be successfully type
checked at compile time.

You may not believe it, but I perfectly understand that The
problem is that this is just not true (with a good static type
system): It is not a real restriction. If your program is a good
program, it will type check. If it doesn't type check, then there is
something wrong with it.

I am annoyed in the very same way if I have to write programs in a
language with a bad type system (say, C++). I cannot express myself as
abstractly as I would want to, I have to write down lots of
unnecessary type annotions, and I have to invent tricks to please the
type checker and let it allow me do what I want to do. Really
horrible.

Again, try thinking of the static type systems as an automatic testing
tool. Saying that you want to write programs that will be rejected by
the static typing is like saying that you want to write programs that
will be rejected by your unit tests. It just doesn't make any sense;
the unit tests are there to guarantee that you write good quality
software, so why would you want to ignore them? The only case when you
want to do that is if they are bad tests; when they point to problems
that are not really there. But with a good static type system, that
doesn't happen.

- Dirk

 

[Fergus Henderson]

Have you made sure that this is not a circular argument?
Yes.

Does "consistent design" mean "acceptable by a type checker" in your book?

No.

 

[Dirk Thierbach]

Dirk Thierbach <[email protected]> writes:

As I mentioned earlier in this thread, the two things I object to in a
static type system are these:

1) The rejection of code I know to be useful, yet the system is
unable to prove correct.

2) The requirement that I decorate my program with type
information to give the type checker hints to enable it
to check things that are, to me, obviously correct.

Yes. I have also said it earlier, but (1) is nearly never going to
happen (if you substitute "correct" with "type correct", and for a
suitable definition of useful), and you don't have to do (2) if there
is type inference.

Being unable to prove code correct is the same thing as being able to
prove it incorrect. This makes three classes of code:

1) provably type safe for all inputs
2) provably erroneous for all inputs
3) neither of the above

Both dynamic and static type systems behave the same way for classes 1
and 2 except that static systems reject the code in section 2 upon
compilation while dynamic systems reject it upon execution. It is
section 3 that is under debate.

Those of us that are suspicious of static typing believe that there
are a large enough number of class 3 programs that they will be
regularly or frequently encountered.

Yep. The static typers believe (from experience) that there is a very
small number of class 3 programs, and usually all programs you
normally write fall into class 1. They also know that this is not true
for all static type systems. For languages with a lousy static type
system, there is a large number of class 3 programs, where you have to
cheat to convince the type checker that they are really type safe. The
static typers also believe that with a good static type system, all
useful class 3 programs can be changed just a little bit so they fall
into class 1. In this process, they will become better in almost all
cases (for a suitable definition of "better").

We believe that a large number of these class 3 programs will have
inputs that cannot be decided by a static type checker but are
nonetheless `obviously' correct. (By obvious I mean fairly apparent
with perhaps a little thought, but certainly nothing so convoluted
as to require serious reasoning.)

Why do you believe this? A HM type checker doesn't do anything but
automate this "obvious" reasoning (in a restricted field), and points
out any errors you might have made (after all, humans make errors).

Static type check aficionados seem to believe that the number of class
3 programs is vanishingly small and they are encountered rarely. They
appear to believe that any program that is `obviously' correct can be
shown to be correct by a static type checking system. Conversely,
they seem to believe that programs that a static type checker find
undecidable will be extraordinarily convoluted and contrived, or
simply useless curiosities.
Yes.

No one has offered any empirical evidence one way or another, but the
static type people have said `if class 3 programs are so ubiquitous,
then it should be easy to demonstrate one'. I'll buy that. Some of
the people in here have offered programs that take user input as an
example. No sane person claims to read the future, so any statically
typed check program would have to perform a runtime check.

Yes, and that's what it does. No problem.

I (and Don Geddis) happen to believe that there are a huge number of
perfectly normal, boring, pedestrian programs that will stymie a
static type checker. I've been offering a few that I hope are small
enough to illustrate the problem and not so contrived as to fall into
the `pointless' class.

The first program I wrote (a CPS lookup routine) generally confuses
wimp-ass static type checking like in Java.

Stephan Bevan showed that SML/NJ had no problem showing it was type
safe without giving a single type declaration. I find this to be
very cool.
Good.

I offered my `black hole' program and got these responses: [...]
Will this the response for any program that does, in fact, fool a
number of static type checkers?

No. You have also been shown that it can check statically both in
Haskell and OCaml. (I cannot think of any way to make it pass
in C++ or Java, but that's to be expected.)

This appears to be getting very close to arguing that static type
checkers never reject useful programs because, by definition, a
program rejected by a static type checker is useless.

It may not be useless, but you will definitely need to think about
it. And if it is useful, in nearly all cases you can make a little
change or express it a little differently, and it will check.

Another one was a CPS routine that traverses two trees in a lazy
manner and determins if they have the same fringe. The point was not
to find out if this could be done in SML or Haskell. I know it can.
The point was to find out if the static type checker could determine
the type safety of the program.
There is a deliberate reason I did not create a `lazy cons'
abstraction. I wanted to see if the type checker, with no help
whatsover, could determine that the type of the lambda abstractions
that are *implementing* the lazy consing.

See below for "lazy cons".

Re-writing the program in C++ with huge amounts of type decorations
and eliminating the lambdas by introducing parameterized classes does
not demonstrate the power of static type checking.

No, it doesn't. That was just Brian saying "it's so easy, I'll
do it the hard way and demonstrate that it can even be done with
a lousy static type system as in C++".

Re-writing the program in a lazy language also does nothing to
demonstrate the power of static type checking.

May I suggest that you try it yourself? It might be a good way to
get some experience with OCaml, though for a beginner it might take
some time to get used to the syntax etc. Pure lambda terms are the
same in every functional language, after all.

The only issue is that one should use datatypes for recursive
structures, i.e. one would normally use a 'lazy cons' abstraction
(which would be the natural thing to do anyway). In OCaml, you can get
around this with -rectypes (someone has already demonstrated how to do
lazy lists in this way). In Haskell you would need them, but since
Haskell is already lazy, that's probably not the point.

So yes, for recursive types you need to give the type checker "a
little hint", if you want to put it that way. But that's done on
purpose, because it is the natural way to do it, and it is note done
because it would be impossible to statically check such terms.

So if you are extremely picky, and if you refuse to do the "lazy cons"
initially and consider command line options cheating, that's one of
the programs of class 3 that can be put into class 1 by making a
little change, where this change turns out to make your program better
to understand in the first place. Is this so bad that you want to stay
clear from static typing at any price?

(I bet someone will now comment on that ignoring the "extremely picky"
part :-( .)

- Dirk

 

[Dirk Thierbach]

Dirk Thierbach wrote:

What are "non-arbitrary classes of values"?

Those that can be described by the language available for static types
e.g. in Haskell or OCaml.

According to your criteria, (real * 200) is
- a certain class of values
- given in a limited language describing that class

Yes, but you will have a hard time developing a static type checker
that will work with such a language.

I would be interesting to see a convincing definition of the term "type"
that precludes (real * 200), and similar type specifications.

Look at the definition for type in Haskell or OCaml, for example.

(Maybe it helps to explain that CHECK-TYPE doesn't check a value per se.
(check-type 5 (real * 200)) doesn't work. CHECK-TYPE checks a property
of the variable it is being passed.)

Yes, I know. What does that explain?

"very rare situations"
"never a show-stopper"

How do you know?

If you are only talking about your personal experiences, that's fine,
but you should say so.

Of course I am talking from personal experience, like everyone does.
There is not other way. But in this case, I think my experience is
sufficient to say that.

The only claim I make is that static type systems need to reject
well-behaved programs. That's an objective truth.

This depends on the definition of "well-behaved". The claim I make is
that for a suitable definition of "well-behaved", it is not an
objective truth. And even if you stick to your definition of
"well-behaved", it doesn't really matter in practice.

All I hear is that you (and many others) say that the disadvantages
of static typing are negligible. However, I haven't found any
convincing arguments for that claim.

What kind of arguments would you like to have? I have tried to
show with a few examples that even programs that you think should
be rejected with static typing will be accepted (if you allow for
the fact that they are written in a different language).

What else is there I could possibly do? The simplest way is probably
that you just sit down and give it a try. No amount of talking can
replace personal experience. Get Haskell or OCaml and do a few simple
examples. You will find that they have many things that you won't
like, e.g. no good IDE, no "eval", and (as every language) they
require a slightly different mindset compared to what you're used
to. They might also not have the library functions that you are used
to. But it might give you a good idea what programs are statically
typeable and what are not.

But I am interested in the question why you (or others) think that
almost all software should be developed like that.

I didn't say that. Please do not put up a strawman. In fact, I
explicitely said "you use whatever tool you like best".

I have chosen to illustrate examples in which a dynamic approach might
be considerably better.

And you didn't convince me; all your examples can be statically
typed.

Again, to make this absolutely clear, it is my personal experience
that dynamic type checking is in many situations superior to static
type checking.

That's maybe the important point. HOW DO YOU KNOW IF YOU HAVE NEVER
TRIED IT? (In a language with good static typing, not in a language
with lousy static typing). And obviously you haven't tried it,
otherwise you wouldn't give examples that can be easily statically
typed, or confuse exceptions or dynamic checks with static type checks.
So it cannot come from your personal experience.

But I don't ask anyone to unconditionally use dynamically typed
languages.

But you insist that dynamically typed languages are "better" or
"superior to" statically typed, because you claim you cannot do things
in a statically typed language that you can do in a dynamically typed
one. That's the point where I disagree. I don't ask you to use a
statically typed language, I just want you to give admit that both
are equally good in this respect, or at least you should sit down and
verify that yourself before saying it.

- Dirk

 

[Ed Avis]

No. Syntax errors make the program fail, regardless whether this is
checked at compile-time or at runtime.

A type "error" detected at compile-time doesn't imply that the
program will fail.

Actually it does, in a statically typed language. If you write a
function which expects a Boolean and you pass it a string instead,
it's going to fail one way or another.

OK, the bad call of that function might never be reachable in actual
execution, but equally the syntax error in Tcl code might not be
reached. I'd rather find out about both kinds of mistake sooner
rather than later.

(I do mean a type error and not a type 'error' - obviously if you have
some mechanism to catch exceptions caused by passing the wrong type,
you wouldn't want this to be checked at compile time.)

 

[Matthias Blume]

Actually it does, in a statically typed language.

Nitpick: Neither syntactic nor statically checked type errors make
programs fail. Instead, their presence simply implies the absence of a
program. No program, no program failing...

Matthias