Conversation

🥢 Jon 🧄
@ionathanch
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
·
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
4
14
David Jaz Myers
@myers_jaz
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!
2
2
Brendan Zabarauskas
@brendanzab
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. :(
4
1