On Wed, 2008-08-06 at 18:04 -0400, Swaroop Sridhar wrote:
> Jonathan S. Shapiro wrote:
> > Because of this, I suspect that we will never see "pure" inferred by the
> > type system. We have already seen that map ends up with an effect
> > variable, but things like
> >
> > (define always-return-unit (x)
> > ())
> >
> > will *also* end up with an effect variable, precisely because their
> > application is legal in either context.
>
> I don't think this is true. the function always-return-unit will have
> the type (fn pure ('a) ()). However, an application of this function
> is legal in both pure as well as impure contexts.
Per our phone discussion, I do not believe so. Think about how the
unification goes.
In
(define (f x)
(set! location x))
The unifier initially assigns f the type
('%e fn ('a) 'b)
the '%e eventually unifies with the effect of set!, which is:
(impure fn (by-ref (mutable 'a)) 'a)
leading to the conclusion that f is impure.
But the converse is not true. The ABSENCE of a set! in the body of f
does not cause '%e to converge to "pure". Off the top of my head, only
the presence of an explicit (pure e) form somewhere in the body of f
would have that effect, and then only if we had something like:
(define (f g)
(g) ;; effects of g unify with effects of f, and
(pure (g))) ;; g must be pure
The following certainly does NOT cause f to be pure:
(define (f g)
(pure (g)))
because effects do not unify across PURE.
As you have pointed out, if the effect variable survives unresolved at
the close of the defining form, and does not unify with any effect of
any argument or return type, then we can fix it to PURE without loss of
information. I'm actually inclined to think that this is a good thing to
do for documentation reasons, but making sure that we get this right is
moderately tricky.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
