Yeah, I didn't mean to insinuate that function extensionality is provable or testable in those languages, just that one can ensure that one is actually writing

Yeah, I didn't mean to insinuate that function extensionality is provable or testable in those languages, just that one can ensure that one is actually writing total functions today. I'm sure the same could be done in a simple or polymorphic type theory, I'm just not aware of one. Is there a Haskell extension like Idris's totality checking? I was gonna say, just wait until the OP hears about HoTT. Thanks though, I didn't know Cubical Agda exists.