[m-dev.] for review: support constructions for existential data types

[David Glen JEFFERY]

On 08-Jul-1999, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> 
> Estimated hours taken: 5
> 
> Allow construction unifications for existentially typed functors,
> using the syntax "X = 'new foo'(Y)" rather than the usual "X = foo(Y)".
> We need to use a special syntax for exisentially typed constructions
> because type analysis and polymorphism need to know which occurrences
> of existentially typed functors are constructors and which are deconstructors.
> 
> Note that we still don't yet support RTTI for existentially typed data types.
> 
> compiler/typecheck.m:
> 	For existentially typed functors, allow the functor to have
> 	a "new " prefix, and if so, make the quantifiers and constraints
> 	universal rather than existential.
> 
> compiler/polymorphism.m:
> 	For unifications with existentially typed functors,
> 	check for a "new " prefix on the functor.
> 	If the functor has such a prefix, strip off the prefix,
> 	and treat the unification as a construction rather than
> 	treating it as a deconstruction.
> 
> compiler/modecheck_unify.m:
> 	For construction unifications, check that all the type_info
> 	and typeclass_info arguments introduced by polymorphism.m
> 	are ground.
> 
> tests/hard_coded/typeclasses/existential_data_types.m:
> 	Change the test case to use this new feature,
> 	rather than hacking it using the C interface.
> 
> doc/reference_manual.texi:
> 	Document the new features.

> Index: compiler/typecheck.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
> retrieving revision 1.259
> diff -u -r1.259 typecheck.m
> --- typecheck.m	1999/06/30 17:12:42	1.259
> +++ typecheck.m	1999/07/07 17:06:20
> @@ -3168,6 +3168,41 @@
>  	;
>  		ConsInfoList0 = []
>  	),
> +
> +	% For "existentially typed" functors, whether the functors

s/the functors/functors/

> + at example
> +:- type list_of_any
> +	---> nil_any
> +	;    some [T] cons_any(T, list_of_any).
> +
> +:- typeclass showable(T) where [ func show(T) = string ].
> +:- type list_of_showable
> +	---> nil
> +	;    some [T] (cons(T, list_of_any) => showable(T)).

It is probably worth putting an example like this here too:


:- type showable ---> some [T] (s(T) => showable(T)).

:- type list_of_showable == list(showable).

> +are inverses: when constructing a value of an existentially quantified
> +data type, the ``existentially quantified'' functor acts for purposes
> +of type checking like a universally quantified function: the caller
> +will determine the value of the type variable.
> +Conversely, for deconstruction the functor acts like an
> +existentially quantified function: the caller must be defined so
> +as to work for all types which are an instance of the declared type.

`instance of the declared type' isn't too clear.

Otherwise, that diff is fine. Thanks, Fergus!


dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) | If your thesis is utterly vacuous
PhD student,                    | Use first-order predicate calculus.
Dept. of Comp. Sci. & Soft. Eng.|     With sufficient formality
The University of Melbourne     |     The sheerist banality
Australia                       | Will be hailed by the critics: "Miraculous!"
                                |     -- Anon.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------