Lennart Augustsson wrote:
On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann
<[EMAIL PROTECTED] <mailto:[EMAIL PROTECTED]>> wrote:
Lennart, you said
(It's also pretty easy to fix the problem.)
What do you mean? Easy to fix the type checker, or easy to fix the
program by inserting annotations
to guide the type checker?
Martin
I'm referring to the situation where the type inferred by the type
checker is illegal for me to put into the program.
In our example we can fix this in two ways, by making foo' illegal
even when it has no signature, or making foo' legal even when it has a
signature.
To make it illegal: If foo' has no type signature, infer a type for
foo', insert this type as a signature and type check again. If this
fails, foo' is illegal.
To make it legal: If foo' with a type signature doesn't type check,
try to infer a type without a signature. If this succeeds then check
that the type that was inferred is alpha-convertible to the original
signature. If it is, accept foo'; the signature doesn't add any
information.
Either of these two option would be much preferable to the current
(broken) situation where the inferred signature is illegal.
I understand now what you meant. See my earlier reply to Claus' email.
Regarding your request to take into account alpha-convertibility when
checking signatures.
We know that in GHC the check
(forall a, b. Foo a b => a) <= (forall a, c. Foo a c => a) (**)
fails cause when testing the constraint/formula derived from the above
subsumption check
forall a, b. Foo a b implies exists c. Foo a c
GHC simply drops the exists c bit and clearly
Foo a b does NOT imply Foo a c
We need to choose c to be equal to b. I call this process "matching" but
it's of course
a form of alpha-conversion.
(We convince GHC to accept such signatures but encoding System F style
type application via redundant type proxy arguments)
The point I want to make is that in Chameleon I've implemented a
subsumption check
which takes into account matching. Therefore, (**) is checkable in
Chameleon.
BUT matching can be fairly expensive, exponential in the worst case, for
example
consider cases such as Foo x_i x_i+1
So maybe there's good reason why GHC's subsumption check doesn't take
into account matching.
The slightly odd thing is that GHC uses a "pessimistic" subsumption
check (no matching) in combination
with an "optimistic" ambiguity check (see my earlier message on this topic).
I'd say it's better to be pessimistic/pessimistic and
optimistic/optimistic, maybe this could be
a compiler switch?
Martin
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
