[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