[bitc-dev] newbie questions

[Jonathan S. Shapiro]

On Mon, Jun 14, 2010 at 3:50 PM, Josh Bronson <josh.bronson at gmail.com> wrote:
>
> Jonathan S. Shapiro <shap at eros-os.org> wrote:
> > On Sun, Apr 4, 2010 at 1:49 AM, Elias Gabriel Amaral da Silva <
> > tolkiendili at gmail.com> wrote:
> >
> > Quite some time ago, we discussed a three-level effect system:
> >
> >    pure < noassign < (general)
> >
> > The problem with this is that it becomes depressingly intrusive. Even though
> > a total ordering on the effect is maintained, the fact that there are three
> > values means that the compiler cannot locally solve the inequality in many
> > more cases. The effect of this is to make both the effect variables and the
> > inequalities visible to the developer.
> >
> > To illustrate the issue, consider the NOALLOC effect type. In most cases you
> > won't see any effect variable associated with this effect, because the
> > compiler can "solve" the effect inequality locally. It only shows up when
> > you have something like MAP, whose effect depends on the passed procedure.
> > So NOALLOC is a "friendly" effect - it doesn't introduce confusion for
> > inexperienced developers.
>
> Doesn't the same problem occur with other (non-effect) types?


Only in the presence of inferred subtypes. In the absence of that
feature, there are no inequality relationships in the rest of the type
system, and consequently this user-visible complexity doesn't arise.

>
> The
> output type of a MAP function, for example, is "a list of the same
> type as the output of the passed function." That can be inferred
> without any special action on the part of the programmer, correct?

Not in the presence of a three-level inequality. What can be inferred
is that the output effect type of map is something that is at least as
effectful as the passed procedure. Because there are three levels, we
can't presumptively collapse that down to an equality relationship.


>
> > The three-valued purity effect tends to be less friendly, because the effect
> > variable shows up more often. This is true mainly because you'll get
> > MAP-like things where the calling procedure is noassign, but the effect of
> > the called procedure is unknown. So the effect of the calling procedure is
> > "the effect of whatever I call, but not less than NOASSIGN".
> > In one sense, this is no worse than MAP, because there is still just one
> > effect variable. But now there is a visible constraint as well.
>
> Where is this constraint visible? Why couldn't just part of the MAP
> type (the effect type) be inferred?

It is visible at the type of MAP, and therefore tends to become
visible as a constraint on everything that calls map. It is the
visibility of the inequality that is the impediment to the user.

>
> I like the idea of using imports as an analogy for effect types. A
> procedure can import multiple modules, along with all of their
> submodules. Modules contain other procedures, which are the basis for
> effects. In this case, you have three modules: pure, noassign, and
> general. The general module is a submodule of noassign, which is a
> submodule of pure. The type of MAP can now be restated as a tuple:
> "(NOASSIGN, whatever the value of the passed function is)"

Unfortunately, effects aren't scoped this way, and probably cannot be.

>
> And if you're willing to accept this idea, why stop with three effect
> types? Why not have all of the procedures called by a method
> constitute its effect type?


Because in a higher-order language, it isn't that simple, and also
because we aren't interested in what procedures are called, but what
their effect on the system state might be.

> And I don't see how a programmer would ever have to
> worry about declaring effect types (i.e. explicitly exporting modules)
> unless he knew what he was doing.

They need to be declared at module boundaries in order for separate
compilation to work, or a default needs to be assumed and enforced on
both sides of the module boundary.1

> Then you could add the same type of metainformation to describe
> machine code and design a secure operating system without any
> virtualization or context switching...

Definitely not going there.


shap