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

[Fergus Henderson]

On 01-Jul-1998, David Glen JEFFERY <dgj at cs.mu.OZ.AU> wrote:
> > Merge in the changes from the existential types branch.
> > These changes add support for existentially quantified type variables
> > and type class constraints on functions and predicates.
> 
> I would explicitly mention that existentially quantified components of data
> structures are not yet supported, and give a justification. (ie. that it's
> a tricker problem... you need to overcome the problem that an appearance of
> a constructor may be a construction or a deconstruction (or both), so the
> type variable could be existentially or universally quantifed).
> 
> (Oh, I see that you mention this briefly later on... probably worth a mention
> here too).

OK, I've added the following:

	(Existential data types, however, are not supported -- see below.)

> s/instead/instead of

Done.

> > There's still several limitations:
> > 
> > 0.  XXX It's not yet documented in the language reference manual.
> 
> I actually think that it's a good idea not to document it in the language
> reference manual at this stage. After all, there are a lot of details to be
> worked out. (Then again, I guess there will be few user-visible changes...).
> 
> I think it would be best not to mention this stuff until it is a whole lot
> more stable. (ie. at least until we have fixed the compile errors you
> mentioned, but probably longer).

I agree that it shouldn't be documented in the language reference manual
proper until it is a lot more stable.  The language reference manual
really ought to be changed as infrequently as possible.

On the other hand, it really ought to be documented _somewhere_ in the
intervening period.  Perhaps we should a new section to the language
reference manual for "Future extensions" which would be less stable.

> > -			Proofs0, Proofs1, SuperClasses, 
> > +			Proofs0, Proofs1, SuperClasses,
> 
> Did you mean that one?

That was just whitespace at the end of the line -- I've undone that change.

> > Index: compiler/goal_util.m
> > ===================================================================
> > RCS file: /home/mercury1/repository/mercury/compiler/goal_util.m,v
> > retrieving revision 1.46
> > diff -u -r1.46 goal_util.m
> > --- goal_util.m	1998/06/09 02:12:44	1.46
> > +++ goal_util.m	1998/06/29 09:25:29
> > @@ -68,19 +68,25 @@
> >  :- mode goal_util__goals_goal_vars(in, in, out) is det.
> >  
> >  	%
> > +	% goal_util__extra_nonlocal_typeinfos(TypeInfoMap, TypeClassInfoMap,
> > +	%		VarTypes, ExistQVars, Goal, NonLocalTypeInfos):
> > +	% compute which type-info and type-class-info variables
> > +	% may need to be non-local to a goal.
> > +	%
> >  	% A type-info variable may be non-local to a goal if any of 
> >  	% the ordinary non-local variables for that goal are
> > -	% polymorphically typed with a type that depends on that
> > -	% type-info variable.
> > +	% polymorphically or existentially typed with a type
> > +	% that depends on that type-info variable.
> 
> "polymorphically or existentially typed" doesn't quite make sense. Maybe
> you should talk specifically about which inputs to the pred you are talking
> about.

I have changed it to read as follows:

        %
        % A type-info variable may be non-local to a goal if any of
        % the ordinary non-local variables for that goal are
        % polymorphically typed with a type that depends on that
        % type-info variable, or if the type-info is for an
        % existentially quantified type variable.
        % 
        % In addition, a typeclass-info may be non-local to a goal if
        % any of the non-local variables for that goal are
        % polymorphically typed and are constrained by the typeclass
        % constraints for that typeclass-info variable,
        % or if the the type-class-info is for an existential constraint,
        % i.e. a constraint which contrains an existentially quantified
        % type variable.
        % 

> Could you please add a couple more lines of comments to this? I imagine
> others won't find it too obvious.

I've added the following comments:

