The Artima Developer Community
Sponsored Link

Weblogs Forum
A Type System is a Set of Tests

73 replies on 5 pages. Most recent reply: Apr 26, 2006 4:08 AM by Achilleas Margaritis

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 73 replies on 5 pages [ « | 1 2 3 4 5 | » ]
Vesa Karvonen

Posts: 116
Nickname: vkarvone
Registered: Jun, 2004

Re: A Type System is a Set of Tests Posted: Apr 18, 2006 3:29 PM
Reply to this message Reply
Advertisement
just how complicated type inference is and who could maintain it?

Depends on how you measure "complicated", but the essense of many type inference based type systems can be described in about half a page of BNF and inference rules.

I'd like to say that any competent programmer should be able to maintain an implementation of a type inference algorithm, but I'm afraid there is no generally accepted norm for "competent" in this line of business. ;-)

Leo Lipelis

Posts: 111
Nickname: aeoo
Registered: Apr, 2006

Re: A Type System is a Set of Tests Posted: Apr 18, 2006 3:52 PM
Reply to this message Reply
> just how complicated type inference is and who could
> maintain it?

>
> Depends on how you measure "complicated", but the essense
> of many type inference based type systems can be described
> in about half a page of BNF and inference rules.
>
> I'd like to say that any competent programmer
> should be able to maintain an implementation of a type
> inference algorithm, but I'm afraid there is no generally
> accepted norm for "competent" in this line of business. ;-)

If that's true, then why it wasn't already added to every popular dynamic language? I mean, OCaml isn't exactly new, right? OCaml also gets many positive reviews.

If a person can have all the benefits of dynamic typing, such as interactive programming, duck typing, easy dynamic behaviors (as opposed to something grotesque like Java reflection API), small program size, while using a type inferance system, then maybe it almost makes no sense to use dynamic typing. The problem is that traditionally the languages that have been popular examples of static typing a) did not use type inference and b) were and are horrible in day to day usage compared to modern dynamic languages.

It seems like a system with implicit inferred static interfaces would be like the ultimate rubber band and then what would the need be to write your own "pluggable" type system? If the infinite rubber band works nicely and feels dynamic while giving all the benefits of static typing, then it's case closed -- we don't need any plugins. :)

Isaac Gouy

Posts: 527
Nickname: igouy
Registered: Jul, 2003

Re: A Type System is a Set of Tests Posted: Apr 18, 2006 4:14 PM
Reply to this message Reply
Erik Engbrecht wrote
> > Yes we always pass foo a Bar but, without looking at the
> > implementation, how will we know that foo(Bar x) does
> > indeed call x.rollback() when it should?
>
> You test it.

In that case, it doesn't make any difference if the language was statically type checked or dynamically type checked.

(Initially, it seemed as though you were saying that there was a difference.)

Vesa Karvonen

Posts: 116
Nickname: vkarvone
Registered: Jun, 2004

Re: A Type System is a Set of Tests Posted: Apr 18, 2006 4:32 PM
Reply to this message Reply
when it should?

I think that one should distinguish between verification and validation.

Erik Engbrecht

Posts: 210
Nickname: eengbrec
Registered: Apr, 2006

Re: A Type System is a Set of Tests Posted: Apr 18, 2006 7:52 PM
Reply to this message Reply
>In that case, it doesn't make any difference if the language was statically type checked or dynamically type checked.

>(Initially, it seemed as though you were saying that there was a difference.)

My point is static type usually buys you something, but sometimes that something isn't worth as much as it costs. Which is why I think static type information is something that should be incrementally added to a program as it is increasingly well understood.

Isaac Gouy

Posts: 527
Nickname: igouy
Registered: Jul, 2003

Re: A Type System is a Set of Tests Posted: Apr 19, 2006 10:43 AM
Reply to this message Reply
> My point is static type usually buys you something, but
> sometimes that something isn't worth as much as it costs.
> Which is why I think static type information is something
> g that should be incrementally added to a program as it is
> increasingly well understood.

Consider something that static type information buys us more precise refactoring and something that static type checking buys us consistency checking - it seems like those things will be valuable whenever we change the code.

Just as the benefits of unit tests are available as soon as we begin a program, the benefits of static type information are available as soon as we begin a program.

Leo Lipelis

Posts: 111
Nickname: aeoo
Registered: Apr, 2006

Re: A Type System is a Set of Tests Posted: Apr 19, 2006 3:15 PM
Reply to this message Reply
> >In that case, it doesn't make any difference if the
> language was statically type checked or dynamically type
> checked.
>
> >(Initially, it seemed as though you were saying that
> there was a difference.)
>
> My point is static type usually buys you something, but
> sometimes that something isn't worth as much as it costs.
> Which is why I think static type information is something
> g that should be incrementally added to a program as it is
> increasingly well understood.

That's now how I think when I program though. When I use statically typed languages, I always understand the types, but I also understand that my current understanding of types is of provisional nature.

