To my notes on the overlapping instances and deduced contexts
Marcin 'Qrczak' Kowalczyk <[EMAIL PROTECTED]> writes
on 29 Feb 2000
>> If we want the recent implementations to compile this as needed, we
>> have to write
>> g :: (Eq a, Eq (Maybe a)) => (a -> Bool) -> [a] -> [Bool]
>> ------------
>> g h xs@(x:_) = (Just x == Just x) : map h xs
>>
>> - "because this g uses Eq (Maybe a)".
> It can't be. First, with polymorphic recursion the function uses an
> unbounded number of instances, and the context must be finite.
This Eq (Maybe a) have to add here only if
(in the mentioned example) instance Eq (Maybe Bool) ...
is in the scope where g compiles.
If it is not in the scope, I expect, it would suffice mere
g :: Eq a => (a -> Bool) -> [a] -> [Bool]
g h xs@(x:_) = (Just x == Just x) : map h xs
This is all due to the detected overlap of the two Eq instances for
Maybe that Eq (Maybe a) has to add.
> [..] First, with polymorphic recursion the function uses an
> unbounded number of instances, and the context must be finite.
What about concrete example?
You had provided certain example, with Eq [[[[[[[String]]]]]]] ...
- was it of polymorphic recursion?
But it can be handled by the existing compilers.
The method is evident. The instance with depth n of [,] causes n
additional contexts - *finitely many*.
One program cannot contain infinitely many instances, nor an
instance showing infinitely many constructors applied.
The instance may contain Eq [[[a]]] ...
but not Eq [..infinitely many..[[a]] ...]
>> I propose for the user to remain with `Eq a =>'.
>> Let the compiler itself deduce and add the needed context.
> No, no, no.
>
> Would the function really have the type that is specified, or the
> one with extended context?
> [..]
You may put: one with extended context. See below.
> If the latter, it is confusing. You say that a function having an
> explicit type signature will have a different type? So what is
> the reason of writing type signatures if they are false?
Probably, the type context means something different from what you
assume. The programs f :: Eq a => a -> Bool
f x = (Just x)==(Just x)
and
f :: (Eq a, Eq (Maybe a)) => a -> Bool
f x = (Just x)==(Just x)
may have the same meaning
- it depends on the scope (like the meaning of almost all things
in Haskell): visible items, instances, and so on.
This is similar like in mathematics the algorithm descriptions
" for a finite set x let f x = cardinality (union x {1}) "
and
" for a finite set x, and (union x {1}) being a finite set,
let f x = cardinality (union x {1})
"
have the same meaning.
The second description has sense but looks a bit stupid, and
naturally, it is good to omit
" and (union x {1}) being a finite set "
- preserving the meaning of the method.
One can replace one description with another, and this would not
change neither the result of computation of this f, nor even the
way of computation.
Let us say that these programs have the same *meaning*.
Returning to the Haskell programs, we have to put that the compiler
has right to change the program to any that has the same meaning -
to (strongly) equivalent one.
Example.
Consider the programs
(1) f :: Eq a => a -> Bool
f x = x==x
------------------------
(2) f :: (Eq a, Eq [a]) => [a] -> Bool
f x = x==x
------------------------
(3) f :: (Eq a, Eq [a], Eq [[[[a]]]]) => [a] -> Bool
f x = x==x
------------------------
(4) f :: (Eq a) => [a] -> Bool
f x = [[x]]==[[x]]
------------------------
(5) f :: (Eq a, Eq [[a]]) => [a] -> Bool
f x = [[x]]==[[x]]
Then, under the Standard Scope, (1),(2),(3) mean the same,
(4) and (5) mean the same.
If it is not true, then maybe, Haskell needs improvement - right?
You say "has a different type".
According to the proposed notion, different type descriptions in
the source program may have the same *meaning*.
Saying "has a different type", do you mean "different meaning"?
Now, add to the scope
instance Eq [[Bool]] where
(xs:_)==(ys:_) = (head xs)==(not $ head ys)
I believe, (1),(2),(3) should remain equivalent.
And I think that (4) should be equivalent to (5).
But the existing compilers pretend that (4) contains an error.
Reason: instance Eq [[Bool]] .., Eq a,
instance Eq a => Eq [a] ..
together present certain overlap - we spoke of this in earlier
letters.
I suggest to improve the language: to put that (4) and (5) have the
same meaning:
`Eq a' means everything that follows from `Eq a' and all the items
(and instances) in the scope.
I do not know, maybe, the language report already allows such
interpretation?
The compilation technique can support easily this meaning:
instead of reporting error, add the context that was found for
overlap and was said to cause the error. Then, compile as usual.
And the overlap is resolved at the further compilation stage,
according to certain rules (fixed part of the language).
What is wrong here?
> The type describes how a function can be used. If I know the type, I
> know which parameters it will (statically) accept and what information
> it needs. This is a purpose of types and should not be broken.
It looks like it is not broken.
If you see, how it is broken, please, show an example.
> Second, I don't want my programs to be big and slow only because
> somebody wanted an extension which caused the compiler to pass 10
> instances instead of 2 to my functions (that don't use the extension
> of overlapping instances).
And this would not happen. This may touch only the situation when
the instance overlaps are visible and relate to the body of a
function being compiled.
Using not overlapping instances, one does not have to care.
Further, with the overlaps, it would run not worse than the user
program "asks".
> Third, it does not work well with local universal quantification:
> data A = A (forall a. Eq a => [a] -> a)
> [..]
> Fourth, it does not work well with local existential quantification:
> data E = forall a. Eq a => E a (a -> [a])
> [..]
Probably, the overlapping instances have to be first investigated
with ignoring the possibility of local universal quantification and
local existential quantification -
if the latters really present an obstacle.
One cannot solve any problem keeping in mind all the Haskell
language.
>> Finally, I continue suggesting what I call *deduced context*.
> It has been discussed. It could be convenient. Possibly not only in
> contexts, but also in parts of types.
>
> However it would not prevent the poor compiler from being required to
> pass all these dictionaries at runtime, even if it makes a little sense
> because I will certainly not redefine equality on (String,Int) etc.
The compiler aiming to support real applications cannot be poor.
And for a poor compiler, it is natural to implement only some modest
subset of Haskell-98: no overlaps, no multiple class parameters ...
>> In brief, is has to support the overlapping instances like for the
>> class Cast a b. Defining its instances (together with certain
>> compiler pragma) gives a nice tool for the user to set the implicit
>> domain casting.
> I believe that C++ allows only one user defined type conversion at
> a time because the general problem of finding a path of conversions
> is undecidable. Cast a b with instances like
> instance (Cast a b, Cast b c) => Cast a c where cast = cast . cast
> is even more general and I'm sure that the whole thing gets undecidable.
Only easily decidable cases would help a lot - when the user avoids
rather generic instances that somehow compose in cycles.
And when the compiler fails, it reports an error.
Then the user defines something less ambiguous. And so on.
> Moreover, it is very easily ambiguous. Even if various possibilities
> would yield the same result, the compiler can't prove it.
It should not be supposed to prove it.
> IMHO designing a set of complex rules of choosing the best way
> among several valid ways is a path to nowhere (and simple rules
> will not do). It's a mess, especially if added to such powerful
> system as Haskell's [..]
Well, the braver user is, the richer instance overlaps one sets.
You have the right to avoid overlaps at all.
When I feel, that the rich casting between the domains is highly
needed, I risk with overlapping instances, even with the two
parameters, and see how it behaves ...
By the way, the overlapping instances of Cast a b do work in my
recent program.
Some attempts had lead to the ambiguity and compile errors.
Therefore, I defined less casting instances, more modest than
initially aimed. For example, I had to reject the nicely looking
instance (Cast a b,Cast b c)=> Cast a c where cast = cast .cast
And still it helps a lot in practice.
Probably, developing this feature is a matter of investigation.
I do not believe in your total denying.
> Remember: today about the only place in Haskell where the compiler
> resolves an ambiguity itself without reporting an error, [..]
Even when it merely reports an ambiguity error, it is often useful.
Guessing of the possible restrictions to put, the user often gets,
by and by, to the consistent program.
>> Such a casting is of great importance, at least, in computer algebra.
>> It is a pity that, due to the overlaps lack, my recent CA program
>> is not able to support this cast.
> I'm afraid that such casting is incompatible with Haskell, or even
> impossible to be sanely expressed in any language.
The situation is different.
The existing overlap policy, even for the two-parametric classes,
allows certain practically useful instance system for the domain
casting.
The problem is:
what change for the overlap resolution rules to undertake in order
to increase the expressive power of casting, but to avoid the
situation when the ambiguity starts to arise too often.
>> 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 ...
> No: if there is the standard 'deriving', a user instance is illegal.
> There is no choice. I say exactly what I mean and expect the compiler
> to do exactly what the program means.
Discussed is the language with overlapping instances.
Without overlapping instances in the scope, the question of deducing
contexts do not arise.
With overlapping instances, the meaning of the program is also
fixed.
>> Let us distinguish between the *unique* meaning of the program and
>> various possible compilation techniques.
> With overlapping instances there is no unique meaning. (The compiler
> does not know whether several user instances yield the same result.)
??
First, there exist a unique meaning:
it is defined by all the items, instances in the scope,
and by certain fixed rules (part of language) to resolve the
overlapping instances.
Second, what to you mean by "same result" ?
Each instance leads to the result the user intended.
The overlap is resolved according to fixed rules.
And it was pointed out in earlier letters that it is not natural for
the user to define overlapping with operation op,
that may return op x = 1 and op x = 2 depending on what
instance works. Such examples, usually appear only for *testing*.
Finally, if the user still defines it so, then this means one
*wants* to consider the results 1 and 2 as equivalent.
This means that the user programs using the result of op ignore
the difference between op x = 1 or 2.
And this possibility is a good feature: it is a non-determinism
controlled by the user via overlapping instances.
Again, this is a plus, not minus.
The main meaning of the program is its *user meaning*.
And the user is free to make it to coincide with the compiler
meaning.
And definitely, the compiler should *not* try to test (unless,
maybe, it is asked specially) whether op x is the same for
different instances
Example.
One can set one instance that returns the expression for polynomial
op .. as "x^2 + 1",
and another instance to yield "x^2 + 0*x + 1".
If the user considers (1) and (2) as equivalent and supports this
in one's program, this difference may cause no harm, sometimes may
help.
And note that in this case, we have to say that "x^2 + 1" and
"x^2 + 0*x + 1" have the same (user) meaning.
But if they should not be equivalent, then the user should not
define such strange overlapping instances.
>> But the existing implementations often force me to write the things
>> like (Field a, Ring (ResidueE (Pol a)) =>
>> instead of plain (Field a) =>
> Because overlapping instances are not quite compatible with Haskell
> lasses! With the concept, not a particular implementation.
Probably, not.
I expect, it is a small misfeature in the compilation technique.
Once you provided two useful examples - in favor of your denying of
overlaps.
But these examples were solved positively.
Then, you continue denying every bit.
The existing implementations handle systematically the overlaps, and
GHC formulates clearly the restrictions on the language using
overlaps, the generic scheme for compiling the overlaps was
illustrated in this mail list with the given example.
With all this, the mere generic denying assertions sound strange -
unless they are accompanied by concrete examples.
------------------
Sergey Mechveliani
[EMAIL PROTECTED]