@@ -538,9 +548,30 @@
 		% Find all the type-infos and typeclass-infos that are
 		% non-local
 	solutions_set(lambda([Var::out] is nondet, (
-			list__member(TheVar, NonLocalTypeVars),
-			map__search(TypeVarMap, TheVar, Location),
-			type_info_locn_var(Location, Var)
+			%
+			% if there is some TypeVar for which either
+			% (a) the type of some non-local variable
+			%     depends on that type variable, or
+			% (b) that type variable is existentially
+			%     quantified
+			%
+			( list__member(TypeVar, NonLocalTypeVars)
+			; list__member(TypeVar, ExistQVars)
+			),
+			%
+			% then the type_info Var for that type,
+			% and any type_class_info Vars which represent
+			% constraints on types which include that type,
+			% should be included in the NonLocalTypeInfos.
+			%
+			( map__search(TypeVarMap, TypeVar, Location),
+			  type_info_locn_var(Location, Var)
+			;
+			  % this is probably not very efficient...
+			  map__member(TypeClassVarMap, Constraint, Var),
+			  Constraint = constraint(_Name, ArgTypes),
+			  term__contains_var_list(ArgTypes, TypeVar)
+			)
 		)), NonLocalTypeInfos).
 
> (Also, is the last disjunct actually correct, or is it an oversimplification?)

To the best of my knowledge, the last disjunct is correct.

> > Index: compiler/hlds_out.m
> 
> You don't seem to mention this in the log message.
...
> > -:- pred hlds_out__write_constructor(tvarset, constructor, io__state, io__state).
> > -:- mode hlds_out__write_constructor(in, in, di, uo) is det.
> 
> Why does this disappear? (Mention it in the log message).

I've added the following:

compiler/hlds_out.m:
	Print out the new fields in the pred_info (except the
	unsatisfied type class constraints -- if these are non-empty,
	post_typecheck.m will print them out in the error message).
	When printing out types, pass the AppendVarNums parameter down,
	so that HLDS dumps will distinguish between different type
	variables that have the same name.
	Delete hlds_out__write_constructor, since it was doing exactly
	the same thing as mercury__output_ctor.

> > +++ inlining.m	1998/06/29 09:25:38
> 
> > @@ -315,6 +317,11 @@
> >  		int,			% variable threshold for inlining
> >  		set(pred_proc_id),	% inlined procs
> >  		module_info,		% module_info
> > +		list(tvar),		% universally quantified type vars
> > +					% occurring in the argument types
> > +					% for this predicate (the caller,
> > +					% not the callee).  These are the
> > +					% ones that must not be bound.
> 
> Does this include the existential tvars from the callees too?

This is a good question.  No, it doesn't.

The reason it doesn't is that it may need to bind type variables
for a callee, if it is inlining that callee.

The only time that binding type variables causes a problem
is if we bind one of the universally quantified type vars
in the argument types for the predicate.  Such bindings
could only ever rename the type variable to something different,
rather than actually binding it to a ground type, but that
might cause problems because, um, the list of type variables
in the pred decl would no longer be the same as the type variables
in the proc.  Well, I'm not sure if that would cause problems,
but I'm not sure it won't, so best to be on the safe side.

So how about I just add "... must not be bound, because renaming
those type variables would mean that the type variables in the
proc_info don't match the ones in the pred_info, which I think
might cause problems." at the end of that comment?

