[m-rev.] for review: subtypes

[Mark Brown]

Hi Peter,

On Tue, Jan 7, 2014 at 2:18 PM, Peter Wang <novalazy at gmail.com> wrote:
> On Mon, 6 Jan 2014 17:46:48 +1100, Mark Brown <mark at mercurylang.org> wrote:
>> Hi Peter,
>>
>> On Mon, Jan 6, 2014 at 2:19 PM, Peter Wang <novalazy at gmail.com> wrote:
>> > On Tue, 31 Dec 2013 05:05:15 +1100, Mark Brown <mark at mercurylang.org> wrote:
>> >> Hi everyone,
>> >>
>> >> I have had a shot at implementing something along the lines of the old
>> >> subtypes proposal. It is for review by anyone. The log message is
>> >> attached, and the diff can be found at
>> >>
>> >> https://github.com/markbrown/mercury/
>> >>
>> >> in the subtypes branch. Please note I am not currently subscribed to this list.
>> > ...
>> >>
>> >> Another design issue is that subtypes are currenly only allowed to be used
>> >> in pred and func declarations (including typeclass methods).  Alternative
>> >> designs could include:
>> >>
>> >> (1) Allowing subtypes to be used in ordinary type declarations, inferring a
>> >> ground inst for every type that refers, directly or indirectly, to a subtype.
>> >
>> > This seems a major restriction.
>>
>> Indeed, I hit it already in parsing_utils.
>>
>> Do you think the alternative is better? I mentioned some concerns
>> about it already, so I wanted feedback before looking further.
>
> I would find subtypes much more useful then.
>
> Could `cord' be written like this?
>
>     :- type cord(T)
>         --->    empty
>         ;       unit(T)
>         ;       list(nonempty_list(T))
>         ;       branch(nonempty_cord(T), nonempty_cord(T)).

That's the kind of thing I had in mind for the alternative design, but
is not what I have implemented.

In Mercury currently, you can express subtypes this way:

:- type cord(T)
    --->    empty
    ;       unit(T)
    ;       list(list(T))
    ;       branch(cord(T), cord(T)).

:- inst cord
    --->    empty
    ;       unit(ground)
    ;       list(non_empty_list)
    ;       branch(non_empty_cord, non_empty_cord).

:- inst non_empty_cord
    --->    unit(ground)
    ;       list(non_empty_list)
    ;       branch(non_empty_cord, non_empty_cord).

:- func first(cord(T)::in(non_empty_cord)) = (T::out) is det.

first(unit(X)) = X.
first(list([X | _])) = X.
first(branch(Cord, _)) = first(Cord).

Here's how I would do the same thing with the proposed subtype declarations:

:- type cord_base(T)
    --->    empty
    ;       unit(T)
    ;       list(list(T))
    ;       branch(cord(T), cord(T)).

:- inst cord ...  % as above

:- inst non_empty_cord ... % as above

:- subtype cord(T) < cord_base(T) :: cord.

:- subtype non_empty_cord(T) < cord_base(T) :: non_empty_cord.

:- func first(non_empty_cord(T)) = T.

In other words, we keep the same type and inst declarations, except
the type is renamed cord_base/1, and we add two subtype declarations
to connect the base type with each inst. With these subtype
declarations, the signature of first/1 can be written much more
easily.

Note that we don't write non_empty_cord(T) < cord(T), even though that
statement would notionally be true.

With the alternative design, the idea is that you could write something like:

:- type cord(T)
    --->    empty
    ;       unit(T)
    ;       list(non_empty_list(T))
    ;       branch(non_empty_cord(T), non_empty_cord(T)).

:- type non_empty_cord(T) < cord(T)
    --->    unit(T)
    ;       list(non_empty_list(T))
    ;       branch(non_empty_cord(T), non_empty_cord(T)).

:- func first(non_empty_cord(T)) = T.

This is easily the most concise version.

> What do you mean by "inferring a ground inst ..."?

In the alternative version we don't explicitly state the insts as we
do currently and in the proposed version. They still need to be
propagated into the modes prior to mode checking, though, so the
compiler would need to infer them some way. In the case of
non_empty_cord/1, that would involve joining together the implied inst
information from the body of the definition, and from the definition
of non_empty_list/1 (and checking that it matches cord/1).

> If I'm not mistaken, container types could not be abstract exported.

That's right. In none of these examples could the data structure be
abstractly exported, since Mercury does not support abstract insts.
The workaround in parsing_utils.m would still be needed.

In the first two versions, that roadblock would at least be more
obvious, since the insts are explicit.

>
>> >
>> > construct would be even more complicated, no doubt.
>>
>> The types in type_desc currently provide access to type information
>> only, not inst information. I wasn't planning to change that at all,
>> even in the alternative design, so construct, etc, won't be affected.
>
> construct should not be able to subvert the type declaration, though.

Can you give me an example of what you mean?

Cheers,
Mark.