[mercury-users] invalid universal quantification example confuses me

[Fergus Henderson]

On 09-Jul-2001, Terrence Brannon <tmbranno at oracle.com> wrote:
> I'm still not completely clear on this section of the manual.
> 
> Fergus Henderson writes:
>  : 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
> 
> Ok, is the below an example of "a type variable in the type
> declaration for a polymorphic predicate" :
> 
> :- pred distance(P1, P2, float) <= (point(P1), point(P2)).

That *contains* two examples of "a type variable in the type
declaration for a polymorphic predicate", namely "P1" and "P2".

>  : >   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 bad_foo(T).
>  : > bad_foo(42).
>  : > % type error
> 
> Ok, so applying the remainder of the paragraph to this errant code:
> 
> 1 - the callee is bad_foo/1 per the last email msg
> 2 - the caller is something like:
> 
> main ---> { bad_foo(42) }.
> 
> 3 - Please state the following:
> 
>   a - how is the caller determining the type of the type variable and
>   what is the outcome of this process? I am guessing that the caller
>   is determining that the type of the type variable is integer. 

The caller determines the *value* of the type variable.
Your guess that the value of this type variable is "integer" is
almost correct -- actually it is "int", not "integer".
The value of the type variable is determined by the constraints
placed on it; in this case, the argument of bad_foo is unified
with an int literal, which constrains that argument to have
type "int".

>   b - since bad_foo/1 doesn't do anything with its input argument, why
>   is it failing this requirement: "the callee must be defined so that
>   it will work for all types which are an instance of its declared
>   type."

bad_foo/1 *is* doing something with its argument;
it is unifying it with the int literal 42.
This requires that the argument have type "int".
It will happen to work for this particular call from main/2,
but the compiler rejects the definition of bad_foo/1 because
it won't work for all types which are an instance of its
declared type.  If main/2 was written differently, e.g. as

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

then you'd be able to see the problem more clearly --
the argument would have type "string", but the callee bad_foo/1
would try to unify that with the value 42, which has type "int".

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