Python from Wise Guy's Viewpoint

[prunesquallor@comcast.net]

Re: Python from Wise Guy's Viewpoint

Dirk Thierbach <dthierbach@gmx .de> writes:
[color=blue]
> prunesquallor@c omcast.net wrote:[color=green]
>> gt5163b@prism.g atech.edu (Brian McNamara!) writes:[/color]
>[color=green][color=darkred]
>>> This one is so easy, we do it in C++ just for spite. :)
>>> I'm using the FC++ library as a helper.[/color][/color]
>[color=green]
>> Yuck! Type declarations *everywhere*. Where's this famous inference?[/color]
>
> 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.[/color]

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.

Dirk Thierbach <dthierbach@gmx .de> writes:
...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)

Joachim Durchholz <joachim.durchh olz@web.de> writes:
... 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 <vanicat+invali d@labri.fr>
`I don't see how this function can be useful...'

Jesse Tov <tov@eecs.harvR EMOVEard.edu>
`we don't need functions with those types.'

Dirk Thierbach <dthierbach@gmx .de>
`recursive types are very often a result of a real typing error.'

"Marshall Spight" <mspight@dnai.c om>
`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 <joachim.durchh olz@web.de> 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]

Re: Python from Wise Guy's Viewpoint

Don Geddis <don@geddis.org > writes:
[color=blue]
>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.[/color]

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 <ed@membled.com >

[Ed Avis]

Re: Python from Wise Guy's Viewpoint

prunesquallor@c omcast.net writes:
[color=blue]
>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.[/color]

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.
[color=blue]
> 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.[/color]

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).
[color=blue]
>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.[/color]

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]
[color=blue]
>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.[/color]

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.

--
Ed Avis <ed@membled.com >

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Andreas Rossberg wrote:
[color=blue]
> As an example of the kind of "overloadin g" (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.[/color]

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.

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Ed Avis wrote:
[color=blue]
> - 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?[/color]

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

[Pascal Costanza]

Re: Python from Wise Guy's Viewpoint

Dirk Thierbach wrote:
[color=blue][color=green]
>>I think you have a restricted view of what "type" means.[/color]
>
>
> 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.[/color]

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.)
[color=blue][color=green][color=darkred]
> >>P.S.: Please always remember the original setting of this thread. The[/color]
>>original original questions was something along the lines of "why on
>>earth would one not want a static type system?"[/color]
>
> The answer to this is of course "You use what you like best. End of
> story."[/color]

Fine. (Really.)
[color=blue]
> 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.[/color]

"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.
[color=blue][color=green]
>>Yes, you can clearly tell from my postings that I prefer dynamic typing
>>over static typing.[/color]
>
> 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.[/color]

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

[Joachim Durchholz]

Re: Python from Wise Guy's Viewpoint

prunesquallor@c omcast.net wrote:[color=blue]
> 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.[/color]

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.
[color=blue]
> 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.[/color]

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).
[color=blue]
> 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.[/color]

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.
[color=blue]
> 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.[/color]

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.
[color=blue]
> Being unable to prove code correct is the same thing as being able to
> prove it incorrect.[/color]

This true for HM typing but not true for inference systems in general.
But probably you wanted to say something else anyway.
[color=blue]
> 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.[/color]

Agreed.
Programs in class 2 are rarely encountered and quickly fixed, so I'm not
sure that this category is very interesting.
[color=blue]
> 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.[/color]

There's also the question how to decide whether a program is in class 1
or class 3.
[color=blue]
> 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.[/color]

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.)
[color=blue]
> (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.
>
> Dirk Thierbach <dthierbach@gmx .de> writes:
> ...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)
>
> Joachim Durchholz <joachim.durchh olz@web.de> writes:
> ... 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 <vanicat+invali d@labri.fr>
> `I don't see how this function can be useful...'
>
> Jesse Tov <tov@eecs.harvR EMOVEard.edu>
> `we don't need functions with those types.'
>
> Dirk Thierbach <dthierbach@gmx .de>
> `recursive types are very often a result of a real typing error.'
>
> "Marshall Spight" <mspight@dnai.c om>
> `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 <joachim.durchh olz@web.de> replied:
> ``Matthias' and my position is that such a program doesn't exist
> (and cannot even exist)''[/color]

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).
[color=blue]
> 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.[/color]

That's a misunderstandin g, 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]

Re: Python from Wise Guy's Viewpoint

