To my suggestion on deduced contexts in overlaps
Jeffrey R. Lewis <[EMAIL PROTECTED]> writes
> Let's take f again, as you've typed it:
>
> f :: Eq a => a -> Bool
> f x = Just x == Just x
> [..]
> Would it make sense at this point for the compiler to
> say, "heck, I don't know why he put `Eq a' in the context, what he
> really needs is `Eq (Maybe a)'", and just correct the programmer's
> error for him?
Yes, it should think like this. More expanded:
"Eq a means all the infinitely many things that can be deduced
from this according to all the visible instances.
--------------------------------------------------------------
But now, I have to care only of the ones that are really used in
f. And I discover that it uses Eq [Bool].
But the instance (dictionary) for Eq [Bool] can be deduced in
multiple ways! The first is the standard `deriving'. The second
deduces from the user instance.
But I have certain wise rules to resolve the choice ... Done!
I add the deduced context to declaration and continue compilation.
I keep mum: the user should not know of all this my private
business.
The source program F.hs remains with `Eq a =>'.
I compiler another, "corrected", auxiliary program.
I create the interface module which *may contain* the deduced
context, and other things too. But the interface modules are not
for the ordinary user to read.
"
> I'm afraid if you agree to that, then I'm afraid
> you're also stuck with this:
>
> f :: Eq a => a -> a -> Bool
> f = (>)
>
> What should the compiler do now? Should it say "heck, I don't know
> why he put `Eq a' in the context, what he really needs is `Ord a'?
Very naturally. Only it has to continue:
"The program pretends Ord a to be a consequence of Eq a.
I have to find, in what way ... I look for the relative visible
instances to deduce it from them ...
but I fail to find such deduction!
The visible instances do not look to be enough for this.
Report an ERROR: cannot deduce Ord a needed in f ...
"
It should try to deduce it by the simple rules, we all know of.
If it fails, it reports the fail.
The whole matter is that the *meaning* of Eq a
and (Eq a,Eq [a],Eq [[a] ...)
should be (I suggest to be) the same
- if the related instance is in scope.
I suggest for the language:
Eq a should mean all the infinitely many things that follow
from this and from all the visible instances.
Similarly - with other contexts.
And what the implementors speak of the necessity to add Eq [a] ...
in one or another situation with overlaps
- this has to be only one of the possible compilation ways.
The compiler should not discuss with the user its compiler's
problems, if they can be solved automatically.
Let us distinguish between the *unique* meaning of the program and
various possible compilation techniques.
Usually, it is good for the user not to think of possible
compilation ways. The user has enough problems of one's own.
Writing possibly short program (and suffering of that it comes out
large), one expects it to give the correct results. And this is all.
The user does not care what the intermediate auxiliary clever
finite list of contexts and dictionaries, and so on, the compiler
would deduce in one or another situation.
The compiler has to help the user to write possibly shorter, simpler
program.
Suppose, we are reading a book on mathematics:
Axiom: for each set x and an integer n
if x is finite then x++{n} is finite.
Theorem: if x is a finite set then <Statement(x)>,
and f x can be computed in such and such way.
Computation Method for such and such map g = (\x ->...):
for a finite set x, let y = f ((x++{1})++{2}) in ...
So, g declares finite(x), and uses finite (x++{1}) ...
Do you suggest me to write to the book author
"you forget to add
`and finite(x++{1}) and finite ((x++{1})++{2})'
"
?
This is not a mathematical error. But the author may get irritated
and prosecute me, probably, via Interpol.
And the recent implementations, they say sometimes things like
"Error: you forget to add Eq [[a]] ...".
>> f :: (Eq a) => Int -> a -> a -> Int
>> f n x y =
>> if n==0 then 0
>> else if x==y then n else f (n-1) [x] [y]
>>
>> main = let r = f 100 True False in putStr $ shows r "\n"
>>
>> instance Eq [[[[[[[Bool]]]]]]] where x==y = (length x)==(length y)
>> [..]
>> * adding only Eq [[[[[[[a]]]]]]] would not suffice
>> * if the extra instance shows n
>> brackets, the forced type context has to contain about (n^2)/2
>> of them.
> Oddly enough, this sort of thing just hasn't come up when I use
> overlapping instances ;-)
> Yes, that's nicely pathological, but is it a real problem?
It is NOT a real problem.
Just a small technical obstacle.
But it leads to a bit of ugly style.
When a thing does not look nice, it has less chances to get into
the language standard.
The application programs look more lengthy - this is bad.
I use essentially the overlaps in my CA program. They help a lot.
And I want them to get into the language standard.
But the existing implementations often force me to write the things
like (Field a, Ring (ResidueE (Pol a)) =>
instead of plain (Field a) =>
The compiler has to help to write easy to read programs.
The teachers of the handicraft say:
"do it the best way from the start, for it would get to bad outcome
itself".
BUT: if people show that this *deduced context* approach leads to
some great inconsistensy, then one has to think of other means, or
just give up and remain as it is.
The strongest objection I observed so far was that it agrees badly
with writing programs to link to the object libraries given without
sources. With overlaps, the interface module export types may start
to depend on the single `import A' declaration.
It will be harder to satisfy the linkage of this to the shared
library.
I consider such a case as esoteric, personally, fear to think of any
program without source:
how can one fix a bug in them, if their developers had quitted the
support?
And if one aims to link the program to object library and has not
the sources for this library, all right, avoid overlapping
instances.
------------------
Sergey Mechveliani
[EMAIL PROTECTED]
