<div dir="ltr"><div>I'm not sure I can explain the error message to you adequately, but I can tell you what's happening here.<br><br></div>Basically, your replacement f takes implicit arguments, instead of explicit ones as in the original. (That is what the {} mean - implicit arguments).<br>To fix this, you can do either of:<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote"><span style="font-family:monospace,monospace">uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →<br> (∀ x y → C (x , y)) →<br> ((p : Σ A B) → C p)<br>uncurry f (x , y) = f x y</span><br></blockquote><div><br></div><div>Or<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote"><span style="font-family:monospace,monospace">uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →<br> (∀ {x y} → C (x , y)) →<br> ((p : Σ A B) → C p)<br>uncurry f _ = f </span><br></blockquote><div><br></div><div> (notice how Agda inferred the arguments to f here).<br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Feb 16, 2015 at 2:43 AM, N. Raghavendra <span dir="ltr"><<a href="mailto:raghu@hri.res.in" target="_blank">raghu@hri.res.in</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
I am looking at this definition of uncurry in Data.Product:<br>
<br>
--8<---------------cut here---------------start------------->8---<br>
uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →<br>
((x : A) → (y : B x) → C (x , y)) →<br>
((p : Σ A B) → C p)<br>
uncurry f (x , y) = f x y<br>
--8<---------------cut here---------------end--------------->8---<br>
<br>
As I understand, it says that if we have a set A, a function B from A to<br>
Set, and a function C from the disjoint union M:=(\coprod_{a:A} B(a)) to<br>
Set, then uncurry is the map from \prod_{a:A}(\prod_{b:B(a)} C(a,b)) to<br>
\prod_{p:M}(C(p)) which is defined by<br>
<br>
uncurry f p = f (proj1 p) (proj2 p)<br>
<br>
Now I thought that the product of a family of sets (S_i)_{i\in I}<br>
corresponds to the type (\forall {i} -> S i). So in the definition of<br>
uncurry, I replaced<br>
<br>
((x : A) → (y : B x) → C (x , y)) with<br>
<br>
(\forall {x} -> \forall {y} -> C (x , y))<br>
<br>
But then I got an error like ".C (_x_47 f x y , _y_48 f x y) should be a<br>
function type, but it isn't". What's the explanation?<br>
<br>
Thanks,<br>
Raghu.<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
N. Raghavendra <<a href="mailto:raghu@hri.res.in">raghu@hri.res.in</a>>, <a href="http://www.retrotexts.net/" target="_blank">http://www.retrotexts.net/</a><br>
Harish-Chandra Research Institute, <a href="http://www.hri.res.in/" target="_blank">http://www.hri.res.in/</a><br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</font></span></blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature"><div dir="ltr"><div><div>Christopher Jenkins<br></div>Embedded Systems Software Engineer<br></div>Genesi USA Inc.<br></div></div>
</div>