[m-dev.] for review: MR_TypeInfo cleanup, part 3 (of 3)

Fergus Henderson fjh at cs.mu.OZ.AU
Thu Mar 23 02:07:09 AEDT 2000


On 23-Mar-2000, Tyson Dowd <trd at cs.mu.OZ.AU> wrote:
> On 22-Mar-2000, Zoltan Somogyi <zs at cs.mu.OZ.AU> wrote:
> > +** MR_create_type_info and MR_make_type_info both assume that all type
> > +** variables inside the given pseudo typeinfo are universally quantified.
> > +** Their maybe_existq variants do not make this assumption; they also work
> > +** if the pseudo typeinfo contains existentially quantified arguments.
> > +** This can happen only when the pseudo typeinfo describes the type of
> > +** an argument of a function symbol from a MR_TYPE_CTOR_REP_DU* type.
> 
> This makes me curious, since there is another place exist vars can occur.
> 
> What happens in the case of an existentially quantified type variable
> in a higher order type?  I'm not sure that we handle this.

Well, strictly speaking the comment in the code above is not correct; the
pseudo typeinfo could describe *part of* the type of an argument of a function
symbol from a d.u. type.

For example, for

	:- type foo --> some [T] f(list(set(T))).

we may end up recursively calling MR_create_type_info_maybe_existq() to
create the `set(T)' type.  Similarly for the `pred(T)' type in

	:- type foo --> some [T] f(list(pred(T))).

So the comment should be changed:
s/describes the type/describes the type (or a part thereof) of

However, if you're asking about existentially quantified higher-order
types, e.g.

	:- type foo --> f(list(some [T] pred(T))).	% not legal Mercury

then the answer is that we don't support them yet -- nor
do we support universal quantifiers there either:

	:- type foo --> f(list(all [T] pred(T))).	% not legal Mercury

Currently, higher-order terms are always monomorphic,
i.e. the type is determined at the point where you create
the higher-order term, not at the point where you call it.

Support for polymorphic higher-order terms (a.k.a. "first class polymorphism")
is needed only very rarely, and it is possible use type classes to achieve
the same effect (albeit with greater verbosity), so this is fairly
low on the priority list.

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



More information about the developers mailing list