[m-rev.] for review: subtypes

[Mark Brown]

On Mon, Jan 13, 2014 at 2:42 PM, Peter Wang <novalazy at gmail.com> wrote:
> On Sat, 11 Jan 2014 21:21:14 +1100, Mark Brown <mark at mercurylang.org> wrote:
>> On Thu, Jan 9, 2014 at 5:31 PM, Peter Wang <novalazy at gmail.com> wrote:
>> > On Thu, 9 Jan 2014 16:35:27 +1100 (EST), Julien Fischer <jfischer at opturion.com> wrote:
>> >> Hi,
>> >>
>> >> On Thu, 9 Jan 2014, Peter Wang wrote:
>> >>
>> > ...
>> >> >>
>> >> >> I think it is just constructing dynamically that is a problem.
>> >> >
>> >> > The compiler could generate a function for each subtype which returns
>> >> > true if a value fits that subtype, then we extend typeinfos to contain
>> >> > pointers to such functions.  Construct could then check that its
>> >> > arguments have the expected subtypes, otherwise fail.
>> >>
>> >> If the arguments don't have the expected subtypes there should be a mode
>> >> error (as mentioned elsewhere in this thread) -- I know in many cases
>> >> there's not at the moment, but that's a problem (or more likely, several
>> >> problems) with the mode checker.
>> >
>> > Not if, as I hope, the use of subtypes for functor arguments can be kept
>> > internal to a module.
>>
>> You mean it should not be checked statically?
>>
>> >
>> > To reiterate the example, say cord.m uses subtypes internally but
>> > presents the same interface as before.  To an importing module, cord(T)
>> > is an abstract type and cord values are just 'ground'.  There, you could
>> > dynamically construct a cord value where arguments don't have the
>> > expected subtypes, and there would be no mode error because the value
>> > has inst 'ground' as expected.
>> >
>> > Right?
>>
>> Correct. The error would be in cord.m, which is trying to implicitly
>> define an abstract inst. Mercury doesn't support these yet.
>
> What I'm thinking of is rather more straightforward.
>
> Leaving aside dynamic construction, all cord values must be constructed
> in cord.m as it is the only module with access to the type declaration.
> All the constructions would be statically checked.
>
> When a cord value leaves cord.m, the instantiation state can be
> approximated by 'ground'.
>
> A cord value may re-enter cord.m.  As the value must have been
> originally created in cord.m (with exceptions), we can immediately cast
> a 'ground' input cord value to a more precise inst - the inst which we
> inferred for the cord type because its type declaration refers to subtypes.
>
> Unless I've missed something completely obvious, this should be one
> possible way to allow subtypes for functor arguments of a type which is
> abstractly exported and without introducing abstract insts to the
> language.  It does require changes to the runtime and standard library,
> hence the discussion about construct.

I understand what you are proposing, but I don't agree that it is more
straightforward. One thing you may have missed is that the argument
terms can be higher order, in which case they can't be tested in the
way you describe.

As the log message says, the purpose of subtype declarations is to
allow complex insts to be used more readily in pred and func
declarations. They're not intended to make insts do anything that they
can't already do.

Cheers,
Mark.