[m-rev.] for discussion: subtypes documentation

[Mark Brown]

Here's a new form of subtype declaration for discussion: subtypes with an
implicit supertype.  The declaration

	:- subtype t(P_i)		---> f_j(s_k).

where each s_k is a subtype of some t_k, is equivalent to the
declarations:

	:- type t_base(P_i)		---> f_j(t_k).
	:- subtype t(P_i) < t_base(P_i) ---> f_j(s_k).

The body of the implicit supertype t_base is just the body of the
subtype except that all types have been replaced by the base type.

(Also, the name of the implicit supertype could be the same as the
subtype without any serious ambiguity.  Any reference to the name
would refer to the subtype if subtypes are legal at that point,
otherwise it would refer to the supertype.  If the user needs full
access to the supertype, they will have to declare it explicitly.)

On 25-Nov-2002, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> I think we should allow subtypes in the bodies of type definitions.
> Otherwise, subtypes would be too much second-class citizens.
> 
> Here is a proposed semantics for them.  For a discriminated union definition
> which has parameters P_1, P_2, ..., P_n
> (think of "_" as the Latex subscript operator ;)
> and which uses subtypes s_1 < t_2, s_t < t_2, ..., s_m < t_m,
> the type definition will be of the form
> 
> 	:- type t(P_i) ---> f_j(... s_k ...).
> 
> (That is, it will be of the form
> 
> 	:- type t(P_1, ..., P_n) ---> f_1(...) ; f_2(...) ; ... ; f_m(...).
> 
> where the s_k occur somewhere in the body of the type definition.)
> We can define the semantics of this to be equivalent to
> 
> 	:- type t_base(...)             ---> f_i(... t_j ...).
> 	:- subtype t(...) < t_base(...) ---> f_i(... s_j ...).
> 
> where t_base/n is a fresh name not occurring in the program.

As you can see, our proposals are identical except that mine uses
"subtype" where yours uses "type".

Why do I think it should be a subtype declaration rather than a type
declaration?  Because each subtype declaration effectively declares both
a type and an inst, whereas type declarations only declare a type.  The
new form of declaration will effectively declare both a type and an inst,
so it is better to think of it as a subtype, not a type.

With implicit supertypes, subtypes should feel a lot less like
second-class citizens.

Cheers,
Mark.

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