Some thoughts on PIL

6 views
Skip to first unread message

Autrijus Tang

unread,
Jul 28, 2005, 4:59:21 PM7/28/05
to "TSa (Thomas Sandla�)", perl6-l...@perl.org, perl6-c...@perl.org
On Thu, Jul 28, 2005 at 06:31:34PM +0200, "TSa (Thomas Sandla�)" wrote:
> BTW, where can I read about PIL, other then in Parrot/Pugs svn?

(Cc'ing in P6C.)

The current type-indexed design of PIL is going away, because it is
closely tied to the PIR/Parrot model, to the disadvantage of our
Perl5/JavaScript backends. Also it does not capture any notion of
rank-n types, and relies on the VM for a semantics for container types,
which is prone to trouble.

In the past few weeks I've been reading up on F<:, Fw, CoC, vObj, as
well as intersectional and split types for object calculi, in the
hope of revamping PIL -- Pugs's new internal language -- that can
alleviate backend author's pain and improve type-directed translation.

Perl 6's uniqueness is that it relies on runtime-rebindable package
objects for its type system, but at the same time carries the vague
promise of partial static analysis for the part of the closed world via
toplevel `use optimize`. The semantic of type annotations remains
unresolved; I reflected this in the recent `the meaning of "returns"`
thread.

It would be far easier if we concede that Perl 6 is essentially untyped,
and all type annotations are merely storage hints, that will still
always require runtime coercion. This coincide with Parrot's current
idea of never checking subroutine parameter's PMC types (except for
MMD), and always resolve method calls as late as possible, exactly as
Perl 5 did.

Under that view, the only use of type annotation at compile time is
speeding up property/method lookup for typed variables, so they can be
looked up by number instead of names, provided new fields always go
toward the end. Other than that, they can only serve as runtime
assertions, leading to the curious effect that well-typed programs
can run slower than the unannotated counterpart.

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.

Under soft typing, Parrot's role would become a fast implementation for
the object space and primitives, but the soundness of large-scale
programs and the standard library will be provided by the compiler, not
the runtime. This plays well with Pugs's -- not neccessarily Perl 6's --
goal of keeping the language retargettable.

This may not be popular view, as evidented by the relative lack of
research and real-world interest to bridge the gap of static/dynamic
languages, so it would take a while to come up with a suitable formal
treatment. I'm currently trying to express this idea under the F<:
framework for the new PIL, and I'll keep p6c posted as it goes forward,
and cotinue to reflect design issues to p6l.

Thanks,
/Autrijus/

Autrijus Tang

unread,
Jul 29, 2005, 11:08:27 AM7/29/05
to perl6-l...@perl.org, perl6-c...@perl.org
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/

Autrijus Tang

unread,
Jul 29, 2005, 2:45:20 PM7/29/05
to "TSa (Thomas Sandla�)", Autrijus Tang, perl6-c...@perl.org
On Fri, Jul 29, 2005 at 06:36:45PM +0200, "TSa (Thomas Sandla�)" wrote:
> you wrote:
> >Interested readers can consult Manfred Widera's similar work for Scheme,
> >in his "Complete Type Inference in Functional Programming" paper.
>
> Uih, you call a 300 page book a paper? I'm impressed.

Well, it's his dissertation, and Dissertation.does(Paper), including
book-length ones. :-)

> If that is the thing you read between tramp stations here's one of my
> favorites which is the thesis of Vassily Litvinov. It's about CBP.
>
> http://www.cs.washington.edu/research/projects/cecil/www/Papers/vass-thesis.html

Yes, I'm aware of Theta's static where clauses, but Perl 6's where
clause is much more dynamic and almost always undecidable.

In Litvinov's paper, where clauses are determinisitic at compile time,
as a way to encode structural subtyping (aka duck typing). In Perl 6
pseudo-syntax, it would be something like this:

sub foo (
$obj where { .can(
name => 'bar',
signature => :(() returns Int),
) }
) returns Int {
$obj.bar();
}

It's a bit verbose, but I don't know if there is a way to express named
methods to .can succintly. A long name in .can(&bar:(() returns Int))
won't do, as &bar would have been a variable lookup.

=begin digression

As an aside, arguably we could have dropped the braces and write:

Any $obj where .can(...)

Except this is yet another violation of no-auto-bracing rule that can
result in ambiguous parses; I think it's a misfeature to allow

Str where /^[isnt⎪arent⎪amnot⎪aint]$/;

This is much more consistent:

Str where { /^[isnt⎪arent⎪amnot⎪aint]$/ };

=cut

The important difference is that the .can() call in Perl 6 would be a
runtime call. It has to be that way, because .can is not a special
form; it's just a normal method returning a boolean. If you really
want static treatment, that needs a special form:

sub foo (
$obj can bar:(() returns Int)
) returns Int {
$obj.bar();
}

It will allow constructs such as this:

my subtype Duck
has $.half_life
can doom:()
can quake:(() returns Wolfenstein);

# Automagically satisfied iff $obj's interface is compatible
$obj.does(Duck);

Such implicitly-declared Roles is certainly powerful, and we can apply
the same inferencing treatment as for nominal subtyping violations --
fatal error under closed/finalized, raise warning by default.

I think it's cute, and adds real power of row polymorphism to the
language, iff Perl 6 indeed adopts a compile-time inferencing engine.

> BTW, have we as a list considered approaching Universities for assistence?
> E.g. I regard Perl6 as a worthwhile research subject and/or platform.
> After all Manfred Widera's thesis was done at a German University.

It seems to me that to approach researchers for assistance, one need to
give a formal treatment of the language, or at least a specification
that can lead to unambiguous implementations. Which is why I'd like to
formalize the internal language (PIL), basic types and meta-object
protocol, after all... :-)

Thanks,
/Autrijus/

Autrijus Tang

unread,
Aug 2, 2005, 1:54:20 AM8/2/05
to Brad Bowman, Autrijus Tang, perl6language, perl6-c...@perl.org
On Tue, Aug 02, 2005 at 12:49:06PM +1000, Brad Bowman wrote:
> > 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.
>
> Could this be implemented optimistically, with disabled
> assertions which are enabled at runtime if either &f or &open
> are rebound?

Yes, it is conceivable to hoist assertions whereever possible, and
reactivate them if the earlier assertion no longer hold due to rebind.
I'll prototype it a bit and see if it works.

Thanks,
/Autrijus/

Reply all
Reply to author
Forward
0 new messages