To my suggestion on deduced contexts
Jeffrey R. Lewis <[EMAIL PROTECTED]> writes
L> Let's take f again, as you've typed it:
L> f :: Eq a => a -> Bool
L> f x = Just x == Just x
L> [..]
L> Would it make sense at this point for the compiler to
L> say, "heck, I don't know why he put `Eq a' in the context, what he
L> really needs is `Eq (Maybe a)'", and just correct the programmer's
L> error for him?
M> More expanded:
M> "Eq a means all the infinitely many things that can be deduced
M> from this according to all the visible instances.
M> [..]
L> The problem is this: it would be
L> inconsistent to deduce `Eq (Maybe a)' from `Eq a', given the
L> overlapping instance `Eq (Maybe Bool)'
L> [..]
??
If it is inconsistent, why the existing compilers issue an error
report on the initial program
(in the presence of instance Eq (Maybe Bool) ...),
force the user to add `Eq (Maybe a)', and then compile new program
successfully?
It looks like there is some great confusion.
Maybe, the matter is in terminology: "deduced context",
"dictionary" ... - I am not sure that I use these terms as the
Haskellites expect.
Maybe, it is due to that your note refers to some larger program,
not only of these 3-4 lines.
The subject becomes totally unclear to me.
Maybe, we try to fix it?
By `deducing' I mean mere adding `Eq (Maybe a)' to context.
The resolution of which dictionary value to pass is another matter,
performed at the later stages.
(?)
Maybe, the whole answer have to be corrected:
Eq a should mean all the infinitely many things that follow
from this according to all the visible items and instances
and - according to the fixed rules (part of language) for
resolving the overlapping instances.
Similar are other kinds of context.
Value type context declaration meaning ===
deduction consequences + overlap resolution by rules,
all this considered within the given scope.
In this sense, I suggest that the meaning of a program in scope is
unique.
Right?
For the first stage, I propose for the compiler only to add the
necessary deduced contexts (without adding dictionary values).
The overlap resolution happens at the next stages.
Thus, you consider the example like
f :: Eq a => a -> Bool
f x = Just x == Just x
instance Eq (Maybe Bool) where (Just x)==(Just y) = x==(not y)
...
Do you agree to set this example?
I suggest for the compiler to act as follows.
Stage 1.
Deduce all the needed contexts from the body of f and from
the visible instance overlaps.
For this example, it deduces the context Eq (Maybe a) from
the body of f, from the visible instance overlap made by
`Eq a =>', standard instance for Maybe, and the user instance
for Maybe Bool.
Add the deduced thing to the declaration:
f :: (Eq a, Eq (Maybe a)) => a -> Bool
f x = Just x == Just x
instance Eq (Maybe Bool) ...
Stage 2.
Compile the new program as the existing compilers can.
------------------
The user remains to see only the old F.hs - with the old context.
And the produced interface module is not supposed to be read by
the user.
It says "and from the visible instance overlap ...",
because without finding the overlap, the Stage 2 is able to
compile the initial program directly.
By `deducing the context' at Stage 1 I mean only adding things
like `Eq (Maybe a)' to initial program.
I think that at this particular program PP, the instance overlap
is * detected but not resolved *.
The local dictionary *variable* eqMb is only inserted into
f_compiled.
Do I mistake?
Suppose, further, it is set the program PP': g1 = f 'b'
g2 = f True
For the program PP', the compiler really resolves the overlap.
It assigns the values for eqMb in the occurrences of f_compiled.
In g1, f_compiled receives
eqMb = one coming from standard instance Eq a=> Eq (Maybe a)...
In g2, f_compiled receives
eqMb = one coming from the user's instance Eq (Maybe Bool)...
Please, is this correct in main?
If yes, then why you say
L> inconsistent to deduce `Eq (Maybe a)' from `Eq a', given the
L> overlapping instance `Eq (Maybe Bool)'
?
Probably, the above agrees badly with what I wrote in the previous
letter
M> "Eq a means ...
M> But now, I have to care only of the ones that are really used in
M> f. And I discover that it uses Eq a => Eq (Maybe a)
M> [..]
I am sorry, let the version in *this letter* be actual.
> Besides, I think there's a better solution, unrelated to overlaps.
>
> I think what you really want is some form of wildcard in signature
> contexts, as I mentioned previously. That's on my wish list as well.
After somebody explains what does this mean, I may hope to tell
whether I am going to need it.
------------------
Sergey Mechveliani
[EMAIL PROTECTED]
