<div dir="ltr"><div>p.s.<br><br></div>I think I can explain the error message now, actually. Your example is basically equivalent to the following definition<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} x y</span><br></blockquote><div><br></div><div>With an error message easier to understand:<br><br></div><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote"><div><span style="font-family:monospace,monospace">.C (x , y) should be a function type, but it isn't<br>when checking that x y are valid arguments to a function of type<br>.C (x , y)</span><br></div></blockquote><div> </div><div>So Agda sees the f and it's implicit arguments (in your example, hidden) {x} {y}, produces the C (x , y) (underscores in your example because they were inferred), then thinks you meant to apply this result to x and y. Of course, C (x , y) isn't a function type! So Agda complains.<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Feb 16, 2015 at 1:35 PM, Chris Jenkins <span dir="ltr"><<a href="mailto:chris.jenkins@genesi-usa.com" target="_blank">chris.jenkins@genesi-usa.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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"><span class="">uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →<br></span> (∀ x y → C (x , y)) →<span class=""><br> ((p : Σ A B) → C p)<br>uncurry f (x , y) = f x y</span></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"><span class="">uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →<br></span> (∀ {x y} → C (x , y)) →<span class=""><br> ((p : Σ A B) → C p)<br></span>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"><div><div class="h5"><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><font color="#888888"><br>
--<br>
N. Raghavendra <<a href="mailto:raghu@hri.res.in" target="_blank">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" target="_blank">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></div></div><span class="HOEnZb"><font color="#888888">-- <br><div><div dir="ltr"><div><div>Christopher Jenkins<br></div>Embedded Systems Software Engineer<br></div>Genesi USA Inc.<br></div></div>
</font></span></div>
</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>