[comp.lang.misc] Static type inference?

wilson@uicbert.eecs.uic.edu (Paul Wilson) (03/06/91)

sommar@enea.se (Erland Sommarskog) writes:

>Also sprach David Gudeman (gudeman@cs.arizona.edu):
>>There are several advantages to this.  First, it makes program
>>prototyping and developement much faster because declarations are
>>minimized.

>>Another advantage of runtime polymorphism is code generality.  You can
>>write generic procedures that work on many data types (as long as it
>>only makes use of operations that have definitions for all the data
>>types).  For example you can write a procedure to insert something in
>>a tree without knowing the type of the object: (Icon code)
>>...
>>The only operations on x are object comparison (<<<) and inserting
>>into a record, so the procedure is entirely generic.  (As an aside,

>Fine. I can do this in Ada and Eiffel. And assure at compile time, 
>that I don't pass incomparable or uninsertable types to the generic 
>routine.

There's another way.  You can have static type inference, as in ML,
if all you really want is generic routines without having to type
those pesky type declarations.  You get genericity and static typing
with only a little extra work on the part of the programmer, to
disambiguate types where the type-inference mechanism can't.
Whenever the type inference mechanism fails, you have to tell it
what you really meant. 

On the other hand, the ability to have run-time dynamic types is
important.  There are times when you really want a collection of
objects of different types.  But maybe the best compromise is to
use type-inferred static typing by default, and have a way of
specifiying real runtime polymorphism as well.   Most of the gain
without most of the pain.  (No, I don't have a proposal as to what
such a language ought to be like, in detail.  Others probably do, though.)

>>But in my experience this is a minor
>>problem, and the time spent looking for these errors is quite small
>>compared to the time that would have been spent writing strongly typed
>>declarations.

  I don't know about this.  For big and long-running programs, it's nice
to have your really stupid bugs statically detected rather than having
to actually run them, etc.  For medium-sized programs, maybe static type
inference can reduce the typing burden (in two senses :-) on the programmer 
enough to make it worthwhile.  Sometimes I think that having to specify
static vs. runtime polymorphism might be good for the clarity of thought
and expression that it encourages.

    -- PRW
-- 
Paul R. Wilson                         
Software Systems Laboratory               lab ph.: (312) 996-9216
U. of Illin. at C. EECS Dept. (M/C 154)   wilson@bert.eecs.uic.edu
Box 4348   Chicago,IL 60680 

bevan@cs.man.ac.uk (Stephen J Bevan) (03/06/91)

> On the other hand, the ability to have run-time dynamic types is
> important.  There are times when you really want a collection of
> objects of different types.  But maybe the best compromise is to
> use type-inferred static typing by default, and have a way of
> specifiying real runtime polymorphism as well.   Most of the gain
> without most of the pain.  (No, I don't have a proposal as to what
> such a language ought to be like, in detail.  Others probably do, though.)

From the little I know about FX, it seems this language gives you what
you want.  It's based on Scheme, but includes optional type
declarations.  Those that you don't define, the system infers.

For more information on FX :-

Report on FX-90 Programming Language
David K. Gifford, Pierre Jouvelot and Mark A. Sheldon
Programming Systems Research Group
Massachusetts Institute of Technology

Stephen J. Bevan		bevan@cs.man.ac.uk

strom@arnor.UUCP (Rob Strom) (03/07/91)

In article <1991Mar5.180306.1561@uicbert.eecs.uic.edu>, wilson@uicbert.eecs.uic.edu (Paul Wilson) writes:
|> sommar@enea.se (Erland Sommarskog) writes:
|> 
   [embedded quote from David Gudeman deleted]

|> >Fine. I can do this in Ada and Eiffel. And assure at compile time, 
|> >that I don't pass incomparable or uninsertable types to the generic 
|> >routine.
|> 
|> There's another way.  You can have static type inference, as in ML,
|> if all you really want is generic routines without having to type
|> those pesky type declarations.  You get genericity and static typing
|> with only a little extra work on the part of the programmer, to
|> disambiguate types where the type-inference mechanism can't.
|> Whenever the type inference mechanism fails, you have to tell it
|> what you really meant. 
|> 
|> On the other hand, the ability to have run-time dynamic types is
|> important.  There are times when you really want a collection of
|> objects of different types.  But maybe the best compromise is to
|> use type-inferred static typing by default, and have a way of
|> specifiying real runtime polymorphism as well.   Most of the gain
|> without most of the pain.  (No, I don't have a proposal as to what
|> such a language ought to be like, in detail.  Others probably do, though.)

That is the approach we took in Hermes.  Most of the time, the programmer
intends that a variable always contain values of
the same specific type.   Occasionally, it is desirable to
have a collection of objects of different types.  Hermes
provides type constructors and a mechanism for explicit type 
definition to handle the typical case in which
the type is statically invariant.  It provides an additional type, "polymorph", 
for the cases when data of different types are to be handled by a common
piece of code.  Data of any type can be "wrapped" into a polymorph,
and then cast back into a variable of the original type by being
"unwrapped".  (Of course, at this time it is checked that the polymorph
in fact has the expected type.)  

 
|> 
|> >>But in my experience this is a minor
|> >>problem, and the time spent looking for these errors is quite small
|> >>compared to the time that would have been spent writing strongly typed
|> >>declarations.
|> 
|>   I don't know about this.  For big and long-running programs, it's nice
|> to have your really stupid bugs statically detected rather than having
|> to actually run them, etc.  For medium-sized programs, maybe static type
|> inference can reduce the typing burden (in two senses :-) on the programmer 
|> enough to make it worthwhile.  Sometimes I think that having to specify
|> static vs. runtime polymorphism might be good for the clarity of thought
|> and expression that it encourages.

In Hermes we take an intermediate position on declarations.  There is
a type inferencing mechanism.  The same rules used to perform type
checking can be used in certain cases to perform type inferencing when
the type is not known.  However, Hermes is biased towards the needs
of the writer of long-running programs.  It therefore requires more declarations
than would be necessary to satisfy the type inferencing mechanism.  In particular,
interfaces are required to be explicitly typed.  

The use of the "polymorph" type is independent of our position on declarations.
It's just another type which can be declared or inferred.  We do insist
that "wrap" and "unwrap" be explicitly coded, since our position is that
run-time type checking is the exception, not the rule.   In an environment
where almost everything is a polymorph and only a few things explicitly
typed, we might have made a different decision.

|> 
|>     -- PRW
|> -- 
|> Paul R. Wilson                         
|> Software Systems Laboratory               lab ph.: (312) 996-9216
|> U. of Illin. at C. EECS Dept. (M/C 154)   wilson@bert.eecs.uic.edu
|> Box 4348   Chicago,IL 60680 

-- 
Rob Strom, strom@ibm.com, (914) 784-7641
IBM Research, 30 Saw Mill River Road, P.O. Box 704, Yorktown Heights, NY  10958

jouvelot@brokaw.lcs.mit.edu (Pierre Jouvelot) (03/08/91)

In article <BEVAN.91Mar6084338@panda.cs.man.ac.uk> bevan@cs.man.ac.uk
(Stephen J Bevan) writes: 
>From the little I know about FX, it seems this language gives you what
>you want.  It's based on Scheme, but includes optional type
>declarations.  Those that you don't define, the system infers.
>
>For more information on FX :-
>
>Report on FX-90 Programming Language
>David K. Gifford, Pierre Jouvelot and Mark A. Sheldon
>Programming Systems Research Group
>Massachusetts Institute of Technology
>

I don't know how Stephen got a hold of this draft report, but we didn't
plan on distributing it until it is completed, which we expect to be
soon.

Nonetheless there are other published papers that are relevant to the
current FX design:

. O'Toole and Gifford paper in ACM PLDI'89, where it is shown how
  explicit and implicit polymorphism can be merged together.
. Sheldon and Gifford paper in ACM Lisp Conf'90, that describes the
  rationale behind the module system used in FX.
. Jouvelot and Gifford paper in ACM POPL'91, where effect reconstruction
  (or inference) is described.

And, of course, there is the old FX-87 Reference Manual, MIT/LCS TR-407
on which most of this work is built. Other papers have been written and
submitted to conferences, in which other aspects of effect systems are
investigated:

. Talpin and Jouvelot paper about inference of type, effect and regions
  in an ML-like language.
. Dornic, Jouvelot and Gifford paper about using effect system to
  estimate program complexity

... and more should come :-)

Pierre
--
. CRI, Ecole des Mines, Paris (France): jouvelot@ensmp.fr
. LCS, MIT, Cambridge (USA): jouvelot@brokaw.lcs.mit.edu