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
