[mercury-users] typeclass error

[Ian MacLarty]

On 19 Jan 2006, at 14:00, Mark Brown wrote:

> On 19-Jan-2006, Ian MacLarty <maclarty at cs.mu.OZ.AU> wrote:
>> On 19 Jan 2006, at 05:39, Mark Brown wrote:
>>
>>> On 18-Jan-2006, Ian MacLarty <maclarty at cs.mu.OZ.AU> wrote:
>>>> Hello,
>>>>
>>>> What's wrong with the following program?
>>>>
>>>> :- module tc.
>>>>
>>>> :- interface.
>>>>
>>>> :- import_module io.
>>>>
>>>> :- pred main(io::di, io::uo) is det.
>>>>
>>>> :- implementation.
>>>>
>>>> :- import_module list, int.
>>>>
>>>> main(!IO) :-
>>>>        nl(!IO).
>>>>
>>>> :- typeclass tc1(A, C) where [
>>>>        func a_to_c(A) = C
>>>> ].
>>>>
>>>> :- typeclass tc2(B, C) where [
>>>>        func b_to_c(B) = C
>>>> ].
>>>>
>>>> :- func f(A, B) = C <= (tc1(A, C), tc2(B, C)).
>>>>
>>>> f(A, B) =
>>>>        ( if a_to_c(A) = b_to_c(B) then
>>>>                a_to_c(A)
>>>>        else
>>>>                b_to_c(B)
>>>>        ).
>>>
>>> First, here's the clause with some explicit type annotations:
>>>
>>> 	f(A, B):C0 =
>>> 		( if a_to_c(A):C1 = b_to_c(B):C2 then
>>> 			a_to_c(A):C3
>>> 		else
>>> 			b_to_c(A):C4
>>> 		):C5.
>>>
>>> Because of the result unification, we know that C0 = C5.  Because of
>>> the
>>> semantics of if-then-else expressions, we know that C3 = C5 and C4 =
>>> C5.
>>> Because of the unification in the condition, we know that C1 = C2.  
>>> So
>>> at
>>> this stage there are two equivalence classes: {C0,C3,C4,C5} and
>>> {C1,C2}.
>>> There is nothing in the clause which implies that these two 
>>> equivalence
>>> classes are the same.
>>>
>>> The first equivalence class is the type of the function result, so it
>>> is
>>> bound to the universally quantified C from the func declaration.  
>>> Hence
>>> the method calls in the "then" and "else" branches will call methods 
>>> in
>>> those dictionaries that are passed in as hidden arguments to f (that
>>> is,
>>> the dictionaries that correspond to the two constraints on the func
>>> declaration).
>>>
>>> The second equivalence class remains unbound.  Hence there are no
>>> assumed
>>> constraints (e.g., constraints on the func declaration) that can
>>> satisfy
>>> the constraints on the method calls in the condition; this explains 
>>> the
>>> first part of the error message.  The warning you get is because
>>> unbound
>>> type variables are generally never what the programmer intends.
>>>
>>
>> That all makes perfect sense.  I was under the illusion that the
>> compiler would know that C1 and C3 are of the same type, because they
>> have the same value, but I guess type inference doesn't know anything
>> about the values.
>
> Without the functional dependency, they wouldn't necessarily have the 
> same
> value, let alone the same type.  ;-)
>
> Consider:
>
> 	:- typeclass convertible(A, B) where [
> 		func cast(A) = B
> 	].
>
> 	:- instance convertible(int, int) where [
> 		(cast(N) = N)
> 	].
>
> 	:- instance convertible(int, string) where [
> 		(cast(_) = "some number")
> 	].
>
> 	main(!IO) :-
> 		io.write_string(cast(1), !IO),
> 		io.nl(!IO),
> 		io.write_int(cast(1), !IO),
> 		io.nl(!IO).
>
> The output would be:
>
> 	some number
> 	1
>
> You should think of cast/1 as being an overloaded name, which is why it
> appears to violate referential transparency.
>

Good point.

Ian.

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