> > Index: compiler/lambda.m
> > ===================================================================
> > RCS file: /home/mercury1/repository/mercury/compiler/lambda.m,v
> > retrieving revision 1.43
> > diff -u -r1.43 lambda.m
> > --- lambda.m	1998/06/09 02:13:05	1.43
> > +++ lambda.m	1998/06/29 09:25:41
> 
> > +		% Currently we don't allow existentially typed lambda
> > +		% expressions (we can change this if/when we allow
> > +		% `in' modes for existentially typed arguments)
> 
> I'm confused by that comment.

Yes, I think I was confused when I wrote it ;-)
In fact existential types and higher order don't mix, unless
you have support for second-order polymorphism, which we don't --
see the comments below for more details.

I've added some more detailed documentation.
I think I will also need to modify typecheck.m to disallow
taking the address of a predicate or function with an existential type.
It would probably also be a good idea to add some test cases.

Anyway, here's a new diff for lambda.m (I deleted the unrelated
parts, which were the same as in the previous diff).

Index: lambda.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/lambda.m,v
retrieving revision 1.43
diff -u -u -r1.43 lambda.m
--- lambda.m	1998/06/09 02:13:05	1.43
+++ lambda.m	1998/07/01 12:15:49
@@ -30,9 +30,38 @@
 %	'__LambdaGoal__1'(X, Y) :- q(Y, X).
 %
 %
+% Note that the mode checker requires that a lambda expression
+% not bind any of the non-local variables such as `X' in the above
+% example.
 %
-%	Note: Support for lambda expressions which involve class constraints
-%	      is not yet complete.
+% Similarly, a lambda expression not bind any of the type_infos for
+% those variables; that is, none of the non-local variables
+% should be existentially typed (from the perspective of the lambda goal).
+% When we run the polymorphism.m pass before mode checking, this will
+% be checked by mode analysis.  XXX But currently it is not checked.
+%
+% It might be OK to allow the parameters of the lambda goal to be
+% existentially typed, but currently that is not supported.
+% One difficulty is that it's hard to determine here which type variables
+% should be existentially quantified.  The information is readily
+% available during type inference, and really type inference should save
+% that information in a field in the lambda_goal struct, but currently it
+% doesn't; it saves the head_type_params field in the pred_info, which
+% tells us which type variables where produced by the body, but for
+% any given lambda goal we don't know whether the type variable was
+% produced by something outside the lambda goal or by something inside
+% the lambda goal (only in the latter case should it be existentially
+% quantified).
+% The other difficulty is that taking the address of a predicate with an
+% existential type would require second-order polymorphism:  for a predicate
+% declared as `:- some [T] pred p(int, T)', the expression `p' must have
+% type `some [T] pred(int, T)', which is quite a different thing to saying
+% that there is some type `T' for which `p' has type `pred(int, T)' --
+% we don't know what `T' is until the predicate is called, and it might
+% be different for each call.
+% Currently we don't support second-order polymorphism, so we
+% don't support existentially typed lambda expressions either.
+% 
 
 %-----------------------------------------------------------------------------%
 
@@ -241,8 +270,11 @@
 		Unification0, Functor, Unification, LambdaInfo0, LambdaInfo) :-
 	LambdaInfo0 = lambda_info(VarSet, VarTypes, Constraints, TVarSet,
 			TVarMap, TCVarMap, POF, PredName, ModuleInfo0),
-	goal_util__extra_nonlocal_typeinfos(TVarMap, VarTypes,
-		LambdaGoal, ExtraTypeInfos),
+	% XXX existentially typed lambda expressions are not yet supported
+	% (see the documentation at top of this file)
+	ExistQVars = [],
+	goal_util__extra_nonlocal_typeinfos(TVarMap, TCVarMap, VarTypes,
+		ExistQVars, LambdaGoal, ExtraTypeInfos),
 	lambda__transform_lambda(PredOrFunc, PredName, Vars, Modes, Det,
 		OrigNonLocals0, ExtraTypeInfos, LambdaGoal, Unification0,
 		VarSet, VarTypes, Constraints, TVarSet, TVarMap, TCVarMap,
@@ -356,8 +388,11 @@
 			PredOrFunc, OrigPredName, OrigLine,
 			LambdaCount, PredName),
 		goal_info_get_context(LambdaGoalInfo, LambdaContext),
-		% the TVarSet is a superset of what it really ought be,
-		% but that shouldn't matter
+		% The TVarSet is a superset of what it really ought be,
+		% but that shouldn't matter.
+		% XXX existentially typed lambda expressions are not
+		% yet supported (see the documentation at top of this file)
+		ExistQVars = [],
 		lambda__uni_modes_to_modes(UniModes1, OrigArgModes),
 
 		% We have to jump through hoops to work out the mode
 

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