[m-dev.] for review: add support for existential types [3/4]

[Fergus Henderson]

On 03-Jul-1998, David Glen JEFFERY <dgj at cs.mu.OZ.AU> wrote:
> On 30-Jun-1998, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> > [continued from part 2]
> > 
> > Index: compiler/prog_io.m
> > ===================================================================
> > RCS file: /home/mercury1/repository/mercury/compiler/prog_io.m,v
> > retrieving revision 1.173
> > diff -u -r1.173 prog_io.m
> > --- prog_io.m	1998/05/30 12:25:45	1.173
> > +++ prog_io.m	1998/06/29 09:26:14
> >  
> > +:- type decl_attribute
> > +	--->	purity(purity)
> > +	;	quantifier(quantifier_type, list(tvar))
> > +	;	constraints(quantifier_type, term).
> > +
> > +:- type quantifier_type
> > +	--->	exist
> > +	;	univ.
> > +
> > +:- type decl_attrs == list(pair(decl_attribute, term)).
> 
> Could you please add a comment here saying what exactly the "term" is?

I've added the following two comments:

...
> > +	;	constraints(quantifier_type, term).
                % the term here is the (not yet parsed) list of constraints
...
> > +:- type decl_attrs == list(pair(decl_attribute, term)).
        % the term associated with each decl_attribute
        % is the term containing both the attribute and
        % the declaration that that attribute modifies;
        % this term is used when printing out error messages
        % for cases when attributes are used on declarations
        % where they are not allowed.

> > +	% XXX we should check that `TVars' is of the
> > +	%     appropriate form (i.e. a list of variables)
> 
> Does this get checked elsewhere?

No.

> If not, you should fix the code.

Yes, you are right <sigh>.

> > +		% check that all type variables in existential quantifiers
> > +		% occur somewhere in the body
> 
> I wonder if this is strictly necessary. In any case, I guess it would only
> occur if the programmer had made a mistake.

It's not strictly necessary.  I suppose we could make it a warning
rather than an error.  But it would only occur if the programmer had
made a mistake, and warnings are sometimes easy to ignore, so I thought it
reasonable to just disallow it.  Because of the way the code there is written,
reporting an error happened to be easier than reporting a warning

I thought about these restrictions (this one and related ones) a bit more, and
I've added the following comments:

--- p.m	Fri Jul  3 18:14:31 1998
+++ prog_io.m	Fri Jul  3 18:13:09 1998
@@ -1384,6 +1384,8 @@
 		
 		% check that all type variables in existential quantifiers
 		% do not occur in the head
+		% (maybe this should just be a warning, not an error?
+		% If we were to allow it, we would need to rename them apart.)
 		;
 			list__member(Ctor, Constrs),
 			Ctor = ctor(ExistQVars, _Constraints, _CtorName,
@@ -1396,6 +1398,9 @@
 
 		% check that all type variables in existential quantifiers
 		% occur somewhere in the body
+		% (maybe this should just be a warning, not an error?
+		% If we were to allow it, we should at this point delete any
+		% such unused type variables from the list of quantifiers.)
 		;
 			list__member(Ctor, Constrs),
 			Ctor = ctor(ExistQVars, _Constraints, _CtorName,
@@ -1409,6 +1414,11 @@
 					Body)
 		% check that all type variables in existential constraints
 		% occur in the existential quantifiers
+		% (XXX is this check overly conservative? Perhaps we should
+		% allow existential constraints so long as they contain
+		% at least one type variable which is existentially quantified,
+		% rather than requiring all variables in them to be
+		% existentially quantified.)
 		;
 			list__member(Ctor, Constrs),
 			Ctor = ctor(ExistQVars, Constraints, _CtorName,
 
> > +	%
> > +	% Universal quantification is the default, so we just ignore
> > +	% universal quantifiers.  (It might be a good idea to check
> > +	% that any universally quantified type variables do actually
> > +	% occur somewhere in the type declaration, and are not also
> > +	% existentially quantified, and if not, issue a warning or
> > +	% error message.)
> 
> We should definately check that any universally quantified type vars aren't
> also existentially quantified. Could you `XXX' that please?

Done.

> > Index: compiler/switch_detection.m
> > ===================================================================
> > RCS file: /home/mercury1/repository/mercury/compiler/switch_detection.m,v
> > retrieving revision 1.83
> > diff -u -r1.83 switch_detection.m
> > --- switch_detection.m	1998/06/09 02:14:48	1.83
> > +++ switch_detection.m	1998/06/29 09:26:24
> > @@ -227,7 +227,8 @@
> 
> This change isn't mentioned in the log message. Is it meant to be part of this
> commit?

Oops, no.

> > Index: compiler/typecheck.m
...
> > +		; % Inferring = no
> > +			pred_info_set_head_type_params(PredInfo4,
> > +				HeadTypeParams2, PredInfo5),
> > +
> > +			%
> > +			% leave the original argtypes etc., but 
> > +			% apply any substititions that map existentially
> > +			% quantified type variables to other type vars,
> > +			% and then rename them all to match the new typevarset,
> > +			% so that the type variables names match up
> > +			% (e.g. with the type variables in the
> > +			% constraint_proofs)
> > +			%
> 
> Why does this need special handling?

So that the type variable names match up
(e.g. with the type variables in the constraint_proofs).

[i.e. I don't understand your question ;-)]

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.