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

[Mark Brown]

On Mon, Nov 2, 2015 at 2:08 AM, Zoltan Somogyi
<zoltan.somogyi at runbox.com> wrote:
> I think that in the medium term, the best solution to this problem
> would be to take the answer to the fourth question out of insts
> and to put them into types instead. It would be an aspect of types
> that would have to checked during mode analysis, not type checking.
> This would complicate the relationship between the two analyses,
> which is why it wasn't done that way originally.

I don't think that's the entire reason. When subtype information is in
the inst you can give a smaller subtype in the final inst than in the
initial, which says something about which input values always fail in
that mode. Types can't express this because there is no separate
initial and final type, so putting the information in the type is
strictly less expressive.

This is not to say we must keep this expressiveness - I'm not aware of
the feature getting any significant use - just that people ought to be
aware of it.

> However, if it was
> done correctly, it would guarantee that the information cannot
> get lost. With that system, if you took a higher order value out
> of a term, its type would tell you its signature, even if the term
> was (at some intermediate point in time) polymorphic.
>
> Unfortunately, this proposal has been a "medium term solution"
> for way more than a decade now :-(

I posted one solution a couple of years ago, and also proposed an
alternative. This worked by using the existing
propagate_ctor_info_lazily code to push the relevant information from
the types to the mode checker.

If I understand what you're saying about the implementation, it is
that the "pullback" of the inst operations along this propagation
function should be implemented directly on the types where possible,
rather than creating a new inst as an intermediate data structure. So,
for a crude example, we know that ground(shared, none_or_default_func)
always matches itself even for function types, therefore it is
wasteful to expand both of these out to the default inst and then
check if the expanded versions match. I agree with this.

Regarding correctness, how are construct/3 and dynamic_cast/2 to be
handled? It would be unsafe for the universal quantifiers in their
signatures to range over all types, including subtypes, without some
way of checking that the output values really are in the type in
question. They would be okay if the output types were constrained to
be maximal, however.

Mark