All this "what is a type" discourse is very confusing to me. If I asked for a definition of object that includes objects of a category, objects of a multicategory, objects of an infinity category would I expect there to be a useful answer?


We had a similar discussion on the meaning of type soundness in M Felleisen's "history of programming languages" course. I took the radical but IMO only sensible position which was "whatever you say it means" or equivalently in pithy symbols |- => |=

· · Web · 0 · 0 · 6
Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.