A Use of Static Typing

A Use of Static Typing

Post by ram » Tue, 31 Jul 2007 22:50:54



Sometimes it is disputed whether static typing has
an advantage.

I sometimes change the interface of some entity, for
example

int get_difference();

is to become

double get_difference();

When I change just this entity, the compilation process
often will fail, because a site using et_difference? now has a type mismatch: I have to change something at
this site, too. This might create a cascade of even more
type error message, because the new change leads to
other type mismatches at other places. And so on.

Eventually all sites depending directly or indirectly on the
type of the result of et_difference?have been found
and modified to reflect the change.

Without a static type system, I could not have used the
error messages to guide me to all those sites.

So, is this an argument in favor of static typing?
 
 
 

A Use of Static Typing

Post by Robbert Ha » Tue, 31 Jul 2007 23:11:57


Absolutely. Actually, it is almost _the_ argument in favor of static
typing.

By my definition (beware, there are others), static typing means
rejecting programs, unless their types have been proven correct
statically (i.e. without actually running the program).

This means that any type error your program contains (ignoring holes in
the type system, such as type casts in C) must be fixed before the
program is allowed to run.

Your advantage of receiving help with the refactoring of the program
follows from the above.

Regards,

Bob

--
You'll get my inches, miles and gallons when you pry them from my cold
dead feet!

-- Seen on Slashdot

 
 
 

A Use of Static Typing

Post by Nils M Hol » Wed, 01 Aug 2007 00:23:49


> often will fail, because a site using et_difference? > now has a type mismatch: [...]

It is an argument against (explicit) static typing, because it
is exactly the explicit type information which causes the problem
in the first place.

--
Nils M Holm <n m h @ t 3 x . o r g> -- http://www.yqcomputer.com/
 
 
 

A Use of Static Typing

Post by ram » Wed, 01 Aug 2007 01:19:05

Nils M Holm < XXXX@XXXXX.COM > writes:

This holds if the changes are the changes of the types only,
but sometimes other changes needs to be done as well.

For example, in

printf( "%d", v );

, when the type of ?changes from nt?to ouble?
the ?needs to be changed to ?

So, the type errors guide one to all sites
requiring inspection for such changes.

Of course, one now might argue, that this only shows
that the use of format specifiers, like ? is a
problem. This might be true, but some languages
or libraries contain such elements, so one has
to deal with them somehow.
 
 
 

A Use of Static Typing

Post by Nils M Hol » Wed, 01 Aug 2007 02:02:34


Static typing is still the problem here. In a dynamically
typed language you would have a format specifier for numbers
in general rather than a specific type of number.


In other words: the type error guides you to all sites
where explicit static typing caused even more errors.


No. See above.


Of course, once the problem is there, you have to deal
with it in some way. In this particular case, I would
say that explicit static typing is the problem and
dynamic typing (or type inference) would be a solution.

--
Nils M Holm <n m h @ t 3 x . o r g> -- http://www.yqcomputer.com/
 
 
 

A Use of Static Typing

Post by Chris Smit » Wed, 01 Aug 2007 02:28:25


Actually, that has nothing at all to do with static typing. If you want
to design a printf-variant that uses the same format specifier for all
numbers, then fine. You can do that in any language, regardless of
whether it provides static types or not. I would like to address your
concern about doing this with static types, but I'm having trouble
imagining what that concern could be. This obviously has nothing to do
with static types.

Of course, it doesn't really address the problem. Suppose the change
request is now that the int needs to become a string. Oops, same
situation. You need to find everywhere where code was written to assume
that it's a number, and evaluate how to change it. If that knowledge is
embedded into the program in a form that your tools can understand,
that's not so hard. If it's not, then you have more of a problem.

(This is not to say that I agree with you about the distinction between
integers and floating point numbers being unessential; in fact, I'm
convinced you're dead wrong about that. But it's not necessary for the
larger point here, since there is even more clearly an essential
difference between numbers and strings.)


The interesting question is whether the code would have worked if you
just let it compile. You haven't answered that question. Compiler
errors are a good thing if the code wasn't going to work.


Unfortunately, I see absolutely no reason to believe this is the case.
If you really think that code never makes any assumptions about the type
of data it's using, or that everyone's code just magically works unless
the evil type system interferes, then I'm really not sure what to say.
Writing code that remains correct in the face of unanticipated changes
in its inputs and outputs is a hard problem; not something that happens
by accident as long as you keep your nose out of it.

--
Chris Smith
 
 
 

A Use of Static Typing

Post by Nils M Hol » Wed, 01 Aug 2007 03:32:16


It is, because %d is coupled to a specific type rather than a range
of types, which dynamic typing or type inference would allow. And
note that I am not talking about static typing, but about *explicit*
static type information.