In my opinion static types buy a lot less than people think. In particular, many arguments regarding reducing bug counts and reliability I think are unsubstantiated anecdotes. In my experience programs written in good dynamic languages tend to be pretty solid. Likewise, people do circumvent static typing by using the root object class when they feel lazy. So I understand static typing, as a tool at best, but not as any kind of guarantee at all. It still takes some discipline and maybe even wisdom to use it to full effect. But if you have such discipline and wisdom then you can use a dynamically typed language to an even greater effect.

Supposedly LISP doesn't have static typing. Is it true that there are refactoring LISP IDE's? If so, how do they do it?

If I can get whatever little benefits of static typing without actually thinking about types intentionally, and without paying any price, that's great. Otherwise, I'd rather take 1 extra run time bug per year (and 10,000 less bugs due to highly interactive nature of development and fewer files/KLOCs) and go with a dynamically typed language.

From this point of view, the only language I've heard of that seems to approach this, is OCaml. Other than OCaml or some other language like it, I don't prefer statically typed languages. OCaml has a really ugly syntax and is an eye sore. It's far from being elegant and minimalistic in its design, in my opinion. I like languages that have 3 features and 1 reserved keyword, and are extremely well understood at their core, and where 99% of functionality comes from a library. One such language is Scheme. If I could have Scheme with type inference a la OCaml, that might be an ideal language to my mind.

In real world though, I have to settle for less than ideal languages because of the batteries. Java has batteries and so does Python. If I pick OCaml or some really weird Scheme implementation, then I get no batteries to play with. I don't want to hunt all over the net for .01 version libraries just so I can make a GUI or read/write database.

Leo Lipelis

Posts: 111
Nickname: aeoo
Registered: Apr, 2006

Re: A Type System is a Set of Tests Posted: Apr 19, 2006 3:21 PM
Reply to this message Reply
> > My point is static type usually buys you something, but
> > sometimes that something isn't worth as much as it
> costs.
> > Which is why I think static type information is
> something
> > g that should be incrementally added to a program as it
> is
> > increasingly well understood.
>
> Consider something that static type information buys us
> more precise refactoring

Please point me to a study that substantiates this.

Erik Engbrecht

Posts: 210
Nickname: eengbrec
Registered: Apr, 2006

Re: A Type System is a Set of Tests Posted: Apr 19, 2006 3:48 PM
Reply to this message Reply
> > My point is static type usually buys you something, but
> > sometimes that something isn't worth as much as it
> costs.
> > Which is why I think static type information is
> something
> > g that should be incrementally added to a program as it
> is
> > increasingly well understood.
>
> Consider something that static type information buys us
> more precise refactoring and something that static
> type checking buys us consistency checking - it
> seems like those things will be valuable whenever we
> change the code.
>
> Just as the benefits of unit tests are available as soon
> as we begin a program, the benefits of static type
> information are available as soon as we begin a program.

Just to be clear, I think the effort of cleanly specifying my own types is what takes too much effort. When I'm interacting with a library or just someone else's code, I really appreciate static typing.

When I'm working in Java, I usually start with UML. When I'm working in Python, I usually start with a scribble and then just start coding. Python is closer to the free-flow of my mind.

The problem is the free-flow of my mind isn't production ready, so defining and clean set of classes/interfaces makes me work the kinks in my model out.

I just want to do it all in one language.

Isaac Gouy

Posts: 527
Nickname: igouy
Registered: Jul, 2003

Re: A Type System is a Set of Tests Posted: Apr 19, 2006 3:56 PM
Reply to this message Reply
> When I'm working in Java, I usually start with UML. When
> I'm working in Python, I usually start with a scribble and
> then just start coding. Python is closer to the free-flow
> of my mind.

Just to be clear - is the work in Python similar in scale and purpose to the work in Java?

Isaac Gouy

Posts: 527
Nickname: igouy
Registered: Jul, 2003

Re: A Type System is a Set of Tests Posted: Apr 19, 2006 4:11 PM
Reply to this message Reply
Leo Lipelis wrote
> > Consider something that static type information buys us
> > more precise refactoring
>
> Please point me to a study that substantiates this.

Think about the definition of a method signature in say Java, and the definition of a method selector in say Smalltalk, and then wonder how precisely we are able to identify method call sites with that information. (Or just download the tools and try them.)

Isaac Gouy

Posts: 527
Nickname: igouy
Registered: Jul, 2003

Scheme soft typing Posted: Apr 19, 2006 4:16 PM
Reply to this message Reply
Leo Lipelis wrote
> If I could have Scheme with type inference a la OCaml, that
> might be an ideal language to my mind.

Perhaps you're looking for Scheme soft typing.
http://www.google.com/search?hl=en&q=scheme+soft+typing&btnG=Google+Search

Leo Lipelis

Posts: 111
Nickname: aeoo
Registered: Apr, 2006

