subtyping proposal

[Fergus Henderson]

Here's a suggestion for a language extension,
namely a new `:- subtype' declaration.

Syntax:

	:- subtype SubType < Type :: Inst.
	:- subtype SubType < Type ---> BoundInst.

Legality rules:

	`SubType' must be a non-variable term whose arguments (if any)
	are distinct variables.
	`Type' must be a type, or another subtype.
	`Inst' must be a ground inst.  
	`BoundInst' must be a disjunction of non-variable terms whose
	arguments are ground insts.
	`Type', `Inst' and `BoundInst' must not contain any variables
	that don't occur in `SubType'.
	If `Type' is another subtype, then `Inst' or `BoundInst' must
	specify a set of values which is a subset of the values allowed
	for `Type'.

Semantics:

	A subtype declaration

		:- subtype SubType < Type ---> BoundInst.

	is equivalent to the declaration

		:- type SubType < Type :: bound(BoundInst).

	A subtype declaration

		:- subtype SubType < Type :: Inst.

	is equivalent to the declaration

		:- type SubType == Type.
		:- inst SubInst :: Inst.

	where `SubInst' is textually the same as `SubType',
	with the following additional effect: for any argument
	whose type is declared as `SubType', the subtype information
	specified by the inst `SubInst' will be propagated into all the
	mode declarations for that argument. 
	[For example, if `SubInst' is `bound(Functors)', then any
	`ground' inst in the mode of an argument for that subtype
	will become `bound(Functors)', , any `unique' will become
	`unique(Functors)', etc., with the information being
	propagated into functor arguments recursively.]

Example:

	:- type fruit ---> apple ; orange ; lemon.
	:- subtype citrus < fruit ---> orange ; lemon.

	:- pred p(fruit::in, citrus::out).
	:- pred q(citrus::di, citrus::uo).

i.e.

	:- pred p(fruit::ground->ground, citrus::free->ground).
	:- pred q(citrus::unique->unique, citrus::free->unique).

This is equivalent to

	:- type fruit ---> apple ; orange ; lemon.
	:- type citrus == fruit.
	:- inst ground_citrus == bound(orange ; lemon).
	:- inst unique_citrus == unique(orange ; lemon).

	:- pred p(fruit::in, fruit::out(ground_citrus)).
	:- pred q(fruit::di(unique_citrus), fruit::out(unique_citrus)).

i.e.

	:- pred p(fruit::ground->ground, fruit::free->citrus).
	:- pred q(fruit::uniq_citrus->dead, fruit::free->uniq_citrus).

Rationale:
	
	This language extension makes it simpler for users to use
	subtypes, without needing to know the mode system in quite so
	much detail.  It makes it easier to convert a program that
	didn't use subtypes into one that does, and avoids putting
	unnecessary clutter in the mode declarations.

	This change would allow us to use subtypes to define the
	io__stream types

		io__stream
		io__text_stream
		io__input_stream
		io__output_stream
		io__bidirectional_stream
		io__binary_stream
		io__binary_input_stream
		io__binary_output_stream
		io__binary_bidirectional_stream

	with an appropriate subtype relation.
	The subtype relation here involves multiple inheritence:

					io__stream
				 	/         \
				       /	   \
			io__text_stream	  	   io__binary_stream
			/         \			/       \
	    io__input_stream   io__output_stream      ...	...
		        \         /			\       /
		   io__bidirectional_stream		 .......

	This could be handled as follows:

		:- type io__stream.
			% abstract, but conceptually defined
			% as follows:
			% :- type io__stream --->
			%		io__stream(
			%		text_or_binary,
			%		bool,	% input
			%		bool,	% output
			%		c_pointer).
			% :- type text_or_binary ---> text ; binary.
		
		:- inst ? == ground.
		:- inst yes ---> yes.
		:- inst text ---> text.
		:- inst binary ---> binary.

		:- subtype io__text_stream < io__stream
			---> io__stream(text, ?, ?, ?).

		:- subtype io__binary_stream < io__stream
			---> io__stream(binary, ?, ?, ?).

		:- subtype io__input_stream < io__text_stream
			---> io__stream(text, yes, ?, ?).

		:- subtype io__output_stream < io__text_stream
			---> io__stream(text, ?, yes, ?).

		:- subtype io__bidirectional_stream < io__text_stream
			---> io__stream(text, yes, yes, ?).

Drawbacks:
	
	One problem with this proposal as it stands is that using the
	mode system for subtypes doesn't work well with polymorphic
	predicates or containers.

	We could fix these problems by adding support for polymorphic
	modes, with the inst variables required to name ground insts.
	This restriction would make polymorphic modes relatively easy
	to implement.  For polymorphically typed predicates, we could
	propagate type information into the modes so that all polymorphically
	typed predicates also become polymorphically moded.

	For example, for `set__singleton_set(set(T)::out, T::in)',
	if at a particular call the 2nd argument has inst `bound(foo)',
	then on exit the first argument would have inst `set(bound(foo))'
	where `set(I)' is a (compiler-generated) polymorphic inst
	whose shape reflects the definition of the `set(T)' type.

	That is unsound in the case of programs that use std_util__construct/3
	(e.g. via io__read/3 or term__to_type/2).  However, we could patch
	up that hole by adding a typeclass `constructable(T)',
	declaring std_util_construct/3 and its callers to take arguments
	of that typeclass, and allowing the propagation of subtype
	information only for polymorphic type variables which are not
	constrained to be a subclass of `constructable'.
	
Counter-Rationale:

	We already have one mechanism for subtypes/inheritence,
	namely type classes; do we need another one?

-----------------------------------------------------------------------------

While I'm at it, here's an alternative syntax that might (or might not)
be better.

Syntax:

	:- subtype SubType < Type ---> Functors.

Legality Rules:

	`Functors' is a disjunction of non-variable terms
	whose arguments are types or subtypes.
	`Type' and `Functors' must not contain any variables
	that don't occur in `SubType', except that `Functors' may
	contain "don't care" (underscore) variables.
	If `Type' is another subtype, then `Functors' must specify a
	set of values which is a subset of the values allowed for `Type'.

Semantics:

	Any "don't care" (underscore) variables in `Functors' are
	replaced with `ground'.

	A subtype declaration

		:- subtype SubType < Type ---> Functors.

	is equivalent to the declaration

		:- type SubType == Type.

	with the following additional effect: for any argument
	whose type is declared as `SubType', the subtype information
	specified by `Functors' will be propagated into all the
	mode declarations for that argument.  Any `ground' will
	become `bound(Functors)', , any `unique' will become
	`unique(Functors)', etc., with the arguments of `Functors'
	having the type information recursively propagated into the
	mode in the same manner.

Example:

	The io__stream example shown above would look like this:

		:- subtype yes < bool ---> yes.
		:- subtype no < bool ---> no.
		:- subtype text < text_or_binary ---> text.
		:- subtype binary < text_or_binary ---> text.

		:- subtype io__binary_stream < io__stream
			---> io__stream(binary, _, _, _).

		:- subtype io__text_stream < io__stream
			---> io__stream(text, _, _, _).

		:- subtype io__input_stream < io__text_stream
			---> io__stream(_, yes, _, _).

		:- subtype io__output_stream < io__text_stream
			---> io__stream(_, _, yes, _).

		:- subtype io__bidirectional_stream < io__text_stream
			---> io__stream(_, _, yes, _).


Comments?


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