Complete type inferencing

[Autrijus Tang]

On Fri, Jul 29, 2005 at 04:59:21AM +0800, Autrijus Tang wrote:
> However, my intuition is that a soft-typed system, with clearly defined
> dynamic parts translated to runtime coerce and dependent types, that can
> work exactly as Perl 5 did at first, but provide sensible inferencing
> and compile-time diagnostics as you gradually provide annotations, is
> really the way forward.

Several people replied off-list to point out the SBCL/CMUCL system does
inferencing and static+runtime type tagging for Common Lisp.  After
playing with it a bit, it seems that "soft typing" does not naturally
describe my initial intuition, as it never rejects any programs.
When types cannot be inferred, it merely inserts runtime assertions.

What I'm designing is a system that can decide on one of five classes of
judgements for each PIL term:

0. Untyped

    As in Perl 5, nothing is done for $x or the call to $x.close.
    Runtime failures are never detected until the actual call is made.

        sub f (Any $x) { $x.close }
        f(42);

1. Asserted

    The usual case for Perl 6 functions, due to its default "Item"
    signature for parameters.  In the example below, I assume that ::* cannot
    be changed freely to do away with ::*IO at runtime.  (If it could, then
    assertions won't be of much use in general.)

        sub f (IO $x) { $x.close }
        f(open('/etc/passwd'));

    As both &f and &open may be rebound at runtime, we cannot guarantee that
    this will not go wrong.  However, we can insert an runtime assertion for $x
    in &f's scope, so we can avoid doing the same assertion in &*IO::close
    again.  If IO is declared as final, then &*IO::close can also be resolved
    statically.

2. Well-typed

    This term's type is provably sound, and can be optimized at will
    without any runtime checks.  An example:

        {
            my sub f (IO $x) { $x.close }
            my sub g () returns IO { open('/etc/passwd') }
            f(g());
        }

    Here the call to &f and $x.close doesn't need assertions, as &g's return
    type took care of it.  Under "use optimized", many more terms can be
    resolved statically and checked in this manner.

3. Warning

    Under certain circumstances, this term's type can be shown to be unsound,
    but we cannot prove statically that this will come to pass:

        my sub f (IO $x) { $x.close }
        my sub identity ($y) returns IO|Str { $y }
        f(identity("/etc/passwd"));

    Here the call to &identity masked a potential type incompatibility.
    We know that if the IO half of the junctive type is chosen then it
    will typecheck; on the other hand, nothing in &identity or $y tells
    whether it will return IO or Str.  Hence we can raise a warning that
    says "this call can potentially go wrong had it returned Str".

4. Error

    This is a type error:

        my sub f (IO $x) { $x.close }
        f("/etc/passwd");

    Note that this can still be made to work at runtime by introducing
    &coerce:<as> from Str to IO, or make Str a subtype of IO.  Therefore
    in the absence of optimization hints of "closed" for Str and "final"
    for IO, the compiler should only raise a severe warning, that says
    "if you don't do something, this will fail at runtime".

    However, if the user had provided the neccessary optimization hints: 

        use optimize :classes< close finalize >;
        my sub f (IO $x) { $x.close }
        f("/etc/passwd");

    Then there is no way it could have worked, and the compiler should
    reject this program.

Interested readers can consult Manfred Widera's similar work for Scheme,
in his "Complete Type Inference in Functional Programming" paper.

Feedback, preferably on-list, are most welcome. :-)

Thanks,
/Autrijus/

pgpmOuOsKeqPW.pgp
Description: PGP signature