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/
pgp5buvcnk4pn.pgp
Description: PGP signature
