<div dir="ltr"><div class="gmail_extra">On Wed, Feb 25, 2015 at 3:26 AM, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I guess programmers are more interested in whether something is a pair or a function than in Descartes or families of sets.<br></blockquote><div><br><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">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.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">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.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">-- Dan<br></div></div></div><br></div></div>