[m-rev.] for review: subtypes

[Peter Wang]

On Wed, 8 Jan 2014 20:58:06 +1100, Mark Brown <mark at mercurylang.org> wrote:
> 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.

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.

We would need to be able to check the modes of higher-order terms at
runtime.  At first I thought adding a mode string to the closure
representation would suffice, but another representation would probably
be better to handle higher-order terms with polymorphic modes.

Peter