The Artima Developer Community
Sponsored Link

Weblogs Forum
Programming with "Duh" Typing

370 replies on 25 pages. Most recent reply: Aug 8, 2007 9:54 AM by James Watson

Welcome Guest
  Sign In

Go back to the topic listing  Back to Topic List Click to reply to this topic  Reply to this Topic Click to search messages in this forum  Search Forum Click for a threaded view of the topic  Threaded View   
Previous Topic   Next Topic
Flat View: This topic has 370 replies on 25 pages [ « | 1 ... 12 13 14 15 16 17 18 19 20 ... 25  | » ]
Achilleas Margaritis

Posts: 674
Nickname: achilleas
Registered: Feb, 2005

Re: Static Type Checks are not Tests Posted: Jul 20, 2007 7:54 AM
Reply to this message Reply
Advertisement
> I've thought about it, and I've decided that static type
> checks are not tests. Tests are dependent on codepath.
> Each test excerises a different codepath (well,
> , more-or-less, some may validate that several different
> inputs have the same codepath). While static type
> checking is completely independent of codepath.

Actually, type checks are tests, if done correctly. Type checking is a form of theorem proving. See the following link for details:

http://lambda-the-ultimate.org/node/2353#comment-35194

The problem is that current static type systems of mainstream programming languages leave a lot to be desired.

Achilleas Margaritis

Posts: 674
Nickname: achilleas
Registered: Feb, 2005

Re: Programming with "Duh" Typing Posted: Jul 20, 2007 8:00 AM
Reply to this message Reply
> > The documentation burden is also equal in both cases.
> Even
> > with static typing, types do not tell us anything about
> > how the variables are used, so they have to be
> > documented.
>
> I see the documentation burden on dynamic languages being
> much higher because the variable declarations in a static
> language are a form of automatic documentation. For
> example, in java, if I'm looking at someone else's code
> and I see
>
> Map<URI, Date> dates = someObject.getSomething();
>
> I immediately know that the dates variable is a Map of
> Dates with URI as the key. If I haven't forgotten what
> the usual methods are on a Map I immediately know what
> methods I can use if I need to modify the code.
>
> With a dynamic language I'd have to trace back through the
> code to find what methods I can use on that object.

But what kind of dates does the variable 'dates' represent? it's not visible from the code you posted. Perhaps you meant to write it like this:

//dates that the products were shipped
Map<URI, Date> dates = someObject.getSomething();


But then you placed a comment in it! if that is not documentation, I don't know what it is.

Cedric Beust

Posts: 140
Nickname: cbeust
Registered: Feb, 2004

Re: Programming with "Duh" Typing Posted: Jul 20, 2007 8:40 AM
Reply to this message Reply
> The only changes that do not require testing are the very
> trivial ones, which is a very limited set of changes.

That's incorrect.

Renaming a type can sometimes impact hundreds of different classes. It's something that's 100% safe in a statically typed language but requires heavy testing with a dynamic language, to the point that I sometimes decide not to do it because I think it's not worth the risk.

IDEA and Eclipse offer more than thirty such refactorings, all of which are 100% safe, and this number is growing with each new release, so I would certainly not call this set "limited" nor "trivial".

--
Cedric
http://testng.org

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: Programming with "Duh" Typing Posted: Jul 20, 2007 9:01 AM
Reply to this message Reply
> Even if you spot the problem in a previous branch, you can
> pause the program, change the values, and let the program
> continue from the previous branch, or divert it so as that
> the previous branch runs at some point in the future.

Assuming we are talking about the same thing, that is something. Does anyone know of a tool that does this with Python or is it under my nose?

I actually started thinking about the pause and restart idiom and it might be a feature that I would want to incorporate into my application and not just for testing and development.

I am still not convinced that dynamic programming always trumps static programming but I hope you understand that I am not a partisan in this issue.

> I actually started with maintaining a Smalltalk program
> written by someone else.

