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

[Zoltan Somogyi]

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.

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

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.

- Replace the existing MR_ti_var_arity_typeinfos field
  with a new array of MR_Words, the first N of which would contain
  MR_TypeInfos, and the next N would contain MR_ModeInfos.

- Replace the existing MR_ti_var_aritity_typeinfos field
  with a new array of N MR_TypeModeInfos, each of which
  is a structure containing one MR_TypeInfo and one MR_ModeInfo.

I don't remember whether we have anyplace in the runtime,
in the accurate gc code or in debugger that would need the type
information in the form of a dense array of MR_TypeInfos. If we don't,
or if we could rewrite any such code without problems, then the third
approach is preferably. If we can't do that, then the choice is between
the first two approaches. The first preserves as much type safety
as C allows, but the second requires fewer memory allocations
and has better locality.

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.


Zoltan.