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

[Tom Schrijvers]

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