DoCon and GHC
Serge D. Mechveliani
mechvel at botik.ru
Thu Jan 3 13:29:05 CET 2013
On Wed, Jan 02, 2013 at 11:27:15PM +0000, Simon Peyton-Jones wrote:
> I made a second mistake. I meant (LinSolvRing (UPol k)). Apologies.
>
> | > I don't know why 7.4 accepts it, but I'm not inclined to investigate...
> | > looks like a bug in 7.4.
> |
> | ghc-7.4.1 may use a special trick, but is correct.
>
> I don't understand your explanation. What is wrong with this reasoning?
>
> 1. The call to upEucRing in cubicExt gives rise the constraint
> (LinSolvRing (UPol k))
> Corect?
>
> 2. There are two overlapping instances for (LinSolvRing (UPol k)),
> defined in UPol2_ and UPol3_
> Correct?
>
> 3. So GHC cannot solve the constraint using an instance declaration.
> Correct?
>
> 4. The type signature provides
> (Field k, FactorizationRing (UPol k))
> but neither is enough to satisfy LinSolvRing (UPol k).
> Correct?
>
> 5. Therefore we must add LinSolvRing (UPol k) to the signature.
>
> If you believe that the function should typecheck as-is, please explain
> how to deduce (LinSolvRing (UPol k)) from
> (Field k, FactorizationRing (UPol k)).
1. I try adding `, LinSolvRing (UPol k)' to the sig of cubeExt.
Now, ghc-7.6.1.20121207
builds docon-2.12 but does not compile the demonstration of T_cubeext.hs
(where cubicExt is)
-- with {-# LANGUAGE ScopedTypeVariables, MonoLocalBinds #-}
prepended to the module.
Can you, please, reproduce this in ghc-7.6.1.20121207 ?
Because
a) the problem is in porting to a fresh stable GHC version,
b) ghc-7.6.1.20121207 is announced to become a fresh ghc-7.6.2,
and it asks for testing,
c) if I use an older version, then, why, I could simply remain with
ghc-7.4.1.
2. Now suppose that a fresh GHC is fixed, and the point (1) works.
Adding `, LinSolvRing (UPol k)' is not an error.
But is an awkward algebraic statement.
For example, one can formulate
"for all integer p > 2 such that p is prime and p is odd,
it holds Foo(p)".
Adding "and p is odd" is not an error, but looks awkward, because it is
derived from (p > 2, p is prime) according to previous theory.
This reduces redability of the text, because the reader starts to think
that he is missing something subtle.
Similarly, LinSolvRing (UPol k) is derived in cubicExt from
cubicExt and from the proper DoCon.
The matter is that the algorithm (instance) for this LinSolvRing (UPol k)
is derived in multiple ways -- overlapping instances.
3. For this particular case, I agree to tell to GHC:
"choose any derivation way you like".
Because a) I know that the needed final result part does not depend on
this choice (even though the algoritms differ),
b) the cost difference will not be great.
How can I tell this to GHC -- with respect to only this function signature,
or maybe, only to this module ?
4. Probably, the rule of the substitutional instance specialization in
Haskell+Glasgow is not enough to follow algebra.
Why not give the user an additional way to choose the derivation?
For example, let there be the instances I, II, III, IV, and the instance
(Foo T) is derived from I, II, III, IV in multiple ways.
The programmer writes the signature
f :: (..., (Foo T, using {II, III}, notUsing {I, IV})) => ...
which means to consider for (Foo T) only those derivations which use
{II, III} and do not use {I, IV}.
I do not know, may be I am missing something.
5. Now, I specify how LinSolvRing (UPol k) is derived in the existing
Haskell+Glasgow language.
DoCon = Proper-DoCon + demo; cubicExt is a part of demo.
First, Proper-DoCon is installed -- this works.
And cubicExt is not compiled.
Proper-DoCon includes:
GCDRing a and EuclideanRing a are superclasses for Field a, (I)
class (GCDRing a, LinSolvRing a) => EuclideanRing a where ... (II)
instance GCDRing a => GCDRing (UPol a) where ... (III)
instance Field k => EuclideanRing (UPol k) where ... (IV)
instance EuclideanRing a => LinSolvRing (UPol a) where ... (V)
(in Pol2_.hs)
Each of these has a very useful algebraic meaning.
Now, GHC starts to compile cubicExt. And there
Field k => LinSolvRing (UPol k)
is derived from I -- V in at least two ways, and may be there are
even more of them.
Algebraically, these overlaps are all right, they are in the nature,
these derivations give equivalent results.
But one may insist: "choose the way, because the algorithms are different,
and the computation cost may differ".
For example, for
Field k => LinSolvRing (UPol k),
I would choose this way:
"Field k is declared.
Euclidean is a superclass for Field by (I).
hence there is the instance Euclidean k.
hence there is the instance LinSolvRing (UPol k)
by V with a := k.
"
And Haskell+Glasgow sees this derivation surely.
In the algebra textbooks it is expressed like this:
"k is a Field, hence it is EuclideanRing, hence, by V, (UPol k)
is LinSolvRing."
Other ways I consider as algorithmically parasitic.
They appear by GHC composing I -- V in various combinations.
I am forced to write I -- V, because each of them is useful by itself
in various situations; this is in the nature of algebra.
On the other hand, I have not enough language constructs to cut out
(for GHC) the combinations that are parasitic -- with respect to the
computational cost choice.
Here is another derivation for Field k => LinSolvRing (UPol k).
Repeat the state:
GCDRing a and EuclideanRing a are superclasses for Field a, (I)
class (GCDRing a, LinSolvRing a) => EuclideanRing a where ... (II)
instance GCDRing a => GCDRing (UPol a) (III)
instance Field k => EuclideanRing (UPol k) (IV)
instance EuclideanRing a => LinSolvRing (UPol a) (V)
(in Pol2_.hs)
The derivation is:
Field k is given.
EuclideanRing (UPol k) is by IV.
LinSolvRing a is a superclass for EuclideanRing a by II.
Hence, with a := UPol k, there must presense the instance
LinSolvRing (UPol k), such an instance must precede IV in order
IV to be compiled.
And GHC finds the instance for LinSolvRing (UPol k).
For example, it is by V with a := k.
And it occurs that the first derivation is a part of the second one.
I do not know how many derivations exist, and whether GHC ignores the
second one.
But at least I have answered to the question
> If you believe that the function should typecheck as-is, please explain
> how to deduce (LinSolvRing (UPol k)) from
> (Field k, FactorizationRing (UPol k)).
I have presented the two derivations, the first one looks natural.
> I don't understand your explanation. What is wrong with this reasoning?
> 1. The call to upEucRing in cubicExt gives rise the constraint
> (LinSolvRing (UPol k))
> Corect?
Yes.
It gives rise to EuclideanRing (UPol k).
And LinSolvRing a is a superclass for EuclideanRing a.
And the constraint of EuclideanRing (UPol k)
follows from the call to upEucRing in cubicExt and from the declaration
upEucRing :: EuclideanRing a => ADomDom a
in Ring_0.hs.
Because cubicExt applies upEucRing with a = (Field k, ...) => UPol k
The condition of EuclideanRing (UPol k) is satisfied by the following
declarations in DoCon (not in the demonstration program):
GCDRing a and EuclideanRing a are superclasses for Field a, (I)
class (GCDRing a, LinSolvRing a) => EuclideanRing a (II)
instance GCDRing a => GCDRing (UPol a) (III)
instance Field k => EuclideanRing (UPol k) (IV)
instance EuclideanRing a => LinSolvRing (UPol a) (V)
(in Pol2_.hs)
So, Field k => EuclideanRing (UPol k)
follows by IV
and also by V & III & I (I find this way only now).
> 2. There are two overlapping instances for (LinSolvRing (UPol k)),
> defined in UPol2_ and UPol3_
> Correct?
a) DoCon has not UPol2_.hs nor UPol3_.hs.
It has Pol2_.hs and Pol3_.hs.
(And for any occasion: as I wrote earlier, the data costructors Pol
and UPol have different meaning and different instance sets
).
b) I have shown the two derivations for Field k => LinSolvRing (UPol k)
(the second one in strange, because it is included in the first).
May be, there exists some more clear overlap.
instance EuclideanRing a => LinSolvRing (UPol a) of Pol_2.hs
is used in the first derivation.
c) Pol3_ has
instance (LinSolvRing (Pol a), CommutativeRing a) =>
LinSolvRing (UPol (Pol a))
But this does not overlap with I -- V,
in particular, not with Field k => LinSolvRing (UPol k).
Because Pol a is never of a Field nor of EuclideanRing.
And Hashell+Glasgow sees this.
> 3. So GHC cannot solve the constraint using an instance declaration.
> Correct?
GHC finds multiple solutions for this constraint.
Several instances overlap. Each of these derivations is algebraically
correct.
I do not know of whether this overlap is resolved by the rules of the
Haskell+Glasgow language.
Also ghc-7.4.1 says it resolves them (at least, the demo program works
correct),
and ghc-7.6.1.20121207 does not resolve.
> 4. The type signature provides
> (Field k, FactorizationRing (UPol k))
> but neither is enough to satisfy LinSolvRing (UPol k).
> Correct?
No. LinSolvRing (UPol k) is derived by Haskell+Glasgow from
Field k.
See above my explanation.
But it is derived in multiple ways.
> 5. Therefore we must add LinSolvRing (UPol k) to the signature.
This is not an error.
But ghc-7.6.1.20121207 does not compile this.
Also see the beginning of my part of this letter.
> If you believe that the function should typecheck as-is, please explain
> how to deduce (LinSolvRing (UPol k)) from
> (Field k, FactorizationRing (UPol k)).
I have shown this above. The GHC problem is that most probably, it is
deduced in multiple ways.
At least, it is now desirable the following:
to make ghc-7.6.1.20121207 to compile your variant with adding
LinSolvRing (UPol k) to the signature.
Do you agree with this single point?
Regards,
------
Sergei
More information about the Glasgow-haskell-users
mailing list