[m-dev.] Suggestion: default func-type/mode correspondence.

[Ralph Becket]

> From: Fergus Henderson [mailto:fjh at cs.mu.OZ.AU]
> Sent: 23 July 2001 13:20
> 
> What should happen if `T' is an abstract equivalence type that is
defined
> 	(a) in the same module as `foo'
> or	(b) in some other module
> as being equivalent to a higher-order function type?
> 
> I would not be suprised if the current compiler gets that wrong,
> e.g. allowing mode-incorrect code to compile and crash at runtime.

The idea is that the refinement would occur at the call site.  If the
call site doesn't know the concrete type of X then it can't perform
inst refinement on the returned value.  However, should quantity X
ever be returned to a site that does know its type then it can have
its inst refined.

Can you give an example where a mode problem could arise?

> > I propose that the second clause for @ be changed to recurse over
> > known data types so that, for instance, the following would work:
> >
> > :- type t(T) ---> [] ; [func(T) = T | t(T)].
> >
> > :- func f(t(T), T) = list(T).    % No need for explicit modes.
> 
> This might be a good idea.  But I don't see how to make the same thing
work for
> abstract types, unfortunately.
> 
> 	:- func g(t(T), T) = set(T).    % Explicit modes needed here,
> 					% because `set/1' is an abstract
type.

No, we just use the default rule inferring

	:- mode g(in(t), in) = out is det.
where	:- inst t ---> [] ; [func(in) = out is det | t].

At a call site such as

	Y = g([X1, ...], X)

where X1 has type int_to_int, ..., X has type int_to_int
where	:- type int_to_int == (func(int) = int).

we know that Y has type set(int_to_int) and has unrefined return
inst of ground, hence we can refine its return inst to t.

> If we make things easier with concrete types but not with abstract
types,
> then that will encourage people to use concrete types rather than
> abstract types, and so I'm not sure that it would be a win overall.

I'd like to avoid that too, but so far I can't see a problem with this
idea.  Right now abstract types bearing functions are unbelievably hard
to work with anyway.

> > We can extend the idea to get a simple version of parametric modes
> > for funcs as follows: if we call a func or pred with an argument
> > whose type we know, but whose inst is ground after the call, then
> > we can use the @ operator on its type to refine its inst and recover
> > any func mode information.
> 
> This is not safe in the presence of univ__to_type and friends.

Since you couldn't do anything with what univ__to_type etc. would
return, it seems safe to me to make such a call an error.

> > For this to work we have to forbid the
> > return of any ground func object that does not have the inst that @
> > would construct for its type (that is, if X has type func(T1, ...) =
T
> > but its inst I is not the same as @(func(T1, ...) = T) then we
forbid
> > inst transitions of the form I >> ground.
> 
> How can you forbid that, when for polymorphic procedures the exact
type
> their arguments is not know until runtime?
> Are you suggesting a run-time check??

Good grief no - I'm not suggesting a run-time check!

We can check this statically.  The compiler can identify the point at 
which a func containing object is passed as a polymorphic parameter
and flag an error.  Why would the programmer ever want to do such a
thing?

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