[Agda] forced arguments in EqReasoning

mechvel at scico.botik.ru mechvel at scico.botik.ru
Sat Nov 28 13:51:30 CET 2020 

On 2020-11-28 14:45, Sandro Stucki wrote:
> As Guillaume has already hinted at, the problem isn't with equality
> reasoning per se, it is, I believe, to do with unification. I have
> seen this problem whenever an equivalence _≈A_ on some type A is
> defined not as a separate data-type, but via a definition of the form
> 
>   a ≈A b = f a ≈B f b
> 
> where _≈B_ is an equivalence over some type B and f is a
> function/expression from B's to A's. Typical examples are where f is a
> projection or some computation involving B's. The definition of _≈A_
> could also involve some pattern matching -- it doesn't matter, as long
> as it's not a data-type definition. This is what Guillaume meant by
> defining _≈A_ via recursion (I think). Your explanation about =fr
> indicates that this is the case for you.

So, see my last letter, with
                         record Fraction ...


> I think what happens is that during unification/type checking, the
> definition of a ≈A b gets expanded and the original terms a and b
> are "computed away" so the unifier cannot use them any longer to
> instantiate the hidden/implicit arguments of _≈A_ or those of the
> equational reasoning combinators. Someone with more insight into
> Agda's unification machinery, please correct me if I am wrong.
> 
> The workaround is to wrap the direct definition in a data-type or
> record. That requires some extra constructors/projections to convert
> between direct proofs of equality and the wrapped ones, but the
> problem with implicit arguments seems to disappear.
> 

In my example with Fraction and Prefraction (in my last letter)
everything looks wrapped enough, I do not know what kind of wrapping
do you mean.

Wrapping it into something more is a complication of the data structure.
It is simpler to enumerate the needed implicits as

   -- not for reading ---
   I = largeImplcit-1
   ...
   IV = largeImplcit-4
   ----------------------

and then use "{I} ... {IV}" in EqReasoning.
Only a) this still takes a certain garbage volume,
b) the programmer spends effort to trace which  i <- {I ... IV}
    to set to which argument in the combinators.

If Agda developers think that there is a real chance to fix this effect
with forced implicits, and if they ask, I could try to provide a reduced 
example.

Regards,

------
Sergei




> Here's an example from the agda-categories library:
> 
> https://github.com/agda/agda-categories/blob/master/src/Categories/Morphism/IsoEquiv.agda
> 
> I hope that helps.
> 
> Cheers
> /Sandro
> 
> On Sat, Nov 28, 2020, 11:33 <mechvel at scico.botik.ru> wrote:
> 
>> On 2020-11-28 02:19, guillaume allais wrote:
>>> Hi Sergei,
>>> 
>>> Is your notion of equivalence by any change defined by recursion
>> on its
>>> inputs?
>>> That would explain why you're getting really bad inference despite
>> the
>>> equational
>>> reasoning combinators being designed to make inference as strong
>> as
>>> possible.
>>> 
>> 
>> In the last example as below ("begin⟨ fooSetoid ⟩")
>> it is of  polSetoid  - of setoid of polynomials. And its equivalence
>> 
>> _=ₚ_is
>> the _pointwise equality_ of certain ordered lists of pairs. The
>> first
>> component
>> in a pair belongs to the specified CommutativeRing R, the second is
>> of
>> Nat.
>> The first components are compared by _≈_ of R, the second
>> components
>> compared
>> by _≡_.
>> The pointwise equality of lists is taken from lib-1.4, I expect it
>> is
>> implemented
>> by a certain recursion on input that you write about.
>> Is it?
>> 
>> But earlier I dealt with the same difficulty with the equality
>> reasoning
>> which does
>> not apply recursion: generic arithmetic of fractions over a GCDRing
>> R.
>> The equality =fr on fractions is defined by applying once the
>> equality
>> _≈_
>> on R:
>> (Fr num denom denom≉0) =fr (Fr num' denom' denom'≉0) =
>> num * denom' ≈ num' * denom,
>> where _≈_ and _*_ re of R.
>> Still there was the same problem with implicits in EqReasoning for
>> _=fr_.
>> 
>> I wrote
>> 
>>>> eq =  =ₚsym {Y} {Z} eq'
>>>> where
>>>> eq' : largeExpression2 =ₚ largeExpr1 *ₚ x
>>>> eq' = lemma largeExpr1 x,
>>>> 
>>>> where Y and Z are new variables. What terms to substitute for Y
>> and Z
>>>> in order for  eq  to have the needed type?
>>>> If the type checker is able to solve this, then it would not
>> require
>>>> these large implicit arguments.
>> 
>> But the left hand column
>> begin⟨ fooSetoid ⟩
>> fT + 0ₚ
>> fT + ((- largeExpression) + largeExpression)
>> ...
>> 
>> already has these terms. They only need to be substituted for X and
>> Y.
>> Why EqReasoning cannot do this?
>> 
>> --
>> SM
>> 
>>> 
>>> 
>>> On 27/11/2020 21:50, mechvel at scico.botik.ru wrote:
>>>> On 2020-11-27 22:22, mechvel at scico.botik.ru wrote:
>>>>> [..]
>>>>> 
>>>>> For more complex types, Agda forces me to write this:
>>>>> begin⟨ fooSetoid ⟩
>>>>> fT + 0ₚ
>>>>> ≈⟨ +ₚcongˡ {fT} {0ₚ} {(- largeExpression) +
>>>>> largeExpression} $
>>>>> =ₚsym {(- largeExpression) + largeExpression}
>> {0ₚ} $
>>>>> -f+f largeExpression
>>>>> ⟩
>>>>> fT + ((- largeExpression) + largeExpression)
>>>>> ...
>>>>> ∎
>>>>> 
>>>>> It this source code,  largeExpression  is written 7 times
>> instead of
>>>>> 3.
>>>>> And real proofs often contain 5-10 versions of largeExpression
>> that
>>>>> are forced to be copied this way and pollute the source.
>>>> 
>>>> The most nasty is the "sym" combinator.
>>>> For example, its step in Reasoining can represented as
>>>> 
>>>> eq :  largeExpr1 *ₚ x =ₚ largeExpression2
>>>> eq =  =ₚsym {largeExpression2} {largeExpresssion1}
>>>> (lemma largeExpr1 x)
>>>> 
>>>> I am not an expert in this are. But here is a naive
>> consideration.
>>>> Suppose the type checker rewrites the implementation for  eq  as
>>>> 
>>>> eq =  =ₚsym {Y} {Z} eq'
>>>> where
>>>> eq' : largeExpression2 =ₚ largeExpr1 *ₚ x
>>>> eq' = lemma largeExpr1 x,
>>>> 
>>>> where Y and Z are new variables. What terms to substitute for Y
>> and Z
>>>> in order for  eq  to have the needed type?
>>>> If the type checker is able to solve this, then it would not
>> require
>>>> these large implicit arguments.
>>>> ?
>>>> 
>>>> -- SM
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> 
>> 
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=04%7C01%7Cguillaume.allais%40strath.ac.uk%7C0206289743574a9be04408d8931e736b%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637421106314023035%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=CUrWBN2ydEe8xllykjX2gSI3m4xkdSfw9xwQzEAVgUA%3D&reserved=0
>>> 
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

More information about the Agda mailing list