[m-dev.] Existentially quantified data constructors

[Ian MacLarty]

On Wed, Apr 16, 2008 at 02:18:32PM +1000, Julien Fischer wrote:
>
> On Wed, 16 Apr 2008, Ralph Becket wrote:
>
>> Julien Fischer, Wednesday, 16 April 2008:
>>>
>>>> (don't use equivalence types in instance declarations,
>>>
>>> There is no such restriction, perhaps this was the one you were
>>> referring to?
>>>
>>> 	The types in an instance declaration must not be abstract types
>>> 	which are elsewhere defined as equivalence types.
>>
>> Yes, that's the one.
>>
>>>> don't repeat variables in instance declarations, instance
>>>> variable arguments must be of the form typector(typevar, typevar, ...),
>>>
>>> The reference manual already gives the reasons for these restrictions,
>>> from section 10.2
>>>
>>> 	These restrictions ensure that there are no overlapping instance
>>> 	declarations, i.e. for each typeclass there is at most one instance
>>> 	declaration that may be applied to any type (or sequence of types).
>>
>> Is this a necessary restriction or an artefact of our implementation?
>
> The latter.  Certain aspects could (probably) be relaxed, e.g.
> you could have unwrapped variables as some, although not all, arguments
> of an instance head.  Exactly what restrictions could be dropped depend
> on the form that any future version of the type class system takes.
> (This has been extensively discussed on this list some time in the recent 
> past.)
>
>> Why isn't this rule relaxed with functional dependencies?
>
> I don't see how information from functional dependencies would help
> here.
>

Well, suppose you have the typeclass:

:- typeclass set(Set, Element) <= (Set -> Element)

then all you need to uniquely identify the instance is the type of the
first argument, so instances like:

:- instance set(set_ctree234(T), T)

should be allowed.

I tried modifying the algorithm for generating the name of the global
variable that holds the base typeclass info.  I modified it so that if a
variable appeared in the instance type list, it just used the string "T"
in that position.  This then allows me to use instances like the one
above.

If we relax the instance restrictions in the following way:

1. Arguments may be variables as long as they only appear in the range
   of a functional dependency (i.e. don't appear in the domain of a
   functional dependency, or outside a functional dependency).
2. Duplicate variables are allowed as long as there are only two
   occurences of the duplicated variable, with each occurance being in a
   separate argument position, and those argument positions having a
   functional dependency between them.

then we would be able to define a lot of useful instances that we can't
now, without weakening our current ability to detect overlapping instances.

Here is my experimental diff, along with a program with some
instances we can't have now that compiles and runs after applying the
diff.

Index: check_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/check_typeclass.m,v
retrieving revision 1.120
diff -u -r1.120 check_typeclass.m
--- check_typeclass.m	7 Apr 2008 02:32:50 -0000	1.120
+++ check_typeclass.m	21 Apr 2008 01:43:29 -0000
@@ -154,7 +154,7 @@
     maybe_write_string(Verbose,
         "% Checking instance declaration types...\n", !IO1)
     ),
-    check_instance_declaration_types(!ModuleInfo, !Specs),
+    % check_instance_declaration_types(!ModuleInfo, !Specs),
 
     % If we encounter any errors while checking that the types in an
     % instance declaration are valid then don't attempt the remaining
Index: hlds_code_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_code_util.m,v
retrieving revision 1.38
diff -u -r1.38 hlds_code_util.m
--- hlds_code_util.m	3 Apr 2008 05:26:43 -0000	1.38
+++ hlds_code_util.m	21 Apr 2008 01:26:44 -0000
@@ -175,7 +175,7 @@
         string.int_to_string(TypeArity, TypeArityString),
         String = TypeNameString ++ "__arity" ++ TypeArityString ++ "__"
     ;
-        unexpected(this_file, "type_to_string: invalid type")
+        String = "T"
     ).
 
 %----------------------------------------------------------------------------%
Index: polymorphism.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/polymorphism.m,v
retrieving revision 1.332
diff -u -r1.332 polymorphism.m
--- polymorphism.m	7 Apr 2008 02:32:51 -0000	1.332
+++ polymorphism.m	21 Apr 2008 01:42:45 -0000
@@ -2214,6 +2214,7 @@
     construct_typeclass_info(InstanceExtraTypeInfoUnconstrainedVars,
         InstanceExtraTypeInfoVars, InstanceExtraTypeClassInfoVars,
         ClassId, Constraint, InstanceNum, ConstrainedTypes,
+        ProofInstanceDefn ^ instance_types,
         Proofs, ExistQVars, Var, NewGoals, !Info),
 
     MaybeVar = yes(Var),
