winterkoninkje: shadowcrane (clean) (Default)

I've mentioned these a few times in different places, most recently on Reddit. So I figured I should repost them here for better googleability for folks just starting to learn about dependent types and type theory.

PSA #1: Beware: "type theory" and "Type Theory" are not the same thing, note the caps. The former describes the entire field of enquiry which explores possible theories about types; the latter is the name of one particular theory/system, namely the one Per Martin-Löf popularized (and others have extended and reinvented since then).

Yes, this is an extremely obnoxious detail, but it's one that often confuses newcomers; e.g., learning MLTT and thinking that applies to all type systems, or learning other type systems and then being confused when people make flagrantly false statements (when interpreted as statements about type theory as a whole, though they're true of MLTT). This is why I prefer to refer to Type Theory as "TT" or "MLTT", to avoid confusion, and because I am interested in the entire field of enquiry and in comparing different systems rather than focusing on just one.

ObTangent: There are similar reasons for why ML is called "ML" instead of "metalanguage".

PSA #2: There are conflicting meanings for the terms "sum" and "product" in dependent type land. Those coming from category theory and functional programming tend to say "sum" to mean tagged unions, "product" to mean pairs (e.g, cartesian products or similar), and "exponentials" to mean functions as objects— all of these exactly as in non-dependent languages. However, those coming more from the set-theory side of things use "product" to mean functions (whence the capital Pi), "sum" to mean pairs (whence the capital Sigma), and have no common term for unions.

Anonymous( )Anonymous This account has disabled anonymous posting.
OpenID( )OpenID You can comment on this post while signed in with an account from many other sites, once you have confirmed your email address. Sign in using OpenID.
Account name:
If you don't have an account you can create one now.
HTML doesn't work in the subject.


If you are unable to use this captcha for any reason, please contact us by email at

Notice: This account is set to log the IP addresses of everyone who comments.
Links will be displayed as unclickable URLs to help prevent spam.

June 2017

18192021 222324


Page generated 21 Sep 2017 02:15 pm
Powered by Dreamwidth Studios