I assume you found it easy to modify. Is that correct?

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: Programming with "Duh" Typing Posted: Jul 20, 2007 9:27 AM
Reply to this message Reply
> But you can't be sure, even with a static type system,
> that your code is correct. For example, an int erroneously
> converted to short can create great problems. Only
> functional testing can reveal the problems.
>
> ...
>
> Actually, you do. Declaring a function to take type 'int'
> does not say much. You need to document, for example, if
> that integer is to be used as an index in an array, if
> negative values are valid, what will happen if I pass 0,
> etc.

I want to propose something and I hope no one will take offense to it. I don't mean this to be a shot at anyone or to imply anything other than that there are different ways to think about programming.

First of all I just want to clarify that changing an int to a short is not what I mean by making a safe change. That's rarely safe and is one of the hardest kinds of changes. Static typing does help you inventory what kind of pain you are getting into, though. I find it a lot easier to make this kind of change in a static language because I actually know what impact it has. I would have to run tests just to find the dependencies in a dynamic language in a lot of cases.

But more importantly, I think there is a disconnect here. You are talking about primitive or universal types. What I am really talking about are custom types. This is something that Erik alluded to before. It seems to me that a lot of the developers who prefer dynamic programming are those who do not use many custom types in their programs. I find that when I use a dynamic language, I don't use as many custom types precisely because dynamic languages support 'standard type development' so much more.

My contention is that in a static language (e.g. Java), if you do not use custom types liberally, you are not getting much (if any value) from the static type system.

For example, I am currently working on a OS project with a brilliant person who has no professional development experience. Given that lack of experience, what he has achieved is very impressive but one of the things that he has done that basically nullifies the value of static typing in the application is that he has uses raw arrays of doubles to represent a point in n-dimensions. That is, all the classes and methods dealing with these points depend on double[]. This makes it very hard to track dependencies. If I search for usage of double I'll get back a tidal wave of results. It's useless information. So one of the changes I plan to make is to convert this code to use a Point class. Once I do that, I will now be able to see what classes use them and what they are doing with them. The semantics of the program will be coded into the type, not defined solely in the code that uses the data.

I just think we are talking about different things when you use examples like changing an int to a short.

Erik Engbrecht

Posts: 210
Nickname: eengbrec
Registered: Apr, 2006

Re: Static Type Checks are not Tests Posted: Jul 20, 2007 9:45 AM
Reply to this message Reply
>
> Actually, type checks are tests, if done correctly.

I disagree, and feel supported in my disagreement by your attached thread.

> Type checking is a form of theorem proving.

Agreed.

> See the following
> link for details:
>
> http://lambda-the-ultimate.org/node/2353#comment-35194

Interesting thread, I think this post very succintly states what I am thinking:
http://lambda-the-ultimate.org/node/2353#comment-35201

> The problem is that current static type systems of
> mainstream programming languages leave a lot to be desired.

Agreed.

So I'll tie this back to my arguments. The static type systems in mainstream programming languages don't allow me to prove my program is correct, or even free of typos. But it does allow me to prove my program is free of some common classes of typos, and I find that proof to be very useful.

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: Programming with "Duh" Typing Posted: Jul 20, 2007 9:49 AM
Reply to this message Reply
> > The only changes that do not require testing are the
> very
> > trivial ones, which is a very limited set of changes.
>
> That's incorrect.
>
> Renaming a type can sometimes impact hundreds of different
> classes. It's something that's 100% safe in a statically
> typed language but requires heavy testing with a dynamic
> language, to the point that I sometimes decide not to do
> it because I think it's not worth the risk.

I don't disagree with this in any way but I think this example runs the risk of trivializing the value of static typing.

To expand on the point example from my post above, using a double[] to represent this means that the documentation, to be complete, must be repeated again and again. There is no one central place to go and find out about points and how they are used. The double[] declaration carries no semantical information with respect to that particular application. If I declare a Point type, I don't need to describe what a point is and how it is structured everywhere I use it. All I need to do is describe what I am doing in my method and how points fit in.

