Re: in defense of types

[Neel Krishnaswami <address@hidden>]

Matthias Felleisen writes:
> 
> Yes, Jeff, I have heard this before. Program understanding does not
> come from types alone. As for types, the story is wide open for
> powerful type systems (see ML).

What does the idiom "the story is wide open" mean?

At any rate, I can tell a story about a bug I discovered using
types. This Monday, I was writing some parser combinators. In my
implementation, a parser is a function that takes a stream and returns
a value (ie, has type 'a stream -> 'b). I wanted to write a combinator
"seq" that would take a parser and arguments identifying brackets and
separtor tokens, and would return a list of parser values. That is, it
would be a function with type:

  ('a stream -> 'b) -> open:'a -> sep:'a -> close:'a -> 'b list

When I wrote my first verion of this function, I saw that OCaml had
inferred a type of:

  ('a stream -> 'b) -> open:'c -> sep:'d -> close:'e-> 'b list

I immediately knew that since the type variables 'c, 'd and 'e didn't
show up in the parser or return types, that meant that the delimiters
were being ignored. (Testing confirmed this, and posting to Usenet led
to me discovering that the problem turned out to be due to my mis-
understanding some overly terse documentation of some somewhat grotty
syntax.)

Now, an interesting fact is that I would not have found this bug as
easily if I had written down a type declaration for my function,
because the typechecker would happily have restricted 'c, 'd and 'e to
be equal to 'a. This contradicts the usual dogma that declarations
help catch contradictions between intent and implementation. So when I
write ML code, I do my best to avoid declaring types anywhere, because
I want to see unexpected types. But when I was writing a lot of Dylan
code (which is dynamically typed, but permits declaring types for
variables), I declared types whenever I could. There, the declarations
helped me localize errors.

The difference in style is really striking, and I'm not sure what it
signfies. I speculate that the difference is due either to having type
inference available in ML and not Dylan, or to having polymorphic type
variables in ML's type system and not in Dylan's.


-- 
Neel Krishnaswami
neelk@alum.mit.edu