[mercury-users] invalid universal quantification example confuses me

[Terrence Brannon]

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

I believe so, but if I am wrong about this, then I have no hope of
understanding the rest of the paragraph.

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

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

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