Then please do so in C.


In case all of the operators you use in the procedure in question
support the old type as well as the new one, type inference or dynamic
typing both solve the problem. A procedure that wants to print a number
*obviously* does not accept strings, no matter what type system you are
using, so this is a null argument.


Neither dynamic typing nor type inference is about "just letting
some code compile". *Of course* the code would either work or the
type system would flag an error.

And note that we are not talking about C here, where "just letting
something compile" may be a commonplace practice, but about real
type systems.


Then you might want to do some research.


Do you actually read what I write? I have not said anywhere that
static typing is bad /per se/. But I am repeating myself. Just
re-read my earlier postings. Or even this one.


Most problems introduced by type annotations are solved.
You might want to catch up.

--
Nils M Holm <n m h @ t 3 x . o r g> -- http://www.yqcomputer.com/
 
 
 

A Use of Static Typing

Post by Vzalamataz » Wed, 01 Aug 2007 05:35:50

I cannot get beyond the irksome idea that this is the problem with the
potential to demonstrate that zero (0) is TRUE, and -1 is FALSE. It is
seems relaible that the same function will return the same answer. I take
that answer to be a value of a mathematical expression, evaluated as TRUE or
FALSE where you compiler tests some other value, and gives an error. So
just set the true to be zero, like I hav explained so many time... Take
findings to radical poetry month reading, and see how fast your are pushed
off that stage ...



> often will fail, because a site using et_difference? > now has a type mismatch: I have to change something at
 
 
 

A Use of Static Typing

Post by Chris Smit » Wed, 01 Aug 2007 06:15:37

Rude comments snipped. Oops, nothing left. Some rudeness reluctantly
restored.]

Nils M Holm < XXXX@XXXXX.COM > wrote:

Explicit type information certainly doesn't prevent polymorphism. Why
would it?


Fine, you win. I can't do it in C. Nor could I do it in a language
that doesn't have a concept of functions, for goodness sake. Of course,
this has nothing to do with types or inference, and I'm not interested
in whether you can score points by abandoning the topic.

Here it is in Haskell, a statically typed language that is far more
strictly typed than C. (And just to make you happy, I didn't use any
type inference; though it would be irrelevant if I did.)

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}

module MyPrintf where

class Printf a where
format :: String -> a

class PrintfArg a where
asNumber :: a -> String
asString :: a -> String

myprintf :: (Printf a) => String -> a
myprintf s = format s

instance Printf (IO ()) where
format = putStr