@@ -2290,12 +2291,14 @@
 
 :- pred construct_typeclass_info(list(prog_var)::in, list(prog_var)::in,
     list(prog_var)::in, class_id::in, prog_constraint::in, int::in,
-    list(mer_type)::in, constraint_proof_map::in, existq_tvars::in,
+    list(mer_type)::in, list(mer_type)::in,
+    constraint_proof_map::in, existq_tvars::in,
     prog_var::out, list(hlds_goal)::out, poly_info::in, poly_info::out) is det.
 
 construct_typeclass_info(ArgUnconstrainedTypeInfoVars, ArgTypeInfoVars,
         ArgTypeClassInfoVars, ClassId, Constraint, InstanceNum, InstanceTypes,
-        SuperClassProofs, ExistQVars, NewVar, NewGoals, !Info) :-
+        InstanceDefnTypes, SuperClassProofs, ExistQVars, NewVar, NewGoals,
+        !Info) :-
 
     poly_info_get_module_info(!.Info, ModuleInfo),
 
@@ -2319,7 +2322,7 @@
     map.lookup(InstanceTable, ClassId, InstanceList),
     list.index1_det(InstanceList, InstanceNum, InstanceDefn),
     InstanceModuleName = InstanceDefn ^ instance_module,
-    make_instance_string(InstanceTypes, InstanceString),
+    make_instance_string(InstanceDefnTypes, InstanceString),
     ConsId = base_typeclass_info_const(InstanceModuleName, ClassId,
         InstanceNum, InstanceString),
     BaseTypeClassInfoTerm = rhs_functor(ConsId, no, []),


test.m:
%----------------------------------------------------------------------------%
:- module test.

:- interface.

:- import_module io.

:- pred main(io::di, io::uo) is det.

%----------------------------------------------------------------------------%

:- implementation.

:- import_module char.
:- import_module int.
:- import_module list.
:- import_module set.
:- import_module set_ctree234.
:- import_module stream.
:- import_module string.

%----------------------------------------------------------------------------%
% Set typeclass.

:- typeclass set(Set, Element) <= (Set -> Element) where
[
	pred is_member(Set::in, Element::in) is semidet,
	pred add(Element::in, Set::in, Set::out) is det,
	func num_elems(Set) = int
].

:- instance set(set(T), T) where
[
	pred(is_member/2) is set.contains,
	( add(Elem, !Set) :-
		set.insert(!.Set, Elem, !:Set)
	),
	func(num_elems/1) is set.count
].

:- instance set(set_ctree234(T), T) where
[
	pred(is_member/2) is set_ctree234.contains,
	( add(Elem, !Set) :-
		set_ctree234.insert(Elem, !Set)
	),
	func(num_elems/1) is set_ctree234.count
].

:- type some_set
	---> some [S, E] some_set(S) => set(S, E).

:- func some_set_count(some_set) = int.

some_set_count(some_set(S)) = num_elems(S).

:- some [S] func some_value = S.

some_value = 1.

%----------------------------------------------------------------------------%
% Compression stream.

:- type zip(Stream) ---> zip(Stream).

:- instance stream.stream(zip(Stream), State) 
	<= stream.stream(Stream, State)
where
[
	( name(zip(S), "zipped " ++ Name, !State) :-
		name(S, Name, !State)
	)
].

:- instance stream.output(zip(Stream), State)
	<= stream.output(Stream, State)
where
[
	( flush(zip(S), !State) :-
		flush(S, !State)
	)
].

:- type byte == int.

:- instance stream.writer(zip(Stream), string, State)
	<= stream.writer(Stream, byte, State)
where
[
	( put(zip(S), Str, !State) :-
		Chars = string.to_char_list(Str),
		CharCodes = list.map(char.to_int, Chars),
		% ... do compression ...
		list.foldl(put(S), CharCodes, !State)
	)
].

%----------------------------------------------------------------------------%

main(!IO) :-
	S1 = set.make_singleton_set(1),
	S2 = set_ctree234.make_singleton_set(2),
	V:T = some_value,
	add(V, set.init:set(T), S3),
	( is_member(S1, 1) ->
		io.write_string("yes", !IO)
	;
		io.write_string("no", !IO)
	),
	nl(!IO),
	( is_member(S2, 1) ->
		io.write_string("yes", !IO)
	;
		io.write_string("no", !IO)
	),
	nl(!IO),
	( is_member(S3, V) ->
		io.write_string("yes", !IO)
	;
		io.write_string("no", !IO)
	),
	nl(!IO),
	io.write_int(num_elems(S1) + num_elems(S2) + num_elems(S3), !IO),
	nl(!IO),
	SetList = ['new some_set'(S1), 'new some_set'(S2),
		'new some_set'(S3)],
	Counts = list.map(some_set_count, SetList),
	io.write(Counts, !IO),
	nl(!IO),
	ZipStream = zip(io.stdout_stream),
	put(ZipStream, "hello\n", !IO),
	put(ZipStream, "there\n", !IO),
	flush(ZipStream, !IO),
	nl(!IO).

%----------------------------------------------------------------------------%

Is it worth incorporating this diff and modifying the instance check
accordingly?

Ian.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------