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

Tom Schrijvers Tom.Schrijvers at cs.kuleuven.be
Mon Apr 7 12:33:02 EDT 2008

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

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

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