Don Geddis wrote:
[color=blue]
> Dirk Thierbach <dthierbach@gmx .de> writes:
>[color=green]
>>Hindley-Milner type inference always terminates. The result is either
>>a provable mismatch, or a provable-non-mismatch.[/color]
>
> 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.[/color]

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 :-)
[color=blue]
> 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.[/color]

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

[prunesquallor@comcast.net]

Re: Python from Wise Guy's Viewpoint

Joachim Durchholz <joachim.durchh olz@web.de> writes:
[color=blue]
> prunesquallor@c omcast.net wrote:
>[color=green]
>> Being unable to prove code correct is the same thing as being able to
>> prove it incorrect.[/color]
>
> This true for HM typing but not true for inference systems in
> general. But probably you wanted to say something else anyway.[/color]

Um, yeah. I did:

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

[prunesquallor@comcast.net]

Re: Python from Wise Guy's Viewpoint

Joachim Durchholz <joachim.durchh olz@web.de> writes:
[color=blue]
> 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?[/color]

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]

Re: Python from Wise Guy's Viewpoint

Joachim Durchholz wrote:
[color=blue]
> 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?[/color]

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

[Tomasz Zielonka]

Re: Python from Wise Guy's Viewpoint

Brian McNamara! napisa³:[color=blue]
> prunesquallor@c omcast.net once said:[color=green]
>>Are they happy with something like this?
>>
>>(defun black-hole (x)
>> #'black-hole)
>>
>>(for non lispers, the funny #' is a namespace operator.
>> The black-hole function gobbles an argument and returns
>> the black-hole function.)[/color]
>
> 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. :)[/color]

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

--
..signature: Too many levels of symbolic links

[Joachim Durchholz]

Re: Python from Wise Guy's Viewpoint

prunesquallor@c omcast.net wrote:[color=blue]
> Joachim Durchholz <joachim.durchh olz@web.de> writes:
>[color=green]
>>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?[/color]
>
> 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.[/color]

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.
[color=blue]
> 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.[/color]

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

[Fergus Henderson]

Re: Python from Wise Guy's Viewpoint

Pascal Costanza <costanza@web.d e> writes:
[color=blue]
>Fergus Henderson wrote:
>[color=green]
>> In my experience, people who have difficulties in getting their programs
>> to typecheck usually have an inconsistent design, not a design which is
>> consistent but which the type checker is too restrictive to support.[/color]
>
>Have you made sure that this is not a circular argument?[/color]

Yes.
[color=blue]
>Does "consistent design" mean "acceptable by a type checker" in your book?[/color]

No.

--
Fergus Henderson <fjh@cs.mu.oz.a u> | "I have always known that the pursuit
The University of Melbourne | of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.

[Dirk Thierbach]

Re: Python from Wise Guy's Viewpoint

Don Geddis <don@geddis.org > wrote:[color=blue][color=green]
>> prunesquallor@c omcast.net reasonably noted:[color=darkred]
>> > If there are three values that can arise --- provable-mismatch,
>> > provable-non-mismatch, and undecided --- then you cannot assume that
>> > ~provable-mismatch = provable-non-mismatch.[/color][/color]
>
> Dirk Thierbach <dthierbach@gmx .de> writes:[color=green]
>> Hindley-Milner type inference always terminates. The result is either
>> a provable mismatch, or a provable-non-mismatch.[/color]
>
> You're completely wrong, which can be easily demonstrated.[/color]

Unfortunately, I can *prove* that the HM-type inference always terminates,
without any timeout, by induction on the length of the expression.
[color=blue]
> 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.[/color]

Yes, you can do that. But it's not done during HM-type inference.
[color=blue]
> 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?[/color]
[color=blue]
> The answer is no.[/color]

Right. It cannot, because that question is not decidable.
[color=blue]
> That's one obvious case, so even you know that your claim of a "provable
> mismatch" is incorrect.[/color]

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.
[color=blue]
> There are programs that will never have run-time
> errors, but your static type inference will claim a type error.[/color]

Yes. But these programs will have problems, even without a run-time error.
Rewrite them to increase the quality of your software.
[color=blue][color=green]
>> or because you have an implicit restriction for possible arguments to this
>> expression the type system doesn't know about, than you could call it a
>> "valid program", but it will still be rejected, yes.[/color][/color]
[color=blue]
> 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)))[/color]
[color=blue]
> 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.[/color]

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.
[color=blue]
> 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.[/color]

Yes. That's why you cannot express such restrictions statically.
[color=blue]
> 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"?[/color]

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).
[color=blue]
> 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.[/color]

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