I'm somewhat new to the field, so this might not be properly phrased, but isn't ... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		swatow on Jan 18, 2015 \| parent \| context \| favorite \| on: What Doesn't Seem Like Work? I'm somewhat new to the field, so this might not be properly phrased, but isn't totality an inherent part of full dependent types?

nbouscal on Jan 18, 2015 [–]

I'm not an expert, but I wouldn't think so. To me, full dependent types just means you have pi and sigma types. I don't see anything fundamental about pi and sigma types that would prevent you from having bottom in your language, or from allowing users to define partial functions.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact