Okay. This hypothesis is wrong by counter-example:
(define (f g)
(pure (g)))
f: (fn ((pure fn () 'a)) 'a)
So there *are* cases where we see a requirement that an input argument
function must be pure when the calling function is impure.
The reverse case can also happen. While there is no corresponding
expression
(impure e)
it is possible to write something like
(define m-f: (mutable (impure fn ('a) 'b)))
(define (f g)
(set! m-f g))
It isn't immediately obvious (to me) whether a pure function can always
be provided where an impure function is expected. This is actually the
issue that got me started on this whole rat-hole.
shap
On Wed, 2008-08-06 at 17:12 -0400, Jonathan S. Shapiro wrote:
> There provisionally appear to be no correct typings in which an impure
> function can be required as a function type, except as a consequence of
> programmer mis-statement.
>
> The reason is that the pure/impure distinction is a purely
> unidirectional constraint. A procedure that mutates something is clearly
> liegal in pure context, but a procedure that *fails* to mutate something
> is legal in both pure and impure contexts. That is: the effect
> annotation is a restriction on legal contexts of application.
>
> 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.
>
> Further: there is no scenario in which an impure procedure can become
> impure as a consequence of applying a pure procedure.
>
>
> Collectively, these statements seem to suggest that an impure procedure
> can *always* be passed where a pure procedure is expected, *provided*
> the expression evaluation is not occurring in a pure computation
> context.
>
>
> This is moderately puzzling, because we seem to be escaping
> contravariance here.
>
>
> Why?
>
> _______________________________________________
> bitc-dev mailing list
> [email protected]
> http://www.coyotos.org/mailman/listinfo/bitc-dev
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
