[Agda] Forall and product

[Chris Jenkins]

I'm not sure I can explain the error message to you adequately, but I can
tell you what's happening here.

Basically, your replacement f takes implicit arguments, instead of explicit
ones as in the original. (That is what the {} mean - implicit arguments).
To fix this, you can do either of:

uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
>           (∀ x y → C (x , y)) →
>           ((p : Σ A B) → C p)
> uncurry f (x , y) = f x y
>

Or

uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
>           (∀ {x y} → C (x , y)) →
>           ((p : Σ A B) → C p)
> uncurry f _ = f
>

 (notice how Agda inferred the arguments to f here).

On Mon, Feb 16, 2015 at 2:43 AM, N. Raghavendra <raghu at hri.res.in> wrote:

> Hi,
>
> I am looking at this definition of uncurry in Data.Product:
>
> --8<---------------cut here---------------start------------->8---
> uncurry : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
>           ((x : A) → (y : B x) → C (x , y)) →
>           ((p : Σ A B) → C p)
> uncurry f (x , y) = f x y
> --8<---------------cut here---------------end--------------->8---
>
> As I understand, it says that if we have a set A, a function B from A to
> Set, and a function C from the disjoint union M:=(\coprod_{a:A} B(a)) to
> Set, then uncurry is the map from \prod_{a:A}(\prod_{b:B(a)} C(a,b)) to
> \prod_{p:M}(C(p)) which is defined by
>
> uncurry f p = f (proj1 p) (proj2 p)
>
> Now I thought that the product of a family of sets (S_i)_{i\in I}
> corresponds to the type (\forall {i} -> S i).  So in the definition of
> uncurry, I replaced
>
> ((x : A) → (y : B x) → C (x , y)) with
>
> (\forall {x} -> \forall {y} -> C (x , y))
>
> But then I got an error like ".C (_x_47 f x y , _y_48 f x y) should be a
> function type, but it isn't".  What's the explanation?
>
> Thanks,
> Raghu.
>
> --
> N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
> Harish-Chandra Research Institute, http://www.hri.res.in/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
Christopher Jenkins
Embedded Systems Software Engineer
Genesi USA Inc.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150216/5a97cc3e/attachment.html