[bitc-dev] Use of pure functions in impure contexts

Swaroop Sridhar swaroop at cs.jhu.edu
Wed Aug 6 17:04:00 CDT 2008

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.

When we perform an application, the effect on the function is collected
as a result of the application. Pure contexts require that the maximum
of all collected effects be pure. Impure contexts have no such
restriction. So, the compiler can infer pure effect for
always-return-unit and still use it in a impure context. I think I am
missing/misunderstanding what you are asking here.

`map' has a effect variable since its effect depends on the purity of
the function that is its argument.

> Further: there is no scenario in which an impure procedure can become
> impure as a consequence of applying a pure procedure.

Did you mean ``impure procedure can become pure?''

> 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.

My understanding is that pure procedures can be passed when impure is
expected. If we must be able to pass either pure or impure, then,
the function type must have been polymorphic over purity.

> This is moderately puzzling, because we seem to be escaping
> contravariance here.

We are actually not escaping contravariance here. The rules are

  (fn pure (ta) tr) <: (fn impure (ta) tr)              [1]

    ta2 <: ta1             tr1 <: tr2
_____________________________________________          [2]
  (fn pure (ta1) tr1) <: (fn impure (ta2) tr2)

So, for f1,

f1: (fn `e ((fn impure (bool) bool)) int32)

At the time of application, we can provide f1 an actual argument whose
type is either (fn impure (bool) bool) or (fn pure (bool) bool),
due to rule [1].

However, in the case of

f2: (fn `e ((fn impure (fn impure (bool) bool) unit)) int32)

the actual argument of f2 can have type

(fn impure (fn impure (bool) bool) unit) or
(fn pure (fn impure (bool) bool) unit)

but not

(fn impure (fn pure (bool) bool) unit) ;; WRONG    or
(fn pure (fn pure (bool) bool) unit) ;; WRONG

due to rule [2].

Similarly, if we had

f3: (fn `e ((fn impure (fn pure (bool) bool) unit)) int32)

the actual arguments to f3 can have any of the following types

(fn impure (fn pure (bool) bool) unit)
(fn impure (fn impure (bool) bool) unit)
(fn pure (fn pure (bool) bool) unit)
(fn pure (fn impure (bool) bool) unit)

due to rule [2].


More information about the bitc-dev mailing list