Re: A Type System is a Set of Tests Posted: Apr 19, 2006 5:56 PM
Reply to this message Reply
> my own types is what takes too much effort. When I'm
> interacting with a library or just someone else's code, I
> really appreciate static typing.

I'm in complete agreement here with you. :) If it is at all possible to solve this issue without imposing anything on the developer (such as writing their own type plugin, and/or maintaining a separate set of type files), wouldn't that be great?

I think maybe the best place to solve this is not even in the interpreter or compiler. It's a job for a library (module in python).

Leo Lipelis

Posts: 111
Nickname: aeoo
Registered: Apr, 2006

Re: A Type System is a Set of Tests Posted: Apr 19, 2006 7:01 PM
Reply to this message Reply
> my own types is what takes too much effort. When I'm
> interacting with a library or just someone else's code, I
> really appreciate static typing.

Agreed. I don't think we can solve this problem with a pluggable type system + type files. Nor can this problem be solved by a test suite.

This is a documentation + IDE problem, and I think it's best solved by a module that can do static code analysis (like pychecker, but more sophisticated -- it will need to be able to infer types).

IDE may use such a module to guess what the object types are.

For example you are typing

library_obj.undocumented_method(

Ok, in the 3rd party source code undocumented_method looks like this:

def undocumented_method(param1, param2): blah blah

Ok, so it's not helpful, right? What is param1? What is param2? This sucks. How do I feed the right arguments to this thing? Those are the questions that pop in my mind.

The code scanner/type inferer module can then be used by IDE to offer some reasonably good guesses for what these objects may be by looking inside undocumented_method to see what methods and fields are used and comparing those against the database of types that would be bulit up by scanning the code. So, the scanner will know that you're trying to quack param1 inside undocumented_method. Then it will look to see what can possibly quack. Aha.. it finds a few ducks. Then in IDE it tells you about these ducks in a popup/tooltip, so you know what to feed it.

This was an actual issue I faced once in Python. I got a lib and didn't know what parameters were expected due to insufficient docs.

Also you may want IDE to warn you if you are trying to quack something that doesn't quack. I believe pychecker can do this today.

You may want to know return types of methods. A code scanner should be able to give you a reasonable list, which can then appear in an IDE popup/tooltip.

Do I understand correctly? So basically we don't want to quack something that doesn't quack (and really this kind of bug shows up pretty fast at run time, when you exercise the code path). But more importantly we want to know what arguments can we feed to a method and what can we expect back. That's the job for a code scanner/type inferrer.

So if 3rd party lib has a method like

def foo(a, b): return a+b

the scanner will compile a list of method invocations on a and b. b has none. a has __add__. A list of classes that supports __add__ might be unreasonably large, so instead just show what the anonymous implicit interface is, which is just a single method of __add__.

If 3rd party foo method is like this:

def foo(a):
a.quack();
a.walk();
a.fly();
a.eatFish();

Then IDE has a choice.. it can display quack/walk/fly/eatFish methods as an anonymous implicit interface in a tooltip, or even better, it can do a match against the database of all known types, which it was able to infer. In Python most types should have reasonable names too, because they are mostly user defined classes. In other languages you may not have the names to associate with those inferred types. For Python though, it should be possible to determine a reasable list of qualified ducks and hint you about it in an IDE. Also IDE should be able to give you some good hints about what's coming out. Usually it's going to be a single type. If 3rd party did something like this:

def foo(a):
if (a == 1): return One();
if (a == 2): return Two();
...

Then you can get a list inside a tooltip that includes One as possible return type and Two and so on.

It might be hard to implement a 100% solution for this, but I believe an 80% solution should be doable. We already have pychecker. Python IDEs can already give you a lot of hints even today.

Guessing method return types and parameters should be possible. Gived a module to do it, pydoc can use that info as well as IDE, etc.

For example:
http://pydoc.org/2.4.1/MimeWriter.html#MimeWriter-addheader

What type is key? I can guess that it's a string, but type inferrer can give you a much more educated guess. Right? Is that the main issue?

Leo Lipelis

Posts: 111
Nickname: aeoo
Registered: Apr, 2006

Re: A Type System is a Set of Tests Posted: Apr 19, 2006 7:46 PM
Reply to this message Reply
Look, someone already did most of the work, it looks like:

http://codespeak.net/pypy/dist/pypy/doc/architecture.html#rpython-the-flow-object-space-and-translation

I didn't look too much into this, but I think it should be possible to use pypy in an IDE and pydoc to generate some really useful type hints/docs.

At least pypy should have a parser for python code that spits out an AST. So, it's conceivable to then use that information to try to infer types.

Flat View: This topic has 73 replies on 5 pages [ « | 1  2  3  4  5 | » ]
Topic: A Type System is a Set of Tests Previous Topic   Next Topic Topic: Thinking in C, Beta 3

Sponsored Links



Google
  Web Artima.com   

Copyright © 1996-2019 Artima, Inc. All Rights Reserved. - Privacy Policy - Terms of Use