Hi all,
I believe there is a problem in the rule for instance declarations in
"A Static Semantics For Haskell" [1] because the premise which ensures
that instances for all superclasses are defined seems to hold
trivially. [2] seems to have the same problem.
I now describe the problem by showing how an incorrect program is
accepted by the rules given in [1]. I omit many, many details that are
irrelevant to this problem. Consider the following program:
class C a
class C a => D a
instance D Int
The instance environment IE for this program is built recursively by
the rule for modules bodies (Fig. 15) and looks like this:
IE = {forall a. D a => C a, D Int}
We would expect that the rule for instance declarations (Fig. 26)
rejects the program because there is no instance declaration for
C Int. However, the rule uses the *whole* instance environment IE to
check whether there is an instance declaration for C Int. But this
holds trivially, because we have D Int in IE and the
implication (forall a. D a => C a) lets us the conclude that
C Int holds!! In other words: The rule uses the implication
(forall a. D a => C a) to make sure that the very same implication is
valid for a = Int.
A possible solution might be to remove the constraint D Int before
checking whether C Int holds. However, I am not sure whether the
resulting rule is complete. An alternative solution would be to use
a weaker entailment judgment.
Any thoughts? Am I just missing some implicit condition on the
instance environment?
References:
[1] @Article{Faxen02,
title = "A static semantics for {Haskell}",
author = "Karl-Filip Fax{\'e}n",
journal = "Journal of Functional Programming",
year = "2002",
number = "4\&5",
volume = "12",
pages = "295--357",
}
[2] @Article{Hall1996,
author = "Cordelia V. Hall and Kevin Hammond and Simon L. {Peyton
Jones} and Philip L. Wadler",
title = "Type classes in {Haskell}",
journal = "ACM Transactions on Programming Languages and Systems",
volume = "18",
number = "2",
pages = "109--138",
year = "1996",
}
Cheers,
Stefan Wehr
--
Stefan Wehr
Web: http://www.stefanwehr.de
PGP: Key is available from pgp.mit.edu, ID 0B9F5CE4
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
