[m-rev.] for review: subtypes

[Mark Brown]

On Wed, Jan 8, 2014 at 5:27 PM, Peter Wang <novalazy at gmail.com> wrote:
> On Tue, 7 Jan 2014 20:15:05 +1100, Mark Brown <mark at mercurylang.org> wrote:
>> On Tue, Jan 7, 2014 at 6:23 PM, Peter Wang <novalazy at gmail.com> wrote:
>> > On Tue, 7 Jan 2014 17:08:06 +1100, Mark Brown <mark at mercurylang.org> wrote:
>> >> > 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?
>>
>> No, I don't think it can. At least, I'm not sure what would go in the
>> interface files.
>>
>> If the inst information is not passed on to importing modules, then
>> they could indeed subvert the mode system using exactly the technique
>> that you mention below.
>
> I think I understand.  So importing modules wouldn't work with 'ground'
> cord values, but with the inferred inst because the cord type refers to
> a subtype.  The inferred inst is part of the cord module's interface.
> A predicate argument with type cord(T) and mode 'in' is treated as
> 'inferred_inst >> inferred_inst', and mode 'out' is treated as
> 'free >> inferred_inst'.
>

Exactly.

To put things another way, in the alternative design a type can be
turned into a (type, inst) pair. We can't abstractly export that
because the Mercury implementation doesn't support abstractly exported
insts yet.

It's worth pointing out that the design I chose is conservative, in
the sense that it reports an error in these cases. So in future, if
abstractly exported insts are implemented, we would be able to move to
the alternative design without breaking any existing programs.

>
> I was imagining that importing modules would still work with 'ground'
> cord(T) values, so the module interface remains unchanged.  Where the
> compiler can see a type declaration referring to subtypes, it can use
> that information to infer more precise insts for functor arguments,
> e.g. deconstruction
>
>     % C is ground
>     C = cord.list(L)
>     % C is bound(list(bound([ground | ground])))
>     % L is bound([ground | ground])

I think it is just constructing dynamically that is a problem.

Cheers,
Mark.