instance (PrintfArg a, Printf b) => Printf (a -> b) where
format s a = let sub s a = case span (/= '%') s of
(s', []) -> error "Too many args"
(s', ('%':'n':t)) -> s' ++ asNumber a ++ t
(s', ('%':'s':t)) -> s' ++ asString a ++ t
(s', ('%':t)) -> s' ++ "%" ++ sub t a
in format (sub s a)

instance Num a => PrintfArg a where
asNumber = show
asString = error "expected string; got number"

instance PrintfArg String where
asNumber = error "expected number; got string"
asString = id

And here it is in use:

*MyPrintf> myprintf "Hello\n" :: IO ()
Hello
*MyPrintf> myprintf "Hello, %s\n" "Chris" :: IO ()
Hello, Chris
*MyPrintf> myprintf "Hello, %n\n" (27 :: Int) :: IO ()
Hello, 27
*MyPrintf> myprintf "Hello, %n\n" (27.0 :: Double) :: IO ()
Hello, 27.0
*MyPrintf> myprintf "Hello, %n\n" "Chris" :: IO ()
Hello, *** Exception: expected number; got string


Type inference simply determines the most generic type that allows a
block of code to work. If you explicitly declare that type, the same
things still work. Type inference is unrelated to the question; it's a
diversion in this discussion, and nothing else.

Of course, if one explicitly declares types that are more restricted
than the inferrable types, something can break. Then the question is
why one chose to do that. Perhaps it's because that expresses the
assumptions made in writing the code; and one *wants* the programmer to
recheck the code if those assumptions are broken.


Huh? Where did you lose the topic? Just as a reminder, we're
discussing Stefan's comment:


You said:
(1) the problem is static typing, and
(2) the solution is to give printf one tag for all numeric types.

I responded
(1) that static (or explicit) typing is entirely orthogonal, and
(2) solving the problem for just numeric types isn't enough.

In this case, it's not true that printf "*obviously* does not accept
strings". In fact, it does accept strings; you just need to change the
format. If the type system caught the error (which would basically mean
some major dependent type hackery, or a special case for printf like
what gcc does),
 
 
 

A Use of Static Typing

Post by thomas.mer » Wed, 01 Aug 2007 06:27:35


> > often will fail, because a site using et_difference? > > now has a type mismatch: [...]
So you expect the program to deliver correct results with

string get_difference();

and

file get_difference();

Should the dynamic (or implizit static) typing system
automagically decide what to do?
Or will there be a runtime error.

Without any errors such a program will return 42.

When there are errors, I prefer to get them at
compilation time.

If there is no static type checking it is
necessary to test all code paths of a program.
For most programs this is not easily possible
(and almost never done).

So static type checking saves you a lot of testing.

Greetings Thomas Mertes

Seed7 Homepage: http://www.yqcomputer.com/
Seed7 - The extensible programming language: User defined statements
and operators, abstract data types, templates without special
syntax, OO with interfaces and multiple dispatch.
 
 
 

A Use of Static Typing

Post by Nils M Hol » Wed, 01 Aug 2007 14:47:21


I will try. BTW: Taking statements out of context and then attacking
them (which you did) is about as rude as I was.

But I am patient, so let me try to clarify my point once more.

1) The fact that changing one type annotation leads to errors is
an argument against /explicit/ static typing, because it is the
type annotation itself that causes the cascade of errors in the
first place.

2) "%d" /is/ an explicit type annonation, because it says "integer"
and not something more general, like "number".

You countered the argument by saying that I cannot change the
integer to a string in a type inferred language. This is true for
/some/ programs (when at least one operator of the procedure in
question accepts numbers, but no strings) and in this cases you
reach the limits of any known type system known so far, or at
least known to me.

Nevertheless does dynamic typing or type inference allow some
changes that explicit typing does not. As long as all operators
in your procedure support both the old and new type, you do not
have to change the procedure at all. Using explicit static typing
you have to change it for each single new type.

This is what I call an argument against explicit static typing.
And your argument was basically that you can break /any/ type
system. Fine, you can. So?

--
Nils M Holm <n m h @ t 3 x . o r g> -- http://www.yqcomputer.com/
 
 
 

A Use of Static Typing

Post by Nils M Hol » Wed, 01 Aug 2007 16:25:44

Chris, I was under the impression that you tried to push me to the
anti static typing camp (where I definitely do not belong), and I
think I found the reason for this:


| It is an argument against (explicit) static typing, because it
| is exactly the explicit type information which causes the problem
| in the first place.

This should have been, of course:

| It is an argument against *explicit* static typing, [...]

So I am sorry for overreacting, because my original formulation
was indeed a bit unfortunate.

I am not at all arguing against static typing. My sole point is
that explicit static typing (without inference or polymorphism)
often gets in your way. The original posters scenario is a classic
example for this.

And of course you are right when you say that explicit static
typing plus polymorphism is also a solution, although I still
would argue that it is by far not as flexible as type inference
plus polymorphism.

--
Nils M Holm <n m h @ t 3 x . o r g> -- http://www.yqcomputer.com/
 
 
 

A Use of Static Typing

Post by Robbert Ha » Wed, 01 Aug 2007 17:21:42

n Tue, Jul 31, 2007 at 05:47:21AM +0000, Nils M Holm wrote:

Not true. It is not the type annotation that causes the errors, but the
fact that a value of a certain type is fed to an operation that does not
accept that type.

The fact that there is a type annotation is irrelevant. One way to
explain that is that the annotation could have been "any type that
suppports the required operations". Perhaps a given language does not
support such annotations, but that isn't a weakness of explicit type
annotations, but rather of the type system of that language.


I don't really want to go here, as C format strings make for very muddy
waters. There are a lot of definitions you would have to agree on before
any meaningful discussion is possible about whether or not "%d" is an
explicit type annotation and whether or not it is more so than a
hypothetical format directive that accepts any number.


That depends. Actually, you need to be very careful about separating a
number of related issues. Static vs. dynamic typing, type annotations,
type inference, and polymorphism are all related, but can occur in
various combinations.


And now we're back where the discussion started. As long as the new
types support all operations the program performs on them, the program
does not have to change, and any type system that forces it to change
anyway is getting in the way.

On the other hand, if the new types do not support all operations that
the program performs on them, the program must be changed, and static
typing will (as the original poster claimed) help you find the instances
where these changes need to occur. It will also (as I've pointed out
earlier) prevent you from running your program until the types and
operations match again. Both of these are good. The latter is the
definition of static typing. The former is a benefit of static typing
that might also be obtained through soft typing.


That depends on your type annotations. For example, in Java, a type
annotation naming a class will accept that class and any subclass, and a
type annotation naming an interface will accept any class implementing
that interface. That's a far cry from "you have to change it for each
single new type".

Also, I note that you are talking about _explicit_ static typing,
whereas the original post was about static typing in general. From your
posts, I get the impression that you equate the two, which I feel is
harmful to the discussion. Static typing and explicit typing are
orthogonal (OCaml has static typing, but no need for type annotations;
Common Lisp has dynamic typing, but uses type annotations for ad-hoc
polymorphism).

The original poster correctly pointed out an advantage of static typing:
it points out where you have type errors _before_ you run your program.

You seem to see his example as a demonstration of a disadvantage of
explicit typing: the need to change type annotations when a type
changes, even if the new type is interface-compatible with the old type
is a Bad Thing. While I agree with the latter, I don't see that explicit
typing necessarily leads there. Given a sufficiently expressive type
system, and given correct (in this case, not overly restrictive) usage
of type annotations by the programmer, the problem doesn't occur.

Now, if you want to claim that the type systems of many common languages
that require explicit type annotations are lacking
 
 
 

A Use of Static Typing

Post by Nils M Hol » Wed, 01 Aug 2007 18:11:06

obbert Haarman < XXXX@XXXXX.COM > wrote:

IMO, it is a combination of them that causes the error. If the language
would infer the types or allow union types (like ML) or dynamic types,
the error would not occur. The type annotation fixes the type too early
and hence is part of the problem.


True. When I said "explicit type information" I implied that the
language is limited to such (like C or Pascal) and does not provide
additional means of dealing with types, like inference. In such
languages, explicit typing notoriously get in your way.


Yes, and you have to weight the benefits of each of them carefully.
In fact it would be interesting to summarize some of the combinations
and attempt to describe their differences, strengths, and weaknesses.
Here are some attributes I would include:

Static The compiler catches type errors
Dynamic The runtime system catches type errors
Implicit The compiler infers types
Explicit The programmer specifies types
Polymorphism Procedures may accept different types
or Union types or types may have different properties

And, yes, most languages use combinations of these. Given this summary,
my original point (although stated poorly) was that

1) explicit static typing (with none of the other properties) often sets
you up for trouble;

3) the combinations {dynamic} and {static,implicit} are both improvements
over {static,explicit}.

