<div dir="ltr"><div><div><div><div>...and one more question.<br></div><br>How the way you are proposing differs from "reduce₃"?<br></div><br>Does not "reduce₃" turn non-pattern indexes to good one?<br></div>Since as you can see "<span class="">reduce₂</span>" doesn't produce error messages.<br><br></div>Thanks,<br>Dmytro <br><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">2014-12-06 12:28 GMT+02:00 Dmytro Starosud <span dir="ltr"><<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>Thanks, Andreas,<br><br></div>I had a kind of similar thoughts, but needed confirmation.<br></div><div>So, the rule is "do not use functional dependencies as a family indexes, but just constructors".<br></div><div>Please correct if this is not accurate statement.<br><br></div>What is the root cause (I mean what difficulties in compiler/theory) which sometimes doesn't allow solving such unification problems?<br><div><br></div><div>Thanks a lot,<br>Dmytro <br><br></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">2014-12-06 10:57 GMT+02:00 Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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.<br>
<br>
Here is a cut-down version of your plight:<br>
<br>
module _ where<br>
<br>
open import Data.Bool<br>
open import Relation.Binary.<u></u>PropositionalEquality<br>
<br>
module NonPatternFamily where<br>
<br>
data Term : Bool → Set where<br>
I : Term false<br>
App : (a b : Bool) → Term a → Term b → Term (a ∨ b)<br>
-- Non-pattern in target of App<br>
-- _∨_ is a defined function, not a constructor.<br>
<br>
fails : Term false → Set<br>
fails (App false false I x) = Bool<br>
fails _ = Bool<br>
<br>
-- a ∨ b != false of type Bool<br>
-- when checking that the pattern App false false I x has type<br>
-- Term false<br>
<br>
-- Radical fix: no index to Term, just parameter:<br>
<br>
module JustData where<br>
<br>
-- Version with no indices at all, only parameters.<br>
<br>
data Term (i : Bool) : Set where<br>
I : i ≡ false → Term i<br>
App : (a b : Bool) → i ≡ a ∨ b → Term a → Term b → Term i<br>
<br>
test : Term false → Set<br>
test (App false false refl (I refl) x) = Bool<br>
test _ = Bool<br>
<br>
-- Moderate fix: retain the index in harmless (pattern case).<br>
<br>
module PatternFamily where<br>
<br>
-- Version with index,<br>
-- but using equality when non-pattern index would be needed.<br>
<br>
data Term : (i : Bool) → Set where<br>
I : Term false<br>
App : (i a b : Bool) → i ≡ a ∨ b → Term a → Term b → Term i<br>
<br>
test : Term false → Set<br>
test (App .false false false refl I x) = Bool<br>
test _ = Bool<br>
<br>
Hope that helps,<br>
Andreas<div><div><br>
<br>
<br>
On 05.12.2014 22:47, Dmytro Starosud wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div>
Hello guys,<br>
<br>
I am trying to write a function on indexed types:<br>
<a href="https://gist.github.com/dima-starosud/7100947b0e243ea6a034" target="_blank">https://gist.github.com/dima-<u></u>starosud/7100947b0e243ea6a034</a><br>
But I cannot understand the reason of the error messages shown, and how<br>
to solve issues arisen.<br>
<br>
Please see a gist (link above).<br>
Ideally I wanted "reduce₁". But that didn't compile. (And I think I can<br>
imagine the reason why)<br>
<br>
Next attempt was "reduce₂". But this would involve a lot of unnecessary<br>
code on RHSs.<br>
<br>
Than I decided to improve it and got "reduce₃", but it gave me<br>
completely puzzling error message.<br>
<br>
Please help me to understand all that stuff Agda communicates to me.<br>
<br>
I would like something really simple (like "reduce₁"), probably with<br></div></div>
help of *pattern*s.<br>
<br>
Thanks in advance,<br>
Dmytro<br>
<br>
<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br><span><font color="#888888">
</font></span></blockquote><span><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</font></span></blockquote></div><br></div>
</div></div></blockquote></div><br></div>