[m-dev.] for review: enable support for explicit type qualifiers

[Fergus Henderson]

On 20-Sep-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> Any chance of inline type specifiers turning up soon?

Sure.  The long-term aim is probably to use ":" as the
operator for this, but it's easy enough to enable this
feature in the mean time.  For now, I propose we just use
"`with_type`" as the operator.  When we change it to use
`:', we can easily keep the old name as an alternative
for backwards compatibility.

So how about reviewing the following diff?

----------

Estimated hours taken: 1.5

Enable the support for explicit type qualification,
using `with_type` as the operator.

compiler/make_hlds.m:
compiler/hlds_out.m:
	Use `with_type` as the type qualification operator.

tests/hard_coded/type_qual.m:
tests/hard_coded/type_qual.inp:
tests/hard_coded/type_qual.exp:
	Test the new feature.

doc/reference_manual.texi:
	Document the new feature.
	Also make a few improvements to the documentation of
	data-terms, record syntax, and variable scoping.

NEWS:
	Mention the new feature.

Workspace: /home/pgrad/fjh/ws/hg2
Index: NEWS
===================================================================
RCS file: /home/mercury1/repository/mercury/NEWS,v
retrieving revision 1.173
diff -u -d -r1.173 NEWS
--- NEWS	2000/09/19 15:11:36	1.173
+++ NEWS	2000/09/21 02:54:23
@@ -3,6 +3,17 @@
 
 Changes to the Mercury language:
 
+* We've added support for explicit type quantification.
+
+  An expression of the form "Term `with_type` Type",
+  e.g. "X `with_type` list(int)", can be used in place of
+  the specified Term to constrain the type of that term.
+  This is sometimes useful for resolving type ambiguities,
+  which can occur as a result of overloading or polymorphism.
+
+  See the "Explicit type quantification" and "Variable scoping"
+  sections of the language reference manual for details.
+
 * We've added support for record syntax, so that fields of
   constructors can be conveniently extracted and updated
   without writing lots of trivial access predicates.
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.243
diff -u -d -r1.243 hlds_out.m
--- compiler/hlds_out.m	2000/09/08 12:20:31	1.243
+++ compiler/hlds_out.m	2000/09/20 12:07:19
@@ -1849,7 +1849,7 @@
 	hlds_out__write_functor_cons_id(ConsId, ArgVars, VarSet, ModuleInfo,
 		AppendVarnums),
 	( { MaybeType = yes(Type), TypeQual = yes(TVarSet, _) } ->
-		io__write_string(" TYPE_QUAL_OP "),
+		io__write_string(" `with_type` "),
 		mercury_output_term(Type, TVarSet, no, next_to_graphic_token)
 	;
 		[]
@@ -1907,7 +1907,7 @@
 		io__write_string(")")
 	),
 	( { MaybeType = yes(Type), TypeQual = yes(TVarSet, _) } ->
-		io__write_string(" TYPE_QUAL_OP "),
+		io__write_string(" `with_type` "),
 		mercury_output_term(Type, TVarSet, AppendVarnums,
 			next_to_graphic_token)
 	;
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.349
diff -u -d -r1.349 make_hlds.m
--- compiler/make_hlds.m	2000/09/15 05:18:39	1.349
+++ compiler/make_hlds.m	2000/09/20 12:08:03
@@ -6812,8 +6812,7 @@
 	{ RHS = term__functor(F, Args, FunctorContext) },
 	(
 		% Handle explicit type qualification.
-		{ semidet_fail },
-		{ F = term__atom("TYPE_QUAL_OP") },
+		{ F = term__atom("with_type") },
 		{ Args = [RVal, DeclType0] }
 	->
 		{ term__coerce(DeclType0, DeclType) },
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.189
diff -u -d -r1.189 reference_manual.texi
--- doc/reference_manual.texi	2000/09/20 11:45:37	1.189
+++ doc/reference_manual.texi	2000/09/21 03:53:29
@@ -160,6 +160,7 @@
 * DCG-rules::
 * DCG-goals::
 * Data-terms::
+* Variable scoping::
 * Implicit quantification::
 * Elimination of double negation::
 @end menu
@@ -925,12 +926,16 @@
 There are a couple of differences from Prolog.
 The first one is that double-quoted strings are atomic in
 Mercury, they are not abbreviations for lists of character codes.
-The second is that Mercury terms may contain function applications,
-higher-order function applications, and lambda expressions.
+The second is that Mercury provides several extensions to Prolog's
+term syntax: Mercury terms may contain record field selection and
+field update expressions, conditional (if-then-else) expressions,
+function applications, higher-order function applications, lambda
+expressions, and explicit type qualifications.
 
-A data-term is either a variable, a data-functor,
-a conditional expression, a lambda expression,
-or a higher-order function application.
+A data-term is either a variable, a data-functor, or a special data-term.
+A special data-term is a conditional expression, a record syntax expression,
+a lambda expression, a higher-order function application,
+or an explicit type qualification.
 
 @menu
 * Data-functors::
@@ -938,6 +943,7 @@
 * Conditional expressions::
 * Lambda expressions::
 * Higher-order function applications::
+* Explicit type qualification::
 @end menu
 
 @node Data-functors
@@ -945,9 +951,9 @@
 
 A data-functor is an integer, a float, a string, a character literal
 (any single-character name), a name, or a compound data-term.
-A compound data-term is a compound term whose form
-does not match the form of a lambda expression or higher-order
-function application and whose arguments are data-terms.
+A compound data-term is a compound term which does not match
+the form of a special data-term (@pxref{Data-terms}),
+and whose arguments are data-terms.
 If a data-functor is a name or a compound data-term, its top-level functor
 must name a function, predicate, or data constructor declared
 in the program or in the interface of an imported module.
@@ -961,6 +967,8 @@
 Record syntax expressions are transformed into sequences of calls
 to field selection or update functions (@pxref{Field access functions}).
 
+Record syntax expressions have one of the following forms:
+
 @table @code
 @item @var{Term} ^ @var{field}
 
@@ -1098,6 +1106,61 @@
 The type of the higher-order function application term is @var{T}.
 It denotes the result of applying the specified function to the
 specified arguments.  @xref{Higher-order}.
+
+ at node Explicit type qualification
+ at subsection Explicit type qualification
+
+Explicit type qualifications are occaisionally useful
+to resolve ambiguities that can arise from overloading
+or polymorphic types.
+
+An explicit type qualification expression is a term of the form
+
+ at example
+with_type(@var{Term}, @var{Type})
+ at end example
+
+ at noindent
+or equivalently, as it is more commonly written,
+
+ at example
+ at var{Term} `with_type` @var{Type}
+ at end example
+
+ at noindent
+ at var{Term} must be a valid data-term.
+ at var{Type} must be a valid type (@pxref{Types}).
+
+An explicit type qualification expression constrains
+the specified term to have the specified type.
+Apart from that, the meaning of an explicit type qualification
+expression is just the same as the specified @var{Term}.
+
+ at node Variable scoping
+ at section Variable scoping
+
+Variables occurring in data-terms, other than in the right-hand
+(@var{Type}) operand of an explicit type qualification,
+are called ordinary variables,
+while variables occurring in types are called type variables.
+Type variables and ordinary variables occupy different namespaces:
+there is no semantic relationship between a type variable and
+an ordinary variable even if they happen to share the same name.
+(However, as a matter of programming style, it is generally a
+bad idea to use the same name for both a type variable and
+an ordinary variable in the same clause.)
+
+The scope of ordinary variables is the clause or declaration in which
+they occur, unless they are quantified, either explicitly
+(@pxref{Goals}) or implicitly (@pxref{Implicit quantification}).
+
+The scope of type variables in a predicate or function's type
+declaration extends over any explicit type qualifications in the
+clauses for that predicate or function, so explicit type
+qualifications can refer to those type variables.
+The scope of any type variables in an explicit type qualification
+which do not occur in the predicate or function's type declaration
+is the clause in which they occur.
 
 @node Implicit quantification
 @section Implicit quantification
Index: tests/hard_coded/type_qual.exp
===================================================================
RCS file: type_qual.exp
diff -N type_qual.exp
--- /dev/null	Sat Aug  7 21:45:41 1999
+++ type_qual.exp	Thu Sep 21 12:09:36 2000
@@ -0,0 +1,3 @@
+ok(42)
+list:list(io:state)
+list:list(list:list(io:state))
Index: tests/hard_coded/type_qual.inp
===================================================================
RCS file: type_qual.inp
diff -N type_qual.inp
--- /dev/null	Sat Aug  7 21:45:41 1999
+++ type_qual.inp	Thu Sep 21 12:09:20 2000
@@ -0,0 +1 @@
+42.
Index: tests/hard_coded/type_qual.m
===================================================================
RCS file: type_qual.m
diff -N type_qual.m
--- /dev/null	Sat Aug  7 21:45:41 1999
+++ type_qual.m	Thu Sep 21 15:02:17 2000
@@ -0,0 +1,44 @@
+% Test the use of explicit type qualification using the `with_type` operator.
+
+:- module type_qual.
+:- interface.
+:- import_module io.
+
+:- pred main(io__state::di, io__state::uo) is det.
+
+:- implementation.
+:- import_module list, std_util.
+
+main -->
+	test1,
+	test2([] `with_type` list(io__state)),
+	test3.
+
+:- pred test1(io__state::di, io__state::uo) is det.
+
+test1 -->
+	io__read(X `with_type` io__read_result(int)),
+	io__write(X),
+	nl.
+
+:- pred test2(T::in, io__state::di, io__state::uo) is det.
+
+test2(X) -->
+	io__write(type_of(X `with_type` T)),
+	nl,
+	io__write(type_of(_ `with_type` list(T))),
+	nl.
+
+:- pred test3(io__state::di, io__state::uo) is det.
+
+test3 -->
+	io__write(empty_list), nl,
+	io__write(type_of(empty_list)), nl,
+	{ empty(X) },
+	io__write(X), nl,
+	io__write(type_of(X)), nl.
+
+empty_list = [] `with_type` list(int).
+
+empty([] `with_type` list(int)).
+


-- 
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.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------