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

[Mark Brown]

On Thu, Dec 3, 2015 at 3:13 AM, Mark Brown <mark at mercurylang.org> wrote:
> 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.

A language feature that I'd like to propose illustrates the problem.

The feature would be to allow pred and func type expressions to also
include inst information, in much the same way that combined pred/mode
declarations do. For example, you could write code like:

    :- type job == (pred(result::out, io::di, io::uo) is det).
    :- type command ---> job(job).

The mode checker would be able to use the information from the type to
check whether calls are safe. So in the following code the higher
order call 'Pred(Result, !IO)' is mode correct because the necessary
information is available in the type of Pred.

    :- pred run(command::in, io::di, io::uo) is det.

    run(job(Pred), !IO) :-
        Pred(Result, !IO),
        handle_result(Result, !IO).

Values of the command type could be stored in generic data structures,
passed through thread.channel, and that sort of thing.

To do this currently in Mercury, without writing an unsafe cast, you
write something like:

    :- type job == pred(result, io, io).
    :- inst job == (pred(out, di, uo) is det).
    :- type command ---> job(job).
    :- inst command ---> job(job).

    :- pred run(command::in(command), io::di, io::uo) is det.
    ....

To use this with generic data structures requires constrained inst
vars, otherwise the necessary inst information is lost.

As for the problem, for higher order values construct/3 is not an
issue. But the problem with dynamic_cast/2 is that, while there is
RTTI available, there is no run time inst information with which it
can check the value has the right inst.

Dynamic cast has the following signature:

    :- pred dynamic_cast(T1::in, T2::out) is semidet.

Say there was another type defined as follows

    :- type special_job == (pred(result::out(special_result), io::di,
io::uo) is det).

so it's the same as job except the result argument has to be a
special_result. Then say we called dynamic_cast/2 with T1 = job and T2
= special_job. It ought to fail because T1 doesn't match T2, but it
succeeds because the typeinfos for T1 and T2 are the same. If the
implementation of dynamic_cast/2 is to be correct, then the mode
analyser needs to rule out calling it with T2 being a type with extra
information.

So how does the mode analyser rules out these calls while still
allowing calls to, say, list.map, where the extra information is okay?

Anyone have any ideas?

Mark