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

[David Glen JEFFERY]

On 30-Jun-1998, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> Hi,
> 
> DJ, can you please review this?

Sure

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


> Existentially quantified type variables are introduce with
> an explicit `some [T]', e.g. `:- some [T] pred foo(T)'.
> Existentially quantified type class constraints are introduced
> with `&' instead `<=', e.g. `:- some [T] (pred foo(T) & ord(T))'.

s/instead/instead of

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

> Index: compiler/check_typeclass.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/check_typeclass.m,v
> retrieving revision 1.11
> diff -u -r1.11 check_typeclass.m
> --- check_typeclass.m	1998/06/23 05:41:47	1.11
> +++ check_typeclass.m	1998/06/29 09:47:59


> @@ -559,7 +572,7 @@
>  		typecheck__reduce_context_by_rule_application(InstanceTable, 
>  			SuperClassTable, InstanceConstraints, TypeSubst,
>  			InstanceVarSet1, InstanceVarSet2,
> -			Proofs0, Proofs1, SuperClasses, 
> +			Proofs0, Proofs1, SuperClasses,

Did you mean that one?

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

>  	% 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.
> +	% polymorphically or existentially typed and are constrained
> +	% by the typeclass constraints for that typeclass-info variable.

Ditto.

> @@ -538,9 +544,17 @@
>  		% 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)
> +			( list__member(TypeVar, NonLocalTypeVars)
> +			; list__member(TypeVar, ExistQVars)
> +			),
> +			( 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)
> +			)

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

(Also, is the last disjunct actually correct, or is it an oversimplification?) 

> Index: compiler/hlds_out.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
> retrieving revision 1.196
> diff -u -r1.196 hlds_out.m
> --- hlds_out.m	1998/06/19 03:16:14	1.196
> +++ hlds_out.m	1998/06/29 09:25:35

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

>  	module_info_get_predicate_table(ModuleInfo0, PredTable0),
> Index: compiler/inlining.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/inlining.m,v
> retrieving revision 1.77
> diff -u -r1.77 inlining.m
> --- inlining.m	1998/06/09 02:12:58	1.77
> +++ 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?

> 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. Why do we need `in' modes to allow
existentially type lambda expressions? (Oh... I think I do see, actually.
It's the construction versus application thing, I gues. Document it better
nonetheless).

[That's part 1. More to follow].


love and cuddles,
dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) |  Marge: Did you just call everyone "chicken"?
PhD student,                    |  Homer: Noooo.  I swear on this Bible!
Department of Computer Science  |  Marge: That's not a Bible; that's a book of
University of Melbourne         |         carpet samples!
Australia                       |  Homer: Ooooh... Fuzzy.