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: [EMAIL PROTECTED]
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@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: [EMAIL PROTECTED]
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