In a dynamic language it's much the same as the double[] situation in a static language. I cannot see from a variable declaration what it represents or where I should look to find documentation. I must document everywhere that it is used, what is, and how it is expected to behave. With duck-typing, the method really needs public documentation on how that variable is used by the code. If might describe it as a file, but it could be any file-like type. Most likely it only depends on a subset of file behaviors. There are really no dependencies on any type. The dependencies are the names used with respect to that variable. In one aspect this can be liberating and makes things very flexible but on the other hand, it makes it very hard to keep track of the program structure.

Rusty Wright

Posts: 8
Nickname: lumpynose
Registered: Jul, 2007

Re: Programming with "Duh" Typing Posted: Jul 20, 2007 11:18 PM
Reply to this message Reply
The Date type is not what concerns me, it's the outer Map type. In Ruby it could look something like

dates = someObject.getSomething();

I can guess that it has something to do with dates, but is it an array, a hash, or what? I don't know until I go digging through the code.

At this point I haven't even gotten to where I can think about the business logic since I have no clue what type that dates thing is and what I can do with it.


> > > The documentation burden is also equal in both cases.
> > Even
> > > with static typing, types do not tell us anything
> about
> > > how the variables are used, so they have to be
> > > documented.
> >
> > I see the documentation burden on dynamic languages
> being
> > much higher because the variable declarations in a
> static
> > language are a form of automatic documentation. For
> > example, in java, if I'm looking at someone else's code
> > and I see
> >
> > Map<URI, Date> dates = someObject.getSomething();
> >
> > I immediately know that the dates variable is a Map of
> > Dates with URI as the key. If I haven't forgotten what
> > the usual methods are on a Map I immediately know what
> > methods I can use if I need to modify the code.
> >
> > With a dynamic language I'd have to trace back through
> the
> > code to find what methods I can use on that object.
>
> But what kind of dates does the variable 'dates'
> represent? it's not visible from the code you posted.
> Perhaps you meant to write it like this:
>
>
> //dates that the products were shipped
> Map<URI, Date> dates = someObject.getSomething();
> 

>
> But then you placed a comment in it! if that is not
> documentation, I don't know what it is.

Michael Feathers

Posts: 448
Nickname: mfeathers
Registered: Jul, 2003

Re: Static Type Checks are not Tests Posted: Jul 21, 2007 5:16 AM
Reply to this message Reply
> > The testing burden in dynamically typed languages is
> not
> > greater than the testing burden of statically typed
> > languages, provided that you do functional testing for
> all
> > your requirements. Actually, the testing burden is
> equal
> > in both cases.
>
> I've thought about it, and I've decided that static type
> checks are not tests. Tests are dependent on codepath.
> Each test excerises a different codepath (well,
> , more-or-less, some may validate that several different
> inputs have the same codepath). While static type
> checking is completely independent of codepath.
>
> More generally, tests are purely empirical, while static
> type checks are purely deductive.
>
> The point of my comments is that static type checking
> immediately detects a class of errors that I commonly see
> in my own code that are very difficult, or even
> impossible, to detect via testing except by chance.
>
> Unit tests are not enough, because often times the place
> where the error is introduced (e.g., a member variable is
> set to a tuple instead of an integer) is often distant,
> both within the code and within execution of the program,
> from where the error causes failure (when arithmetic
> operations are attempted on the tuple). Only integrated
> testing can detect these errors, and even then a huge set
> of tests is required. Unless, of course, you specify the
> types of the member variables on the object and validate
> them at runtime or check all of them in your tests. In
> which case you've lost both the time savings and
> flexibility gain of dynamic typing.

When I argue that type checks are tests I'm not saying that we should do away with types. I'm just pointing out that typing and traditional testing are connected far more than people think.

