RE: dynamic vs. static typing

["Anton van Straaten" <address@hidden>]

John Clements wrote
> On Nov 26, 2003, at 12:16 PM, Anton van Straaten wrote:
> > Is there anything more specific at work in the type inferencing
> > case that makes more meaningful errors more difficult (or
> > impossible)?
>
> Only the obvious one; rather than checking a type that you
> (the programmer) have written, the type-checker is checking
> types that it has inferred from (possibly distant) "clues"
> that you have provided.  I'll venture to guess that anyone
> who's written ML code has both blessed its type system for
> catching bugs and cursed profusely while trying to figure
> out WHY the type system thinks that 'x' is supposed to be
> an int when it's so OBVIOUSLY of type 'int->string'

ML suffers from other problems which arise at least partly from its
ambitious syntax.  Its syntax is wonderfully terse, but there seems to be a
price for that - dumb mistakes are punished.  Let's say I leave out a bar
between clauses in a function definition, in SML/NJ:

  fun reverse [] = []
      reverse (x::xs) = reverse xs @ [x];

Loading the above from a file called "errortest.sml" produces this:

  errortest.sml:2.36 Error: unbound variable or constructor: x
  errortest.sml:2.30-2.32 Error: unbound variable or constructor: xs
  errortest.sml:2.16-2.18 Error: unbound variable or constructor: xs
  errortest.sml:2.13 Error: unbound variable or constructor: x
  errortest.sml:1.18-2.38 Error: operator is not a function [tycon mismatch]
    operator: 'Z list
    in expression:
      nil reverse
  errortest.sml:1.1-2.38 Error: right-hand-side of clause doesn't agree with
function result type [tycon mismatch]
    expression:  bool
    result type:  _ list
    in declaration:
      reverse = (fn nil => <exp> <exp> = <exp> @ <exp>)

It's sort of amusing to see what is effectively a syntax error being cast in
terms of the type system.  Many languages with more traditional, redundant
syntax could give a much more concise error, simply pointing to the exact
character location where the problem is, because the sequence "... = []
reverse ..." would be syntactically invalid (a function name following a
data value, without some kind of delimiter).

Following my layering argument, perhaps I should be advocating "static
syntax checking", i.e. more comprehensive syntax checks which run prior to
type analysis, capable of detecting more errors at the syntax level (which
of course requires a more redundant syntax).

I seriously do believe that for these type systems or variants of them to
gain wider adoption, issues like these will have to be better addressed.
(Are there any ST functional languages that do much better in these areas?)

> > With highly abstract code, it's often possible to do a better
> > job of error reporting by providing additional information
> > when specializing the code.  I suppose one type system
> > equivalent would simply be to provide explicit annotations,
> > thus possibly losing both polymorphism and inferencing.
> > Are there better options?
>
> I don't see why explicit annotations should cost you polymorphism.

What I meant was what happens in an expression in which a variable has a
polymorphic type, where if you're forced to annotate it with an explicit
type, the expression becomes specific to that type.  You'd then need to
elaborate specific versions of that expression for every type you need to be
able to handle.

Anton