[m-rev.] for review: allow arbitrary types in class constraints

[David Overton]

On Fri, Apr 12, 2002 at 11:24:11AM +0100, David Jeffery wrote:
> > compiler/hlds_data.m:
> > compiler/hlds_out.m:
> > compiler/make_hlds.m:
> > Allow superclass constraints to have arguments of arbitrary type
> > (rather than just variables) in the superclass table.
> 
> OK, problem here.
> 
> Without some kind of restriction on the constraints on instance
> and typeclass declarations, type checking cannot be gauranteed
> to terminate. (Well, at least not the way that we implement it at
> the moment... you can always gaurantee termination by limiting the
> number of iterations that the type checker does, in much the same
> way that we manage to gaurantee termination when inferring types
> in the presence of polymorphic recursion. But we don't.).
> 
> For example, applying the instance declaration:
> 
> :- instance c(f(T)) <= c(f(f(T))).
> 
> is almost certainly going to give you troubles when trying to satisfy
> a 'f(...)' constraint on a pred call.
> 
> ...and similarly for typeclass declarations. e.g. given the following
> declaration:
> 
> :- typeclass c(T) <= c(f(T)) where [...].
> 
> then checking the correctness of an instance declaration for 'c' is
> going to result in an infinite loop. e.g. for 'c(int)' to be a valid
> instance, the typeclass declaration makes us check that
> c(f(int)) is valid, and in turn that c(f(f(int))) is valid, ad infinitum.
> 
> But there shouldn't be any problems with allowing 'arbitrary'
> constraints on predicate types.
> 
> I'm going to have to leave it there... I'll discuss it with you in
> person next week.
> 

After discussing this with DJ and Zoltan, we've decided to restrict the
arguments of constraints on instance and typeclass declarations (at
least for now) to be either type variables or ground types.

This is sufficient to ensure termination of the type checker, although
we may decide to relax this restriciton in the future.

The following is an absolute diff for prog_io_typeclass.m and a relative
diff for the other files.

Index: prog_io_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_typeclass.m,v
retrieving revision 1.24
diff -u -r1.24 prog_io_typeclass.m
--- prog_io_typeclass.m	20 Mar 2002 12:37:14 -0000	1.24
+++ prog_io_typeclass.m	17 Apr 2002 05:19:18 -0000
@@ -156,7 +156,7 @@
 
 parse_superclass_constraints(ModuleName, Constraints, Result) :-
 	parse_simple_class_constraints(ModuleName, Constraints, 
-		"constraints on class declaration may only constrain type variables, not compound types",
+		"constraints on class declaration may only constrain type variables and ground types",
 		Result).
 
 :- pred parse_unconstrained_class(module_name, term, tvarset, maybe1(item)).
@@ -273,15 +273,15 @@
 % or on an existentially quantified type definition.
 
 parse_class_constraints(ModuleName, ConstraintsTerm, Result) :-
-	parse_class_and_inst_constraints(ModuleName, ConstraintsTerm, Result0),
-	extract_class_constraints(Result0, Result).
+	parse_simple_class_constraints(ModuleName, ConstraintsTerm,
+		"sorry, not implemented: constraints may only constrain type variables and ground types",
+		Result).
 
 parse_class_and_inst_constraints(ModuleName, ConstraintsTerm, Result) :-
-	parse_simple_class_and_inst_constraints(ModuleName, ConstraintsTerm, 
-		"sorry, not implemented: constraints may only constrain type variables, not compound types",
+	parse_arbitrary_class_and_inst_constraints(ModuleName, ConstraintsTerm, 
 		Result).
 
-% Parse constraints which can only constrain type variables
+% Parse constraints which can only constrain type variables and ground types.
 
 :- pred parse_simple_class_constraints(module_name, term, string,
 		maybe1(list(class_constraint))).
@@ -307,7 +307,8 @@
 			list__member(Constraint, ConstraintList),
 			Constraint = constraint(_, Types),
 			list__member(Type, Types),
-			\+ type_util__var(Type, _)
+			\+ type_util__var(Type, _),
+			\+ term__is_ground(Type)
 		->
 			Result = error(ErrorMessage, ConstraintsTerm)
 		;
@@ -376,7 +377,15 @@
 		% constraints do not contain any info in their prog_context
 		% fields
 		list__map(convert_type, Args0, Args),
-		Result = ok(class_constraint(constraint(ClassName, Args)))
+
+		% Check that the arguments contain at least one type variable.
+		( term__contains_var_list(Args, _) ->
+			Result = ok(class_constraint(constraint(ClassName,
+						Args)))
+		;
+			Result = error("class constraint contains no variables",
+					ConstraintTerm)
+		)
 	;
 		Result = error("expected atom as class name or inst constraint",
 			ConstraintTerm)
@@ -465,7 +474,7 @@
 
 parse_instance_constraints(ModuleName, Constraints, Result) :-
 	parse_simple_class_constraints(ModuleName, Constraints,
-		"constraints on instance declaration may only constrain type variables, not compound types",
+		"constraints on instance declaration may only constrain type variables and ground types",
 		Result).
 
 :- pred parse_underived_instance(module_name, term, tvarset, maybe1(item)).

 :- pred parse_underived_instance(module_name, term, tvarset, maybe1(item)).
 :- mode parse_underived_instance(in, in, in, out) is det.
diff -u doc/reference_manual.texi doc/reference_manual.texi
--- doc/reference_manual.texi	12 Apr 2002 02:30:18 -0000
+++ doc/reference_manual.texi	17 Apr 2002 05:01:04 -0000
@@ -4300,8 +4300,10 @@
 Type class constraints may also appear in @code{typeclass} declarations, 
 meaning that one type class is a ``superclass'' of another. 
 
-The variables that appear in the arguments to the type classes in the
-constraints
+The arguments of a constraint on a type class declaration must be either type
+variables or ground types.
+Each constraint must contain at least one variable argument and
+all variables that appear in the arguments 
 must also be arguments to the type class in question.
 
 For example, the following declares the @samp{ring} type class, which describes
@@ -4339,10 +4341,12 @@
 @node Type class constraints on instance declarations
 @section Type class constraints on instance declarations
 
-Typeclass constraints may also be placed upon instance declarations.  The
-variables that appear in the arguments to the type classes in the
-constraints must
-all be type variables that appear in the types in the instance declarations.
+Typeclass constraints may also be placed upon instance declarations.
+The arguments of such constraints must be either type variables or ground
+types.
+Each constraint must contain at least one variable argument and all
+variables that appear in the arguments
+must be type variables that appear in the types in the instance declaration.
 
 For example, consider the following declaration of a type class of types that 
 may be printed:
diff -u tests/hard_coded/typeclasses/recursive_instance_1.exp tests/hard_coded/typeclasses/recursive_instance_1.exp
--- tests/hard_coded/typeclasses/recursive_instance_1.exp	12 Apr 2002 02:30:18 -0000
+++ tests/hard_coded/typeclasses/recursive_instance_1.exp	17 Apr 2002 05:01:04 -0000
@@ -1 +1 @@
-[0, 1, 2]
+3
diff -u tests/hard_coded/typeclasses/recursive_instance_1.m tests/hard_coded/typeclasses/recursive_instance_1.m
--- tests/hard_coded/typeclasses/recursive_instance_1.m	12 Apr 2002 02:30:18 -0000
+++ tests/hard_coded/typeclasses/recursive_instance_1.m	17 Apr 2002 05:01:04 -0000
@@ -6,18 +6,29 @@
 
-:- typeclass foo(T) where [
-	func bar(T) = T
+:- typeclass foo(T, U) where [
+	func bar(T) = U
 ].
 
-:- instance foo(list(T)) <= foo(list(T)) where [
-	bar(Xs) = Xs
+:- instance foo(int, list(T)) <= foo(list(int), T) where [
+	bar(N) = ( N < 0 -> [bar([N+1])] ; [] )
+].
+
+:- instance foo(list(T), int) <= foo(T, list(int)) where [
+	( bar([X | Xs]) = N + bar(Xs) :-
+		bar(X) = B,
+		( B = [N | _]
+		; B = [],
+			N = 1
+		)
+	),
+	( bar([]) = 0 )
 ].
 
 :- pred main(io::di, io::uo) is det.
 
 :- implementation.
-:- import_module std_util.
+:- import_module std_util, char.
 
 main -->
 	{ X = bar([0,1,2]) },
-	io__print(X),
+	io__write_int(X),
 	io__nl.
reverted:
--- tests/hard_coded/typeclasses/recursive_instance_2.exp	12 Apr 2002 02:30:18 -0000
+++ /dev/null	1 Jan 1970 00:00:00 -0000
@@ -1 +0,0 @@
-[0, 1, 2]
reverted:
--- tests/hard_coded/typeclasses/recursive_instance_2.m	12 Apr 2002 02:30:18 -0000
+++ /dev/null	1 Jan 1970 00:00:00 -0000
@@ -1,26 +0,0 @@
-:- module recursive_instance_2.
-:- interface.
-
-:- import_module int, io.
-:- import_module list, std_util.
-
-:- typeclass foo(T) where [
-	func bar(T) = T
-].
-:- typeclass baz(T) where [].
-
-:- instance foo(list(T)) <= baz(maybe(T)) where [
-	bar(Xs) = Xs
-].
-
-:- instance baz(maybe(T)) <= foo(list(T)) where [].
-
-:- pred main(io::di, io::uo) is det.
-
-:- implementation.
-:- import_module std_util.
-
-main -->
-	{ X = bar([0,1,2]) },
-	io__print(X),
-	io__nl.

-- 
David Overton      Computer Science and Software Engineering
PhD Student        The University of Melbourne   +61 3 8344 9159
Research Fellow    Monash University (Clayton)   +61 3 9905 5779
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------