[Agda] Forall and product

[Chris Jenkins]

p.s.

I think I can explain the error message now, actually. Your example is
basically equivalent to the following definition

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} x y
>

With an error message easier to understand:

.C (x , y) should be a function type, but it isn't
> when checking that x y are valid arguments to a function of type
> .C (x , y)
>

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.

On Mon, Feb 16, 2015 at 1:35 PM, Chris Jenkins <chris.jenkins at genesi-usa.com
> wrote:

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



-- 
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/b0da2ece/attachment.html