[m-dev.] subtypes (was Re: [m-rev.] for review: don't allow nondefault mode functions in terms)

[Mark Brown]

On Thu, Dec 10, 2015 at 4:20 PM, Zoltan Somogyi
<zoltan.somogyi at runbox.com> wrote:
> On Wed, 9 Dec 2015 21:58:26 +1100, Mark Brown <mark at mercurylang.org> wrote:
>> I have started implementing the language feature as follows:
>>
>>  - A field is added to higher_order_type in mer_type to store any
>> pred_inst_info.
>>  - The extra field is ignored during type checking.
>>  - When mode checking a construction, if there is a pred_inst_info in
>> the type then the argument must match it (using pred_inst_matches).
>>  - When mode checking a deconstruction, if there is a pred_inst_info
>> in the type then propagate it into the argument inst.
>>
>> The implementation will need to use typed_ground insts to propagate
>> more deeply nested information, for a list of predicates for example,
>> but that is not yet done. There's plenty of other holes too - this is
>> a work-in-progress. The current diff is attached in case anyone is
>> interested, although it is not ready for review.
>
> I am not sure about whether the third point is the right thing to do,
> since I don't remember what pred_inst_matches does exactly,
> but the others seem right.

It's the same test used to decide whether passing a higher order term
to an ordinary call is safe.

>
>> The second example illustrates the problem. Construct/3 can in fact be
>> a problem even for higher order types, if some du type has a higher
>> order argument that is expected to match a particular mode, because
>> there is no way to check that the higher-order value inside the univ
>> matches this mode.
>
> There is no way, no mechnanism, to do that YET.
>
> The univ contains nothing but the value and its typeinfo. We can
> implement the needed mechanism in one of two logically equivalent ways:
> we can add a third field containing the mode information to the univ
> when the value it contains is higher order, or we can extend the
> type_infos for higher values themselves with mode information.
> The latter seems preferable.

Definitely. Since the code that actually calls the univ module may
itself be generic, the modeinfo would have to get there either inside
or alongside the typeinfo. It's not needed for most types, so inside
is much better than alongside.

>
> I think you would want to make higher order types stop using
> MR_VAR_ARITY_TYPEINFO_STRUCT, and start using a new type.
> This type would be similar, but would have room not just for
> a typeinfo for each argument, but also a mode.
>
> I see three ways to add the modes. All would require the invention
> of a new type, say MR_ModeInfo, for containing mode information.
> In the following, procedure has N args.
>
> - Add a new field containing a pointer to an array of N MR_ModeInfos.

I think this is the best way. It would save space to represent
commonly used modes, such as default functions, with a small constant,
and there could be a lot more sharing for modes than for types, for
example, a bunch of predicates with mode (pred(in, di, uo) is det)
which differ in the type of the first argument. A tagged pointer for
this field could distinguish between simple modes containing just
in/out/di/uo, which can be represented cheaply, and more complex
modes.

> The design of the MR_ModeInfo type will limit what modes
> the runtime system can reason about. It doesn't have to allow
> the expression of every mode that we currently support,
> since the current runtime allows the expression of NO modes at all.
> However, it would be nice if the reasoning it does allow were
> provably correct. On that score, even just in/out/di/uo would
> probably be useful often enough.

Yes, and in fact I need to keep this task as small and simple as
possible, or risk it not being completed at all. That's why it doesn't
deal with anything other than pred and func subtypes.

At minimum I want to:
- allow all existing programs to run as before
- ensure new programs never crash

For construct/3, it would be sufficient to store one bit of
information with the type constructor, or perhaps with each du
functor, that indicates whether there are any constraints on the
arguments at all. The implementation of construct/3 could throw an
exception if it sees this bit set. Since there are none of these
constraints in existing programs, the bit would never be set and
construct/3 would continue to behave as before. But programs that try
to dynamically construct one of the new types will be prevented from
doing so, thus avoiding crashes.

Dynamic_cast/2 is more of a problem. For safety, it would have to
throw an exception if given a non-default function, so it seems that
programs that rely on such a cast will no longer run as before. It's
not ideal, but it wouldn't affect very many existing programs, I
imagine.

Mark