[Haskell-cafe] type families and type signatures
martin.sulzmann at gmail.com
Fri Apr 11 04:32:29 EDT 2008
Lennart Augustsson wrote:
> On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann
> <martin.sulzmann at gmail.com <mailto:martin.sulzmann at gmail.com>> 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?
> 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
> 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
> 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
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
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
which takes into account matching. Therefore, (**) is checkable in
BUT matching can be fairly expensive, exponential in the worst case, for
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?
More information about the Haskell-Cafe