Home » forums » LtU Forum

A Usability question: Too much typing?

I like typing, and I see lots of things about programs that could perhaps stand to be typed that aren't. For example, I'd like a type that says if a call is (well, expected to be at any rate) synchronous or not (and then some way of using that information to catch "i assumed..." bugs).

Assuming there is a large raft of concepts that could be turned into useful types and incorporated into a language, how does one prevent the typing annotation (either manually entered or, preferably, automatically derived as much as possible) from being too much of a burden - visually in the source code, if nothing else?

I guess things like annotations or JML are an example of one way to format it all: have laundry lists at the top of the function definition. Having some (multiple) inheritance system might work, although then you are in the painful world of sorting through the hierarchy to figure out what your particular concrete item really is.

By raould at 2006-12-21 18:34 | LtU Forum | previous forum topic | next forum topic | other blogs | 6379 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Fundamental Design Parameter

If you check out the slide presentation discussed previously, you will see that this is a well-known trade-off in type system design.

To quote: "The more interesting your types get, the less fun it is to write them down!"

By Marc Hamann at Thu, 2006-12-21 19:26 | login or register to post comments

Formalism vs. UI

Thanks for the link.

Agreed that it gets (self-evidently) complicated. Perhaps it becomes less about language design and more about the tools that come with that language?

Posit that one goes for some big type DAG, understanding it - like understanding a big OO code base with even a bit of inheritance - quickly becomes difficult because one is manually paging around through dijoint ASCII. I'd like a way to gain power through stronger typing, but not break the user's back in the process.

(It is always sort of frustrating to think about how little we have in the way of really good and reall common tools for handling complexity.)

By raould at Thu, 2006-12-21 20:55 | login or register to post comments

I don't really agree with

I don't really agree with comments like "visually in the source code, if nothing else". I used to be enamoured with ML's type inference and lack of explicit type annotations, but these days I'm not so much.

The basic problem is that in a non-trivial project, code is there to be read as much as it is to be written. In order to understand a program you typically need to know the types of things. The type inference algorithm for Hindley-Milner is hard (doubly exponential and provably can't be improved upon I think?), and you're basically forcing the reader to run that in their head (this is mitigated by a good IDE or prompt, but they still need to take the trouble to look up the type). Explicit type annotations don't take up that much room and have significant readability advantages, at the expense of putting a small burden of commenting on the writer.

I guess this is dual to the old "Why write unit tests to check these things when the type system can prove it for you?": "Why write comments to explain this aspect of the code when the type annotations can do it for you?"

And of course if you move to more complicated type systems, like dependently typed ones or ML-sub, the situation with type inference gets even worse.

By David R. MacIver at Fri, 2006-12-22 09:10 | login or register to post comments

And of course if you move

"And of course if you move to more complicated type systems, like dependently typed ones or ML-sub, the situation with type inference gets even worse."

But the verbosity problem gets worse as well. Optional and incomplete typing annotations looks to be the right tradeoff to me. Some kind of tool support to show different kinds of typing information seems like a good idea as well. Types could be both inferred and shown inline with the source.

By Matt M at Fri, 2006-12-22 13:11 | login or register to post comments

brevity

This can be seen as related to the current subdiscussion on The drive to brevity.

I see your point about running Hindley-Milner in one's head -- this applies even more in a dynamically-typed language!

As I mentioned there, using more sophisticated typesetting a la TeX (TeXmacs) and literate programming could make this more pleasant.

raould, do you have examples of actual code, or pseudocode, you wish were more succinct?

By dbfaken at Fri, 2006-12-22 16:26 | login or register to post comments

Yes, everything I have to

Yes, everything I have to say against type inference should be taken as read to apply to dynamic typing with extra helpings. I'm firmly in the static typing camp. (I'm not really in the anti type inference camp. I can definitely see the benefits, I just have misgivings).

I'll take a look at the links. Thanks.

By David R. MacIver at Fri, 2006-12-22 16:40 | login or register to post comments

Agreed

(If I understood your comment right.) I've always found it sad that languages with automatic type inference use that power only for writers, not for readers. I absolutely want the ability to show the inferred types somehow.

By raould at Fri, 2006-12-22 21:23 | login or register to post comments

If you'll pardon the

If you'll pardon the somewhat glib response, I don't think we have verbosity problem. I think we have a verbosity *solution* to the lack of readability problem. ;-)

I just don't think that type inference is very viable for type systems in which the types are less disjoint than in Hindley-Milner. Dynamic dispatch and overloading particularly hurt it.

Let's take the classic stupid example. Camera and Gun types.

Each has a function shoot.

I define a function bangBang(x) { shoot(x); shoot(x) }

What should the type of bangBang be?

The compiler could create a type class or kind combining Camera and Gun, say 'shootable', but why should it? They're really not at all related. They just happen to have a method name in common, and littering the world with an abundance of unneeded type classes is hardly cutting down on verbosity.

It's pretty easy to come up with other similar examples.

Of course, type inference is still possible for a largeish subset of the language. But it's not going to solve the verbosity problem because the areas with the increased verbosity that worries you are exactly the areas the type inference is no longer going to work in. Further this means that the look of the code is going to be awfully inconsistent, with type declarations being present or not seemingly at random.

A better place for type inference is probably entirely in the tool support. Types which can be inferred are inserted for you automatically in the function definitions (I don't just mean displayed - they automatically get inserted as part of the code). Type annotations which can't simply be inferred will give you a pretty red underline saying "I can't infer this type. Please tell me what it is".

On an idle note, I've just had a really cool idea. Why doesn't the IDE colour code variables based on their type? That would help readability matters a lot and definitely allow one to see at a glance what type something was, even if its type declaration was many lines back. :-) (Only half in jest).

By David R. MacIver at Fri, 2006-12-22 16:37 | login or register to post comments

That is basically the core

That is basically the core of my comment, yes. Given a good display mechanism for automatic type inference (ideally one that elegantly integrates with the case where you do need the explicit type annotations, which is why I suggested the system adding them to the code directly), I would withdraw all objections to type inference and consider it an awesome tool I would dearly love to have. :-)

By David R. MacIver at Sat, 2006-12-23 09:55 | login or register to post comments

If you insert the inferred

If you insert the inferred type into the code, then what are the rules for updating the type when the value being typed changes? If we're talking about plain text, then it can't really depend on whether the type was inferred or an explicit annotation, right?

I'd like to see explicit partial type annotations, with tool support to display various inferred types.

By Matt M at Sat, 2006-12-23 17:24 | login or register to post comments