Non-H98 crusade, contd.

[Keean Schupke]

Ross Paterson wrote:

>On Mon, Feb 28, 2005 at 12:40:42PM +0000, Keean Schupke wrote:
>  
>
>>Ross Paterson wrote:
>>
>>    
>>
>>>Where can I read this understanding?  The GHC docs on FDs are terse,
>>>referring to the original paper, but that paper is somewhat informal,
>>>and describes a weaker system than what is implemented.  For example,
>>>(taken from s7 of the paper), given
>>>
>>>	class U a b | a -> b where u :: a -> b
>>>	class U a b => V a b where v :: a -> b
>>>
>>>the paper says that the principal type of \x -> (u x, v x) is
>>>
>>>	(U a b, V a c) => a -> (b,c)
>>>
>>>According to GHC and Hugs, it is
>>>
>>>	V a b => a -> (b,b)
>>>
>>>I think that's sensible, but where are the rules that give it?
>>>I suspect that writing this addendum may take a while.
>>>
>>>      
>>>
>>Thats just a type simplification, in the source, we have
>>
>>\x -> (u x, v x)
>>
>>the type checker knows both x's are the same, and it knows
>>that (V a b) is the same as (U a b)...
>>
>>So in this case it looks like the second type is just a simplification
>>of the first... so they really agree on the type, not disagree.
>>    
>>
>
>No, the paper is clear on this point:
>"For example, given two predicates U a b and V a c, nothing in the rules
>from Section 6 will allow us to infer that b = c."
>
>I agree that they should be identified, but the type system that does
>it isn't written down anywhere (outside of the GHC and Hugs sources,
>and the Hugs version has a number of bugs).
>  
>
Sounds like someone ought to write a new paper?

    Keean.