[Haskell-cafe] Re: type families and type signatures
Tom.Schrijvers at cs.kuleuven.be
Mon Apr 7 12:33:02 EDT 2008
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
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.
> All the best,
> 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.
>> Tom Schrijvers
>> Department of Computer Science
>> K.U. Leuven
>> Celestijnenlaan 200A
>> B-3001 Heverlee
>> 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
Department of Computer Science
tel: +32 16 327544
e-mail: tom.schrijvers at cs.kuleuven.be
More information about the Haskell-Cafe