To me, an automated test is a machine verifiable boolean statement about a program or a piece of a program. So, when I can say, in a Java program, that an instance of Integer can never be referred to by an HttpServletRequest field because they aren't type conformant, I'm basically doing the same thing as I would be if I said that Math.abs(-1) is 1, or Foo.bar(12) is 13 if Foo.staticThing is 1.

All of these are statements about programs. Sure, the first one is more global in scope than the other two, but I think see them as a part of the same thing is valuable because it's possible to extend languages so that they blur what has been seen as a hard line between type systems and tests.

Isaac Gouy

Posts: 527
Nickname: igouy
Registered: Jul, 2003

Re: Static Type Checks are not Tests Posted: Jul 21, 2007 12:06 PM
Reply to this message Reply
Michael Feathers wrote
-snip-
> To me, an automated test is a machine verifiable boolean
> statement about a program or a piece of a program.

You're in the clouds.

Back on the ground the nature of that "boolean statement" is kind of important.


> when I can say, in a Java program, that an instance of
> Integer can never be referred to by an HttpServletRequest
> field because they aren't type conformant, I'm basically
> doing the same thing as I would be if I said that
> Math.abs(-1) is 1, or Foo.bar(12) is 13 if Foo.staticThing
> is 1.

We're basically doing the same thing as we would be if we said that Math.abs(int) is int, of Foo.bar(int) is int if Foo.staticThing is int :-)


> All of these are statements about programs. Sure, the
> first one is more global in scope than the other two, but
> I think see them as a part of the same thing is valuable
> because it's possible to extend languages so that they
> blur what has been seen as a hard line between type
> systems and tests.

The first one is universal. With exhaustive tests can we make universal statements? Without exhaustive tests can we make universal statements?

The other two are unsuccessful tests - they don't show the existence of an error.

Isaac Gouy

Posts: 527
Nickname: igouy
Registered: Jul, 2003

Re: other tools Posted: Jul 21, 2007 12:16 PM
Reply to this message Reply
James Watson wrote
> That 'could' be true for any tool. Hitting myself in the
> head with a mallet 'might' make my headache go away it I
> do it enough. There's no way to prove that another whack
> won't do the trick. It makes no sense to recommend
> something because you don't know that it isn't worth the
> effort.

Previously you asked "Why don't you download Alloy and try to use it..."

You had a mistaken impression and I corrected it.

I think I might be in a better position to judge whether I know enough about Alloy to use it successfully than you ;-)

Isaac Gouy

Posts: 527
Nickname: igouy
Registered: Jul, 2003

Re: Programming with "Duh" Typing Posted: Jul 21, 2007 12:42 PM
Reply to this message Reply
James Watson wrote
-snip-
> Stating that seat-belts do not eliminate deaths in
> accidents is not the 'no perfect solution' fallacy. The
> fallacy is using that as an argument to say seat-belts
> should not be required is.

I can't be bothered quibbling about whether, given the context, there was an implicit argument rather than a simple assertion of fact.


> My argument is that in dynamic programming can actually be
> slower than static programming in certain contexts. I was
> told that this was absolutely not the case. Why should I
> not be allowed to question that? If someone suggests that
> something is a perfect solution, then the 'no perfect
> solution' fallacy does not apply.

I failed to find where you were told "this was absolutely not the case" so obviously I'm missing chunks of the discussion.

I hope one day we'll think it really strange that anyone quarrels about it being faster to program with A rather than B without providing some kind of evidence, and being specific about the circumstances.

Kay Schluehr

Posts: 302
Nickname: schluehk
Registered: Jan, 2005

Re: Static Type Checks are not Tests Posted: Jul 21, 2007 3:09 PM
Reply to this message Reply
> When I argue that type checks are tests I'm not saying
> that we should do away with types. I'm just pointing out
> that typing and traditional testing are connected far more
> than people think.

