[mercury-users] invalid universal quantification example confuses me

[Fergus Henderson]

On 05-Jul-2001, Terrence Brannon <tmbranno at oracle.com> wrote:
> The manual does state:
> 
>   If a type variable in the type declaration for a polymorphic predicate
>   or function is universally quantified, this means the caller will
>   determine the value of the type variable, and the callee must be
>   defined so that it will work for all types which are an instance of
>   its declared type. 
> 
> :- pred foo(T).
> foo(_).
> % ok
> 
> :- pred bad_foo(T).
> bad_foo(42).
> % type error
> 
> But I don't see why the second case causes a type error:
> 1 - we are dealing with a predicate that is universally quantified
> 2 - therefore the caller (in this case bad_foo(42)) determines the
>     type of the type variable

In the clause `bad_foo(42).', bad_foo/1 is the callee, not the caller.

The call is another predicate (maybe yet written), which calls
bad_foo/1, e.g.

	main -->
		{ bad_foo("oops") }.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------