[m-rev.] for review: subtypes

[Peter Wang]

On Tue, 7 Jan 2014 17:08:06 +1100, Mark Brown <mark at mercurylang.org> wrote:
> 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.

Yes.

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

Got it.

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

In the alternative design, is that because you mean to export 'first'
and 'non_empty_cord(T)'?  If 'non_empty_cord(T)' is not exported, then
the type 'cord(T)' can still be abstractly exported, right?

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

Again in the alternative design, the compiler should reject any attempt
to construct the term `list([])'.  But is there anything to stop you
constructing it dynamically?

    TypeDesc = type_of(BadCord),
    find_functor(TypeDesc, "list", 1, Functor, _),
    Univ = construct(TypeDesc, Functor, [univ([] : list(int))]),
    univ_to_type(Univ, BadCord : cord(int)),

Peter