Of course other combinations are also interesting, like
{static,implicit,explicit+polymorphism}
or {static,implicit,explicit+union types}


Which is was I tried to say from the beginning.


I mostly agree.

The rest I will let pass, because I do not want to expand this discussion
to a "dynamic" vs "static" debate. I am sure that both of these approaches
have their advantages.

Only one point: in case you meant "soft" = "dynamic" I have to disagree.
"Soft" or "weak" typing is what C does. I have yet to see a dynamic
language with "weak" typing in the sense that you can override the type
system.


Yes. I would file this under polymorhism.


Indeed. As I already wrote in another follow-up to Chris, this is
an impression you could easily get from my earlier postings. However,
this is not what I actually wanted to say. I hope I could clarify
things in this posting.


These are good examples. ML and Haskell(?) would be examples that use
implicit and explicit static typing. Scheme would be an example for
a language that uses dynamic typing exclusively. And, yes, I would
see this as a great improvement over pure {static,explicit} typing as
defined above.


I would happily give up the {static,explicit} combination for {dynamic},
which was one of my points. The other one was that I would rather have
implicit typing than explicit typing. Although {static,implicit,explicit}
is also fine.


Yes, this sums it up pretty well.

--
Nils M Holm <n m h @ t 3 x . o r g> -- http://t3x.org/nmh/
 
 
 

A Use of Static Typing

Post by Robbert Ha » Wed, 01 Aug 2007 20:10:18


I agree with everything you said.

Yes, two posters agree with each other. On Usenet. And it's not April
Fools Day.

Regarding soft typing:


By "soft typing" I mean that type checking is performed as for static
typing, but without rejecting the program if type checking fails.
Instead, the compiler might emit a warning and insert a run-time check.
Thus, you get early error detection as for static checking, and full
flexibility as for dynamic checking.

For an example, see Soft Typing by Robert Cartwright and Mike Fagan,
available from http://www.yqcomputer.com/

Note that "soft typing" is different from "weak typing": weak typing, at
least according to the definition I know, is implicit type conversion.
Things like "foo: " + 12 in Java, where 12 is implicitly converted to a
String.

Being able to override the type system, finally, is yet a different
thing. I'm not exactly sure what it actually means (if the language
allows you to do it, it is _part_ of the type system, right?), but I
assume you mean things like casts in C. Casts in C aren't weak typing;
they're simply a way to lie to the type checker. This makes C
type-unsafe, but, alas, is the work-around for the otherwise overly
restrictive type checker.

Regards,

Bob

--
``I see'' said the blind man, as he picked up the hammer and saw.