The similarity is a bit superficial. Type-checking is abstract interpretation and when the interpretation gets stuck a type error will be reported. That's just like letting a program run and raising an exception in case of an operation that can't be processed.

> To me, an automated test is a machine verifiable boolean
> statement about a program or a piece of a program.

Exactly. A test has to state an assertion. It always evaluates a predicate.

> So,
> when I can say, in a Java program, that an instance of
> Integer can never be referred to by an HttpServletRequest
> field because they aren't type conformant, I'm basically
> doing the same thing as I would be if I said that
> Math.abs(-1) is 1, or Foo.bar(12) is 13 if Foo.staticThing
> is 1.

But that's not what type-checking is doing. It doesn't make an explicit assertion about the relation between two arbitrary types. Instead type rules are applied on operands in order to compute the type of the resulting value of an operation. If one of the operands has a type where no rule can be applied the algorithm gets stuck and terminates.

Michael Feathers

Posts: 448
Nickname: mfeathers
Registered: Jul, 2003

Re: Static Type Checks are not Tests Posted: Jul 22, 2007 5:07 AM
Reply to this message Reply
> > When I argue that type checks are tests I'm not saying
> > that we should do away with types. I'm just pointing
> out
> > that typing and traditional testing are connected far
> more
> > than people think.
>
> The similarity is a bit superficial. Type-checking is
> abstract interpretation and when the interpretation gets
> stuck a type error will be reported. That's just like
> letting a program run and raising an exception in case of
> an operation that can't be processed.
>
> > To me, an automated test is a machine verifiable
> boolean
> > statement about a program or a piece of a program.
>
> Exactly. A test has to state an assertion. It always
> evaluates a predicate.
>
> > So,
> > when I can say, in a Java program, that an instance of
> > Integer can never be referred to by an
> HttpServletRequest
> > field because they aren't type conformant, I'm
> basically
> > doing the same thing as I would be if I said that
> > Math.abs(-1) is 1, or Foo.bar(12) is 13 if
> Foo.staticThing
> > is 1.
>
> But that's not what type-checking is doing. It doesn't
> make an explicit assertion about the relation between two
> arbitrary types. Instead type rules are applied on
> operands in order to compute the type of the resulting
> value of an operation. If one of the operands has a type
> where no rule can be applied the algorithm gets stuck and
> terminates.

Sure, there are differences, but at the end of it, traditional tests and type systems serve the same purpose. They allow us to have some assurance about the behavior of a program. Tools like JavaCop are a good example of the sort of thing that blurs the line. Some of the constraints that it imposes are the sort of thing that you can see as part of a type system but it can also be seen as a set of tests.

There are languages out there with extensible type systems. They blur the lines even further.

Erik Engbrecht

Posts: 210
Nickname: eengbrec
Registered: Apr, 2006

Re: Static Type Checks are not Tests Posted: Jul 23, 2007 3:45 AM
Reply to this message Reply
> Sure, there are differences, but at the end of it,
> traditional tests and type systems serve the same purpose.
> They allow us to have some assurance about the behavior
> r of a program. Tools like JavaCop are a good example of
> the sort of thing that blurs the line. Some of the
> constraints that it imposes are the sort of thing that you
> can see as part of a type system but it can also be seen
> as a set of tests.
>
> There are languages out there with extensible type
> systems. They blur the lines even further.

Just because two things serve similar, overlapping purposes, doesn't mean that they are the same thing. I don't think one can be substituted for another. When you use a dynamic language, you are trading a measure of certainty about your code for flexibility.

Flat View: This topic has 370 replies on 25 pages [ « | 12  13  14  15  16  17  18  19  20 | » ]
Topic: Programming with "Duh" Typing Previous Topic   Next Topic Topic: Python 3000 Plea for Help


Sponsored Links



Google
  Web Artima.com   

Copyright © 1996-2017 Artima, Inc. All Rights Reserved. - Privacy Policy - Terms of Use - Advertise with Us