[Agda] Re: Forall and product

[Dan Doel]

On Wed, Feb 25, 2015 at 3:26 AM, Andreas Abel <abela at chalmers.se> wrote:

> I guess programmers are more interested in whether something is a pair or
> a function than in Descartes or families of sets.
>

​If they are, then shouldn't they recognize that the sum type A + B is
inhabited by pairs? The values are pairs of a tag and ​a value of the
corresponding type. And sigma types internalize what you get to put in the
tag portion of the pair.

Anyhow, I'm pretty sure I'm a programmer, but I've always used and liked
the sum-product terminology. I actually thought it was the more common
amongst people doing work on dependent type theory (although if you want to
eliminate any chance of misinterpretation, "sigma type" and "pi type" seem
safest, and serviceable). Maybe I'm a weird programmer, though.

-- Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150225/17a7b021/attachment.html