Lúcás Meier@cronokirby·Nov 23, 2021It's more like "refinement" types. Basically you can specify that a type has specific values over just the full range. e.g. type SmallInt = 1 | 2 | 312
eleanor @zornsllama·Nov 23, 2021There are also conditional types which are a nontrivial special case of pi types11
Brendan Zabarauskas@brendanzab·Nov 23, 2021Had to think for a sec, but yeah, you are right: Π(cond : Bool). if cond then A else B very unsound though lol12
Brendan Zabarauskas@brendanzabReplying to @zornsllama and @cronokirbyheh, yup. hopefully folks don't end up hating on dependent types because they are ‘broken’ though 😳9:15 AM · Nov 23, 2021·Twitter Web App1 Like