Conversation

There's a lot of discourse about this today. In the name of justice and to equally appease absolutely no one, I will now be calling (Πx: A. B) a dependent exponent type

Quote Tweet

Amélia Liao

ICFP

@plt_amy

· Jan 25

we need like a decree from God to abolish the names "dependent sum" and "dependent product", for the love of all that is good: call the first dependent pairs and the second dependent functions, like the hott book does (i'm guilty of using the shitty terms)

Show this thread

David Jaz Myers

@myers_jaz

Jan 25

I like this better than dependent product actually lol. The thing is; the sum / pair type is the dependent version of the product type… this is the dependent version of B^A. Great!

Brendan Zabarauskas

@brendanzab

Jan 25

Isn't the idea that dependent (sum | pair) type is an iterated sum? And the dependent (function | product) type is an iterated product? To be clear, I try to use the former names as people familiar with ‘sum types’ will invariably get things around the wrong way. :(

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

Replying to

I guess I object to it being the way stuff is is introduced - it's still a cool connection, but it's an extra layer of stuff to teach, least in the context of explaining things to programmers. I feel similarly to the use of ‘sum types’ and ‘product types’ in non-dependent FP tbh.

5:44 AM · Jan 26, 2022Twitter Web App

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

Yeah, agreed.

Replying to

Maybe it's more of a cultural thing? I do think `(a : A) * B a` seems ripe for being misnamed/confused. Like, “wasn't `A * B` a product type? now you say it's a sum?!”