[Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...

Dmytro Starosud d.starosud at gmail.com
Sun Dec 7 13:39:52 CET 2014


Thank you very much, Andreas, for the explanation.
Now it's clear to me from where the problem arises.

Best regards,
Dmytro


2014-12-06 14:21 GMT+02:00 Andreas Abel <abela at chalmers.se>:

> Unfortunately, the order of arguments in the constructor matters for the
> coverage checker in such delicate cases.  I filed an issue derived from
> your problem:
>
>   https://code.google.com/p/agda/issues/detail?id=1384
>
> If you take look there, putting the equality proof in the constructor
> earlier works.
>
> Ideally, every program that is generated by subsequent splits (C-c C-c)
> should be accepted by Agda.  Unfortunately, in the resulting code the split
> order is no longer visible, and Agda tries to guess an order that works.
> It does not always.
>
> Sorry, at the moment you are forced to try and error.  Agda logging can be
> enabled with the -v option, but I am afraid the logs only make sense if you
> read the source code side by side.  There is no user-friendly log where
> Agda gives an executive summary of what it did.  (Contributions welcome!)
>
> Note that sets of clauses that do not cover all cases are making the
> problem for the coverage checker even harder!  This is why you get the
> failure when you comment-out the catch-all.
>
> The following snippet of the CHANGELOG gives a hint on the strategy of the
> coverage checker:
>
>
> * Improved coverage checker.  The coverage checker splits on
>   arguments that have constructor or literal pattern, committing
>   to the left-most split that makes progress.
>   Consider the lookup function for vectors:
>
>     data Fin : Nat → Set where
>       zero : {n : Nat} → Fin (suc n)
>       suc  : {n : Nat} → Fin n → Fin (suc n)
>
>     data Vec (A : Set) : Nat → Set where
>       []  : Vec A zero
>       _∷_ : {n : Nat} → A → Vec A n → Vec A (suc n)
>
>     _!!_ : {A : Set}{n : Nat} → Vec A n → Fin n → A
>     (x ∷ xs) !! zero  = x
>     (x ∷ xs) !! suc i = xs !! i
>
>   In Agda up to 2.3.0, this definition is rejected unless we add
>   an absurd clause
>
>     [] !! ()
>
>   This is because the coverage checker committed on splitting
>   on the vector argument, even though this inevitably lead to
>   failed coverage, because a case for the empty vector [] is missing.
>
>   The improvement to the coverage checker consists on committing
>   only on splits that have a chance of covering, since all possible
>   constructor patterns are present.  Thus, Agda will now split
>   first on the Fin argument, since cases for both zero and suc are
>   present.  Then, it can split on the Vec argument, since the
>   empty vector is already ruled out by instantiating n to a suc _.
>
>
> On 06.12.2014 12:03, Dmytro Starosud wrote:
>
>> Sorry :)
>> One more issue. Please see another gist
>> https://gist.github.com/dima-starosud/f27ffd54895822a7db03
>> Here I (hopefully) did as you proposed.
>> But I still able to make Agda showing that annoying unification problem
>> error message.
>>
>> Looks like the problem is related to totality checker?
>> I think the real cause is simply shadowed?
>>
>> Please help me understating this.
>> Is there any way to enable Agda logging or something else to see what
>> happens behind the scene?
>>
>> Thanks a lot,
>> Dmytro
>>
>>
>> 2014-12-06 12:37 GMT+02:00 Dmytro Starosud <d.starosud at gmail.com
>> <mailto:d.starosud at gmail.com>>:
>>
>>     ...and one more question.
>>
>>     How the way you are proposing differs from "reduce₃"?
>>
>>     Does not "reduce₃" turn non-pattern indexes to good one?
>>     Since as you can see "reduce₂" doesn't produce error messages.
>>
>>     Thanks,
>>     Dmytro
>>
>>
>>     2014-12-06 12:28 GMT+02:00 Dmytro Starosud <d.starosud at gmail.com
>>     <mailto:d.starosud at gmail.com>>:
>>
>>         Thanks, Andreas,
>>
>>         I had a kind of similar thoughts, but needed confirmation.
>>         So, the rule is "do not use functional dependencies as a family
>>         indexes, but just constructors".
>>         Please correct if this is not accurate statement.
>>
>>         What is the root cause (I mean what difficulties in
>>         compiler/theory) which sometimes doesn't allow solving such
>>         unification problems?
>>
>>         Thanks a lot,
>>         Dmytro
>>
>>
>>         2014-12-06 10:57 GMT+02:00 Andreas Abel <abela at chalmers.se
>>         <mailto:abela at chalmers.se>>:
>>
>>             The problem is that you are indexing your family Term by
>>             non-patterns in some of the constructor cases.  Then Agda
>>             can sometimes not solve the unification constraints involved
>>             in dependent pattern matching, and gives up or produces
>>             error messages.  The solution is to use explicit proofs of
>>             equality in your constructors instead.
>>
>>             Here is a cut-down version of your plight:
>>
>>             module _ where
>>
>>             open import Data.Bool
>>             open import Relation.Binary.__PropositionalEquality
>>
>>
>>             module NonPatternFamily where
>>
>>                data Term : Bool → Set where
>>                  I : Term false
>>                  App : (a b : Bool) → Term a → Term b → Term (a ∨ b)
>>                    -- Non-pattern in target of App
>>                    -- _∨_ is a defined function, not a constructor.
>>
>>                fails : Term false → Set
>>                fails (App false false I x) = Bool
>>                fails _ = Bool
>>
>>                -- a ∨ b != false of type Bool
>>                -- when checking that the pattern App false false I x has
>>             type
>>                -- Term false
>>
>>             -- Radical fix: no index to Term, just parameter:
>>
>>             module JustData where
>>
>>                -- Version with no indices at all, only parameters.
>>
>>                data Term (i : Bool) : Set where
>>                  I   : i ≡ false → Term i
>>                  App : (a b : Bool) → i ≡ a ∨ b → Term a → Term b → Term i
>>
>>                test : Term false → Set
>>                test (App false false refl (I refl) x) = Bool
>>                test _ = Bool
>>
>>             -- Moderate fix: retain the index in harmless (pattern case).
>>
>>             module PatternFamily where
>>
>>                -- Version with index,
>>                -- but using equality when non-pattern index would be
>> needed.
>>
>>                data Term : (i : Bool) → Set where
>>                  I   : Term false
>>                  App : (i a b : Bool) → i ≡ a ∨ b → Term a → Term b →
>> Term i
>>
>>                test : Term false → Set
>>                test (App .false false false refl I x) = Bool
>>                test _ = Bool
>>
>>             Hope that helps,
>>             Andreas
>>
>>
>>
>>             On 05.12.2014 22:47, Dmytro Starosud wrote:
>>
>>                 Hello guys,
>>
>>                 I am trying to write a function on indexed types:
>>                 https://gist.github.com/dima-_
>> _starosud/7100947b0e243ea6a034
>>                 <https://gist.github.com/dima-
>> starosud/7100947b0e243ea6a034>
>>                 But I cannot understand the reason of the error messages
>>                 shown, and how
>>                 to solve issues arisen.
>>
>>                 Please see a gist (link above).
>>                 Ideally I wanted "reduce₁". But that didn't compile.
>>                 (And I think I can
>>                 imagine the reason why)
>>
>>                 Next attempt was "reduce₂". But this would involve a lot
>>                 of unnecessary
>>                 code on RHSs.
>>
>>                 Than I decided to improve it and got "reduce₃", but it
>>                 gave me
>>                 completely puzzling error message.
>>
>>                 Please help me to understand all that stuff Agda
>>                 communicates to me.
>>
>>                 I would like something really simple (like "reduce₁"),
>>                 probably with
>>                 help of *pattern*s.
>>
>>                 Thanks in advance,
>>                 Dmytro
>>
>>
>>
>>                 _________________________________________________
>>                 Agda mailing list
>>                 Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>                 https://lists.chalmers.se/__mailman/listinfo/agda
>>                 <https://lists.chalmers.se/mailman/listinfo/agda>
>>
>>
>>
>>             --
>>             Andreas Abel  <><      Du bist der geliebte Mensch.
>>
>>             Department of Computer Science and Engineering
>>             Chalmers and Gothenburg University, Sweden
>>
>>             andreas.abel at gu.se <mailto:andreas.abel at gu.se>
>>             http://www2.tcs.ifi.lmu.de/~__abel/
>>             <http://www2.tcs.ifi.lmu.de/~abel/>
>>
>>
>>
>>
>>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141207/e8dace5b/attachment.html


More information about the Agda mailing list