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

[Dmytro Starosud]

...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>:

> 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>:
>
>> 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
>>> 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
>>> 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
>> http://www2.tcs.ifi.lmu.de/~abel/
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141206/0da6c4ca/attachment-0001.html