[Haskell-cafe] Re: type families and type signatures

[Tom Schrijvers]

On Mon, 7 Apr 2008, Mark P Jones wrote:

> The surprising thing about this example is the fact that
> the definition of foo is accepted, and not the fact that
> the definition of foo' is rejected.  At least in Manuel's
> "equivalent" program using functional dependencies, both
> functions have ambiguous types, and hence both would be
> rejected.  It sounds like your implementation may be using
> a relaxed approach to ambiguity checking that delays
> ambiguity checking from the point of definition to the
> point of use.  Although this is probably still sound, it
> can lead to puzzling error diagnostics ...

On the algorithmic level I don't see a relaxed approach to ambiguity 
checking.

If alpha is a unifiction variable, you get for the first body

 	(Id a -> Id a)  ~ (alpha ~ alpha)

where there is no ambiguity: the unique solution (modulo equality 
theory) is alpha := Id a.

For the second body you get

 	(Id a -> Id a) ~ (Id alpha -> Id alhpa)

This equation reduces to Id a ~ Id alpha. Our algorithm stops here. There 
is in general no single solution for alpha (*) in such an equation, as 
opposed to the above case.

I hope this clarifies our algorithm.

Cheers,

Tom

> All the best,
> Mark
>
> Tom Schrijvers wrote:
>>>>> type instance Id Int = Int
>>>>> 
>>>>> foo :: Id a -> Id a
>>>>> foo = id
>>>>> 
>>>>> foo' :: Id a -> Id a
>>>>> foo' = foo Is this expected?
>>>> 
>>>> Yes, unfortunately, this is expected, although it is very unintuitive. 
>>>> This is for the following reason.
>>> 
>>> Huh? This sounds very wrong to me, simply because  foo  and  foo'  have 
>>> the very same type.
>> 
>> Type systems reject programs that don't go wrong. It's hard to understand 
>> on the basis of such a single program why it should be rejected. The 
>> problem is decidability. There is no algorithm that accepts all 
>> well-behaved programs and rejects all ill-behaved programs. There probably 
>> is an algorithm that accepts a particular program.
>> 
>> So far we haven't found an algorithm that accepts this example, that is 
>> decidable and sufficiently general to cover many other useful cases. This 
>> is our motivation for rejecting this program.
>> 
>> Consider it a challenge to find a better algorithm in the design space.
>> 
>> Cheers,
>> 
>> Tom
>> 
>> -- 
>> Tom Schrijvers
>> 
>> Department of Computer Science
>> K.U. Leuven
>> Celestijnenlaan 200A
>> B-3001 Heverlee
>> Belgium
>> 
>> tel: +32 16 327544
>> e-mail: tom.schrijvers at cs.kuleuven.be
>> url: http://www.cs.kuleuven.be/~toms/
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: tom.schrijvers at cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/