Why colon to denote that a value belongs to a type?





.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty{
margin-bottom:0;
}








19












$begingroup$


Pierce (2002) introduces the typing relation on page 92 by writing:




The typing relation for arithmetic expressions, written "t : T", is defined by
a set of inference rules assigning types to terms




and the footnote says The symbol $in$ is often used instead of :. My question is simply why type theorists prefer to use : over $in$? If a type $T$ is a set of values then it makes perfect sense to write $t in T$, no new notation needed.



Is this similar to how some cs writers prefer $3n^2 = O(n^2)$ even thought it is abuse of notation and should be written $3n^2 in O(n^2)$?










share|cite|improve this question









$endgroup$










  • 7




    $begingroup$
    The membership predicate $x in X$ can be either true or false, whereas a typing declaration $x : X$ is generally interepreted as a factual statement that is declared to be true or it's truth can be derived by purely syntactic means. Contrast this to being a prime number, for which no syntactic method of membership suffices.
    $endgroup$
    – Musa Al-hassy
    May 25 at 3:59






  • 4




    $begingroup$
    @MusaAl-hassy: that's a misrepresentation of what is going on. It is not declared to be true, as that would mean that I can "declare" that "false : int", for example. Neither is it the case that the judgement must be necessarily derived by "purely syntactic means", for instance in the case of the internal type theory of a category with families.
    $endgroup$
    – Andrej Bauer
    May 25 at 13:25






  • 3




    $begingroup$
    Related question on cs.se: What exactly is the semantic difference between set and type?
    $endgroup$
    – Discrete lizard
    May 25 at 17:28






  • 2




    $begingroup$
    To add to @MusaAl-hassy's comment, in computatioal type theory of Bob Constable, Stuart Allen, Bob Harper, et al., $in$ is used routinely for typing judgments because it's more akin to a membership predicate (see this talk, slide 25, for an example).
    $endgroup$
    – xrq
    May 25 at 20:36






  • 3




    $begingroup$
    Surely $3n^2in O(n^2)$ is also an abuse of notation and should really be written $lambda n.3n^2in O(lambda n.n^2)$? (Mathematicians might prefer $nmapsto 3n^2in O(nmapsto n^2)$.)
    $endgroup$
    – Oscar Cunningham
    May 26 at 10:14




















19












$begingroup$


Pierce (2002) introduces the typing relation on page 92 by writing:




The typing relation for arithmetic expressions, written "t : T", is defined by
a set of inference rules assigning types to terms




and the footnote says The symbol $in$ is often used instead of :. My question is simply why type theorists prefer to use : over $in$? If a type $T$ is a set of values then it makes perfect sense to write $t in T$, no new notation needed.



Is this similar to how some cs writers prefer $3n^2 = O(n^2)$ even thought it is abuse of notation and should be written $3n^2 in O(n^2)$?










share|cite|improve this question









$endgroup$










  • 7




    $begingroup$
    The membership predicate $x in X$ can be either true or false, whereas a typing declaration $x : X$ is generally interepreted as a factual statement that is declared to be true or it's truth can be derived by purely syntactic means. Contrast this to being a prime number, for which no syntactic method of membership suffices.
    $endgroup$
    – Musa Al-hassy
    May 25 at 3:59






  • 4




    $begingroup$
    @MusaAl-hassy: that's a misrepresentation of what is going on. It is not declared to be true, as that would mean that I can "declare" that "false : int", for example. Neither is it the case that the judgement must be necessarily derived by "purely syntactic means", for instance in the case of the internal type theory of a category with families.
    $endgroup$
    – Andrej Bauer
    May 25 at 13:25






  • 3




    $begingroup$
    Related question on cs.se: What exactly is the semantic difference between set and type?
    $endgroup$
    – Discrete lizard
    May 25 at 17:28






  • 2




    $begingroup$
    To add to @MusaAl-hassy's comment, in computatioal type theory of Bob Constable, Stuart Allen, Bob Harper, et al., $in$ is used routinely for typing judgments because it's more akin to a membership predicate (see this talk, slide 25, for an example).
    $endgroup$
    – xrq
    May 25 at 20:36






  • 3




    $begingroup$
    Surely $3n^2in O(n^2)$ is also an abuse of notation and should really be written $lambda n.3n^2in O(lambda n.n^2)$? (Mathematicians might prefer $nmapsto 3n^2in O(nmapsto n^2)$.)
    $endgroup$
    – Oscar Cunningham
    May 26 at 10:14
















19












19








19


6



$begingroup$


Pierce (2002) introduces the typing relation on page 92 by writing:




The typing relation for arithmetic expressions, written "t : T", is defined by
a set of inference rules assigning types to terms




and the footnote says The symbol $in$ is often used instead of :. My question is simply why type theorists prefer to use : over $in$? If a type $T$ is a set of values then it makes perfect sense to write $t in T$, no new notation needed.



Is this similar to how some cs writers prefer $3n^2 = O(n^2)$ even thought it is abuse of notation and should be written $3n^2 in O(n^2)$?










share|cite|improve this question









$endgroup$




Pierce (2002) introduces the typing relation on page 92 by writing:




The typing relation for arithmetic expressions, written "t : T", is defined by
a set of inference rules assigning types to terms




and the footnote says The symbol $in$ is often used instead of :. My question is simply why type theorists prefer to use : over $in$? If a type $T$ is a set of values then it makes perfect sense to write $t in T$, no new notation needed.



Is this similar to how some cs writers prefer $3n^2 = O(n^2)$ even thought it is abuse of notation and should be written $3n^2 in O(n^2)$?







type-theory notation






share|cite|improve this question













share|cite|improve this question











share|cite|improve this question




share|cite|improve this question










asked May 24 at 23:34









Björn LindqvistBjörn Lindqvist

2341 silver badge7 bronze badges




2341 silver badge7 bronze badges











  • 7




    $begingroup$
    The membership predicate $x in X$ can be either true or false, whereas a typing declaration $x : X$ is generally interepreted as a factual statement that is declared to be true or it's truth can be derived by purely syntactic means. Contrast this to being a prime number, for which no syntactic method of membership suffices.
    $endgroup$
    – Musa Al-hassy
    May 25 at 3:59






  • 4




    $begingroup$
    @MusaAl-hassy: that's a misrepresentation of what is going on. It is not declared to be true, as that would mean that I can "declare" that "false : int", for example. Neither is it the case that the judgement must be necessarily derived by "purely syntactic means", for instance in the case of the internal type theory of a category with families.
    $endgroup$
    – Andrej Bauer
    May 25 at 13:25






  • 3




    $begingroup$
    Related question on cs.se: What exactly is the semantic difference between set and type?
    $endgroup$
    – Discrete lizard
    May 25 at 17:28






  • 2




    $begingroup$
    To add to @MusaAl-hassy's comment, in computatioal type theory of Bob Constable, Stuart Allen, Bob Harper, et al., $in$ is used routinely for typing judgments because it's more akin to a membership predicate (see this talk, slide 25, for an example).
    $endgroup$
    – xrq
    May 25 at 20:36






  • 3




    $begingroup$
    Surely $3n^2in O(n^2)$ is also an abuse of notation and should really be written $lambda n.3n^2in O(lambda n.n^2)$? (Mathematicians might prefer $nmapsto 3n^2in O(nmapsto n^2)$.)
    $endgroup$
    – Oscar Cunningham
    May 26 at 10:14
















  • 7




    $begingroup$
    The membership predicate $x in X$ can be either true or false, whereas a typing declaration $x : X$ is generally interepreted as a factual statement that is declared to be true or it's truth can be derived by purely syntactic means. Contrast this to being a prime number, for which no syntactic method of membership suffices.
    $endgroup$
    – Musa Al-hassy
    May 25 at 3:59






  • 4




    $begingroup$
    @MusaAl-hassy: that's a misrepresentation of what is going on. It is not declared to be true, as that would mean that I can "declare" that "false : int", for example. Neither is it the case that the judgement must be necessarily derived by "purely syntactic means", for instance in the case of the internal type theory of a category with families.
    $endgroup$
    – Andrej Bauer
    May 25 at 13:25






  • 3




    $begingroup$
    Related question on cs.se: What exactly is the semantic difference between set and type?
    $endgroup$
    – Discrete lizard
    May 25 at 17:28






  • 2




    $begingroup$
    To add to @MusaAl-hassy's comment, in computatioal type theory of Bob Constable, Stuart Allen, Bob Harper, et al., $in$ is used routinely for typing judgments because it's more akin to a membership predicate (see this talk, slide 25, for an example).
    $endgroup$
    – xrq
    May 25 at 20:36






  • 3




    $begingroup$
    Surely $3n^2in O(n^2)$ is also an abuse of notation and should really be written $lambda n.3n^2in O(lambda n.n^2)$? (Mathematicians might prefer $nmapsto 3n^2in O(nmapsto n^2)$.)
    $endgroup$
    – Oscar Cunningham
    May 26 at 10:14










7




7




$begingroup$
The membership predicate $x in X$ can be either true or false, whereas a typing declaration $x : X$ is generally interepreted as a factual statement that is declared to be true or it's truth can be derived by purely syntactic means. Contrast this to being a prime number, for which no syntactic method of membership suffices.
$endgroup$
– Musa Al-hassy
May 25 at 3:59




$begingroup$
The membership predicate $x in X$ can be either true or false, whereas a typing declaration $x : X$ is generally interepreted as a factual statement that is declared to be true or it's truth can be derived by purely syntactic means. Contrast this to being a prime number, for which no syntactic method of membership suffices.
$endgroup$
– Musa Al-hassy
May 25 at 3:59




4




4




$begingroup$
@MusaAl-hassy: that's a misrepresentation of what is going on. It is not declared to be true, as that would mean that I can "declare" that "false : int", for example. Neither is it the case that the judgement must be necessarily derived by "purely syntactic means", for instance in the case of the internal type theory of a category with families.
$endgroup$
– Andrej Bauer
May 25 at 13:25




$begingroup$
@MusaAl-hassy: that's a misrepresentation of what is going on. It is not declared to be true, as that would mean that I can "declare" that "false : int", for example. Neither is it the case that the judgement must be necessarily derived by "purely syntactic means", for instance in the case of the internal type theory of a category with families.
$endgroup$
– Andrej Bauer
May 25 at 13:25




3




3




$begingroup$
Related question on cs.se: What exactly is the semantic difference between set and type?
$endgroup$
– Discrete lizard
May 25 at 17:28




$begingroup$
Related question on cs.se: What exactly is the semantic difference between set and type?
$endgroup$
– Discrete lizard
May 25 at 17:28




2




2




$begingroup$
To add to @MusaAl-hassy's comment, in computatioal type theory of Bob Constable, Stuart Allen, Bob Harper, et al., $in$ is used routinely for typing judgments because it's more akin to a membership predicate (see this talk, slide 25, for an example).
$endgroup$
– xrq
May 25 at 20:36




$begingroup$
To add to @MusaAl-hassy's comment, in computatioal type theory of Bob Constable, Stuart Allen, Bob Harper, et al., $in$ is used routinely for typing judgments because it's more akin to a membership predicate (see this talk, slide 25, for an example).
$endgroup$
– xrq
May 25 at 20:36




3




3




$begingroup$
Surely $3n^2in O(n^2)$ is also an abuse of notation and should really be written $lambda n.3n^2in O(lambda n.n^2)$? (Mathematicians might prefer $nmapsto 3n^2in O(nmapsto n^2)$.)
$endgroup$
– Oscar Cunningham
May 26 at 10:14






$begingroup$
Surely $3n^2in O(n^2)$ is also an abuse of notation and should really be written $lambda n.3n^2in O(lambda n.n^2)$? (Mathematicians might prefer $nmapsto 3n^2in O(nmapsto n^2)$.)
$endgroup$
– Oscar Cunningham
May 26 at 10:14












3 Answers
3






active

oldest

votes


















12














$begingroup$

Because what's on the right of the colon isn't necessarily a set and what's on the left of the colon isn't necessarily a member of that set.



Type theory started out in the early 20th century as an approach to the foundation of mathematics. Bertrand Russel discovered a paradox in naive set theory, and he worked on type theory as a way to limit the expressive power of set theory to avoid this (and any other) paradox. Over the years, Russel and others have defined many theories of types. In some theories of types, types are sets with certain properties, but in others, they're a different kind of beast.



In particular, many theories of types have a syntactic formulation. There are rules that cause a thing to have a type. When the typing rules used as a foundation for a theory, it's important to distinguish what the typing rules say from what one might infer by applying additional external knowledge. This is especially important if the typing rules are a foundation for a proof theory: theorems that hold based on set theory with classical logic and the axiom of choice may or may not hold in a constructive logic, for example. One of the seminal papers in this domain is Church's A Formulation of the Simple Theory of Types (1940)



Perhaps the way in which the distinction between types and sets is the most apparent is that the most basic rule for sets, namely that two sets are equal iff they have the same elements, usually does not apply for types. See Andrej Bauer's answer here and his answer on a related question for some examples. That second thread has other answers worth reading.



In a typed calculus, to say that the types are sets is in fact to give a semantics to the types. Giving a calculus a type-theoretic semantics is not trivial. For example, suppose you're defining a language with functions. What set is a type of a function? Total functions are determined by their graph, as we're taught in set theory 101. But what about partial functions? Do you want to give all non-terminating functions the same semantics? You can't interpret types as sets for a calculus that allows recursive functions until you've answered that question. Giving programming languages or calculi a denotational semantics was a difficult problem in the early 1970s. The seminal paper here is Toward a mathematical semantics for computer languages (1971) by Dana Scott and Christopher Strachey. The Haskell wikibook has a good presentation of the topic.



As I wrote above, a second part of the answer is that even if you have managed to give types a set-theoretical semantics, the thing on the left of the colon isn't always an element of the set. Values have types, but so do other things, such as expressions and variables. For example, an expression in a typed programming language has a type even if it doesn't terminate. You might be willing to conflate integer and $mathbb{Z}$, but (x := 0; while true; do x := x + 1; x) is not an element of $mathbb{Z}$.



I don't know when the colon notation arose for types. It's now standard in semantics, and common in programming languages, but neither Russel nor Church used it. Algol didn't use it, but the heavily Algol-inspired language Pascal did in 1971. I suspect it wasn't the first, though, because many theory papers from the early 1970s use the notation, but I don't know of an earlier use. Interestingly, this was soon after the concepts of types from programming and from logic had been unified — as Simon Martini shows in Several Types of Types in Programming Languages, what was called a “type” in programming languages up to the 1960s came from the vernacular use of the word and not from type theory.






share|cite|improve this answer









$endgroup$























    36














    $begingroup$

    The main reason to prefer the colon notation $t : T$ to the membership relation $t in T$ is that the membership relation can be misleading because types are not (just) collections.



    [Supplemental: I should note that historically type theory was written using $in$. Martin-Löf's conception of type was meant to capture sets constructively, and already Russell and Whitehead used $epsilon$ for the class memebrship. It would be interesting to track down the moment when $:$ became more prevalent than $in$.]



    A type describes a certain kind of construction, i.e., how to make objects with a certain structure, how to use them, and what equations holds about them.



    For instance a product type $A times B$ has introduction rules that explain how to make ordered pairs, and elimination rules explaining that we can project the first and the second components from any element of $A times B$. The definition of $A times B$ does not start with the words "the collection of all ..." and neither does it say anywhere anything like "all elements of $A times B$ are pairs" (but it follows from the definition that every element of $A times B$ is propositionally equal to a pair). In constrast, the set-theoretic definition of $X times Y$ is stated as "the set of all ordered pairs ...".



    The notation $t : T$ signifies the fact that $t$ has the structure described by $T$.



    A type $T$ is not to be confused with its extension, which is the collection of all objects of type $T$. A type is not determined by its extension, just like a group is not determined by its carrier set. Furthermore, it may happen that two types have the same extension, but are different, for instance:




    1. The type of all even primes larger than two: $Sigma (n : mathbb{N}) . mathtt{isprime}(n) times mathtt{iseven}(n) times (n > 2)$.

    2. The type of all odd primes smaller than two: $Sigma (n : mathbb{N}) . mathtt{isprime}(n) times mathtt{isodd}(n) times (n < 2)$.


    The extension of both is empty, but they are not the same type.



    There are further differences between the type-theoretic $:$ and the set-theoretic $in$. An object $a$ in set theory exists independently of what sets it belongs to, and it may belong to several sets. In contrast, most type theories satisfy uniqueness of typing: if $t : T$ and $t : U$ then $T equiv U$. Or to put it differently, a type-theoretic construction $t$ has precisely one type $T$, and in fact there is no way to have just an object $t$ without its (uniquely determined) type.



    Another difference is that in set theory we can deny the fact that $a in A$ by writing $lnot (a in A)$ or $a notin A$. This is not possible in type theory, because $t : T$ is a judgement which can be derived using the rules of type theory, but there is nothing in type theory that would allow us to state that something has not been derived. When a child makes something from LEGO blocks they proudly run to their parents to show them the construction, but they never run to their parents to show them what they didn't make.






    share|cite|improve this answer











    $endgroup$











    • 1




      $begingroup$
      Andrej, great answer. Do you happen to know the historic origin of the colon notation?
      $endgroup$
      – Andreas Rossberg
      May 25 at 16:26










    • $begingroup$
      Alas, I do not. Church's type theory used subscripts, i.e., $x_alpha$ for a variable of type $alpha$. Russell and Whitehead used $epsilon$ for the relation of belonging to a class. Algol 68 puts types in front of variable names. The 1972 Martin-Löf type theory uses $in$, and so does the 1984 version, but the [1994 version] uses a colon.
      $endgroup$
      – Andrej Bauer
      May 25 at 20:39








    • 1




      $begingroup$
      So your argument is that a type is a like a group? That makes sense, but the notation $g in G$ is common in abstract algebra.
      $endgroup$
      – Björn Lindqvist
      May 25 at 21:14






    • 2




      $begingroup$
      @BjörnLindqvist: I don't think this answer is the full story. Even in standard mathematics we use "$f : S→T$" to denote that $f$ is a function from $S$ to $T$. Why did we not use "$f ∈ (S→T)$" or something like that? Well, we just didn't. Of course, there is good reason to avoid the use of "$∈$" in a presentation of certain kinds of type theories, simply because we don't want ZFC-taught people to think it's like ZFC-sets, which obviously isn't the case. But that doesn't mean that the colon hasn't already been widely used long before type theory became popular.
      $endgroup$
      – user21820
      May 26 at 11:44






    • 1




      $begingroup$
      @user21820 "Why didn't we use $fin (Sto T)$?" Just speculating: because mathematicians never thought of $Sto T$ as a set. For the history of this notation see here. I doubt that the colon from $fcolon Sto T$ was the inspiration for type theorists. More likely type theorists colon has to do with the fact that $in$ is not a ASCII character.
      $endgroup$
      – Michael
      May 27 at 14:31



















    5














    $begingroup$

    Björn,



    There's probably an earlier reference but for one thing, the colon was used in the Pascal programming language:



    First Google hit for Pascal






    share|cite|improve this answer









    $endgroup$











    • 2




      $begingroup$
      Weren't there any earlier programming languages that used :?
      $endgroup$
      – Andrej Bauer
      May 25 at 14:05










    • $begingroup$
      @AndrejBauer indeed, I wrote "There's probably an earlier reference but..." to guard against that likely fact.
      $endgroup$
      – Bjørn Kjos-Hanssen
      May 25 at 15:54










    • $begingroup$
      @AndrejBauer Algol didn't. Was : used in theory papers before 1970s?
      $endgroup$
      – Gilles
      May 25 at 20:24






    • 1




      $begingroup$
      Fortran has REAL :: x but I don't know if this came before Pascal.
      $endgroup$
      – Michael
      May 27 at 14:33






    • 1




      $begingroup$
      @Michael Fortran came earlier than Pascal (ca. 1955 vs. ca. 1970), but I think this specific syntax was introduced only in Fortran 90, so a lot later than Pascal. See e.g. here fortranwiki.org/fortran/show/Modernizing+Old+Fortran
      $endgroup$
      – Federico Poloni
      May 28 at 8:27















    Your Answer








    StackExchange.ready(function() {
    var channelOptions = {
    tags: "".split(" "),
    id: "114"
    };
    initTagRenderer("".split(" "), "".split(" "), channelOptions);

    StackExchange.using("externalEditor", function() {
    // Have to fire editor after snippets, if snippets enabled
    if (StackExchange.settings.snippets.snippetsEnabled) {
    StackExchange.using("snippets", function() {
    createEditor();
    });
    }
    else {
    createEditor();
    }
    });

    function createEditor() {
    StackExchange.prepareEditor({
    heartbeatType: 'answer',
    autoActivateHeartbeat: false,
    convertImagesToLinks: false,
    noModals: true,
    showLowRepImageUploadWarning: true,
    reputationToPostImages: null,
    bindNavPrevention: true,
    postfix: "",
    imageUploader: {
    brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
    contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/4.0/"u003ecc by-sa 4.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
    allowUrls: true
    },
    noCode: true, onDemand: true,
    discardSelector: ".discard-answer"
    ,immediatelyShowMarkdownHelp:true
    });


    }
    });















    draft saved

    draft discarded
















    StackExchange.ready(
    function () {
    StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcstheory.stackexchange.com%2fquestions%2f43971%2fwhy-colon-to-denote-that-a-value-belongs-to-a-type%23new-answer', 'question_page');
    }
    );

    Post as a guest















    Required, but never shown

























    3 Answers
    3






    active

    oldest

    votes








    3 Answers
    3






    active

    oldest

    votes









    active

    oldest

    votes






    active

    oldest

    votes









    12














    $begingroup$

    Because what's on the right of the colon isn't necessarily a set and what's on the left of the colon isn't necessarily a member of that set.



    Type theory started out in the early 20th century as an approach to the foundation of mathematics. Bertrand Russel discovered a paradox in naive set theory, and he worked on type theory as a way to limit the expressive power of set theory to avoid this (and any other) paradox. Over the years, Russel and others have defined many theories of types. In some theories of types, types are sets with certain properties, but in others, they're a different kind of beast.



    In particular, many theories of types have a syntactic formulation. There are rules that cause a thing to have a type. When the typing rules used as a foundation for a theory, it's important to distinguish what the typing rules say from what one might infer by applying additional external knowledge. This is especially important if the typing rules are a foundation for a proof theory: theorems that hold based on set theory with classical logic and the axiom of choice may or may not hold in a constructive logic, for example. One of the seminal papers in this domain is Church's A Formulation of the Simple Theory of Types (1940)



    Perhaps the way in which the distinction between types and sets is the most apparent is that the most basic rule for sets, namely that two sets are equal iff they have the same elements, usually does not apply for types. See Andrej Bauer's answer here and his answer on a related question for some examples. That second thread has other answers worth reading.



    In a typed calculus, to say that the types are sets is in fact to give a semantics to the types. Giving a calculus a type-theoretic semantics is not trivial. For example, suppose you're defining a language with functions. What set is a type of a function? Total functions are determined by their graph, as we're taught in set theory 101. But what about partial functions? Do you want to give all non-terminating functions the same semantics? You can't interpret types as sets for a calculus that allows recursive functions until you've answered that question. Giving programming languages or calculi a denotational semantics was a difficult problem in the early 1970s. The seminal paper here is Toward a mathematical semantics for computer languages (1971) by Dana Scott and Christopher Strachey. The Haskell wikibook has a good presentation of the topic.



    As I wrote above, a second part of the answer is that even if you have managed to give types a set-theoretical semantics, the thing on the left of the colon isn't always an element of the set. Values have types, but so do other things, such as expressions and variables. For example, an expression in a typed programming language has a type even if it doesn't terminate. You might be willing to conflate integer and $mathbb{Z}$, but (x := 0; while true; do x := x + 1; x) is not an element of $mathbb{Z}$.



    I don't know when the colon notation arose for types. It's now standard in semantics, and common in programming languages, but neither Russel nor Church used it. Algol didn't use it, but the heavily Algol-inspired language Pascal did in 1971. I suspect it wasn't the first, though, because many theory papers from the early 1970s use the notation, but I don't know of an earlier use. Interestingly, this was soon after the concepts of types from programming and from logic had been unified — as Simon Martini shows in Several Types of Types in Programming Languages, what was called a “type” in programming languages up to the 1960s came from the vernacular use of the word and not from type theory.






    share|cite|improve this answer









    $endgroup$




















      12














      $begingroup$

      Because what's on the right of the colon isn't necessarily a set and what's on the left of the colon isn't necessarily a member of that set.



      Type theory started out in the early 20th century as an approach to the foundation of mathematics. Bertrand Russel discovered a paradox in naive set theory, and he worked on type theory as a way to limit the expressive power of set theory to avoid this (and any other) paradox. Over the years, Russel and others have defined many theories of types. In some theories of types, types are sets with certain properties, but in others, they're a different kind of beast.



      In particular, many theories of types have a syntactic formulation. There are rules that cause a thing to have a type. When the typing rules used as a foundation for a theory, it's important to distinguish what the typing rules say from what one might infer by applying additional external knowledge. This is especially important if the typing rules are a foundation for a proof theory: theorems that hold based on set theory with classical logic and the axiom of choice may or may not hold in a constructive logic, for example. One of the seminal papers in this domain is Church's A Formulation of the Simple Theory of Types (1940)



      Perhaps the way in which the distinction between types and sets is the most apparent is that the most basic rule for sets, namely that two sets are equal iff they have the same elements, usually does not apply for types. See Andrej Bauer's answer here and his answer on a related question for some examples. That second thread has other answers worth reading.



      In a typed calculus, to say that the types are sets is in fact to give a semantics to the types. Giving a calculus a type-theoretic semantics is not trivial. For example, suppose you're defining a language with functions. What set is a type of a function? Total functions are determined by their graph, as we're taught in set theory 101. But what about partial functions? Do you want to give all non-terminating functions the same semantics? You can't interpret types as sets for a calculus that allows recursive functions until you've answered that question. Giving programming languages or calculi a denotational semantics was a difficult problem in the early 1970s. The seminal paper here is Toward a mathematical semantics for computer languages (1971) by Dana Scott and Christopher Strachey. The Haskell wikibook has a good presentation of the topic.



      As I wrote above, a second part of the answer is that even if you have managed to give types a set-theoretical semantics, the thing on the left of the colon isn't always an element of the set. Values have types, but so do other things, such as expressions and variables. For example, an expression in a typed programming language has a type even if it doesn't terminate. You might be willing to conflate integer and $mathbb{Z}$, but (x := 0; while true; do x := x + 1; x) is not an element of $mathbb{Z}$.



      I don't know when the colon notation arose for types. It's now standard in semantics, and common in programming languages, but neither Russel nor Church used it. Algol didn't use it, but the heavily Algol-inspired language Pascal did in 1971. I suspect it wasn't the first, though, because many theory papers from the early 1970s use the notation, but I don't know of an earlier use. Interestingly, this was soon after the concepts of types from programming and from logic had been unified — as Simon Martini shows in Several Types of Types in Programming Languages, what was called a “type” in programming languages up to the 1960s came from the vernacular use of the word and not from type theory.






      share|cite|improve this answer









      $endgroup$


















        12














        12










        12







        $begingroup$

        Because what's on the right of the colon isn't necessarily a set and what's on the left of the colon isn't necessarily a member of that set.



        Type theory started out in the early 20th century as an approach to the foundation of mathematics. Bertrand Russel discovered a paradox in naive set theory, and he worked on type theory as a way to limit the expressive power of set theory to avoid this (and any other) paradox. Over the years, Russel and others have defined many theories of types. In some theories of types, types are sets with certain properties, but in others, they're a different kind of beast.



        In particular, many theories of types have a syntactic formulation. There are rules that cause a thing to have a type. When the typing rules used as a foundation for a theory, it's important to distinguish what the typing rules say from what one might infer by applying additional external knowledge. This is especially important if the typing rules are a foundation for a proof theory: theorems that hold based on set theory with classical logic and the axiom of choice may or may not hold in a constructive logic, for example. One of the seminal papers in this domain is Church's A Formulation of the Simple Theory of Types (1940)



        Perhaps the way in which the distinction between types and sets is the most apparent is that the most basic rule for sets, namely that two sets are equal iff they have the same elements, usually does not apply for types. See Andrej Bauer's answer here and his answer on a related question for some examples. That second thread has other answers worth reading.



        In a typed calculus, to say that the types are sets is in fact to give a semantics to the types. Giving a calculus a type-theoretic semantics is not trivial. For example, suppose you're defining a language with functions. What set is a type of a function? Total functions are determined by their graph, as we're taught in set theory 101. But what about partial functions? Do you want to give all non-terminating functions the same semantics? You can't interpret types as sets for a calculus that allows recursive functions until you've answered that question. Giving programming languages or calculi a denotational semantics was a difficult problem in the early 1970s. The seminal paper here is Toward a mathematical semantics for computer languages (1971) by Dana Scott and Christopher Strachey. The Haskell wikibook has a good presentation of the topic.



        As I wrote above, a second part of the answer is that even if you have managed to give types a set-theoretical semantics, the thing on the left of the colon isn't always an element of the set. Values have types, but so do other things, such as expressions and variables. For example, an expression in a typed programming language has a type even if it doesn't terminate. You might be willing to conflate integer and $mathbb{Z}$, but (x := 0; while true; do x := x + 1; x) is not an element of $mathbb{Z}$.



        I don't know when the colon notation arose for types. It's now standard in semantics, and common in programming languages, but neither Russel nor Church used it. Algol didn't use it, but the heavily Algol-inspired language Pascal did in 1971. I suspect it wasn't the first, though, because many theory papers from the early 1970s use the notation, but I don't know of an earlier use. Interestingly, this was soon after the concepts of types from programming and from logic had been unified — as Simon Martini shows in Several Types of Types in Programming Languages, what was called a “type” in programming languages up to the 1960s came from the vernacular use of the word and not from type theory.






        share|cite|improve this answer









        $endgroup$



        Because what's on the right of the colon isn't necessarily a set and what's on the left of the colon isn't necessarily a member of that set.



        Type theory started out in the early 20th century as an approach to the foundation of mathematics. Bertrand Russel discovered a paradox in naive set theory, and he worked on type theory as a way to limit the expressive power of set theory to avoid this (and any other) paradox. Over the years, Russel and others have defined many theories of types. In some theories of types, types are sets with certain properties, but in others, they're a different kind of beast.



        In particular, many theories of types have a syntactic formulation. There are rules that cause a thing to have a type. When the typing rules used as a foundation for a theory, it's important to distinguish what the typing rules say from what one might infer by applying additional external knowledge. This is especially important if the typing rules are a foundation for a proof theory: theorems that hold based on set theory with classical logic and the axiom of choice may or may not hold in a constructive logic, for example. One of the seminal papers in this domain is Church's A Formulation of the Simple Theory of Types (1940)



        Perhaps the way in which the distinction between types and sets is the most apparent is that the most basic rule for sets, namely that two sets are equal iff they have the same elements, usually does not apply for types. See Andrej Bauer's answer here and his answer on a related question for some examples. That second thread has other answers worth reading.



        In a typed calculus, to say that the types are sets is in fact to give a semantics to the types. Giving a calculus a type-theoretic semantics is not trivial. For example, suppose you're defining a language with functions. What set is a type of a function? Total functions are determined by their graph, as we're taught in set theory 101. But what about partial functions? Do you want to give all non-terminating functions the same semantics? You can't interpret types as sets for a calculus that allows recursive functions until you've answered that question. Giving programming languages or calculi a denotational semantics was a difficult problem in the early 1970s. The seminal paper here is Toward a mathematical semantics for computer languages (1971) by Dana Scott and Christopher Strachey. The Haskell wikibook has a good presentation of the topic.



        As I wrote above, a second part of the answer is that even if you have managed to give types a set-theoretical semantics, the thing on the left of the colon isn't always an element of the set. Values have types, but so do other things, such as expressions and variables. For example, an expression in a typed programming language has a type even if it doesn't terminate. You might be willing to conflate integer and $mathbb{Z}$, but (x := 0; while true; do x := x + 1; x) is not an element of $mathbb{Z}$.



        I don't know when the colon notation arose for types. It's now standard in semantics, and common in programming languages, but neither Russel nor Church used it. Algol didn't use it, but the heavily Algol-inspired language Pascal did in 1971. I suspect it wasn't the first, though, because many theory papers from the early 1970s use the notation, but I don't know of an earlier use. Interestingly, this was soon after the concepts of types from programming and from logic had been unified — as Simon Martini shows in Several Types of Types in Programming Languages, what was called a “type” in programming languages up to the 1960s came from the vernacular use of the word and not from type theory.







        share|cite|improve this answer












        share|cite|improve this answer



        share|cite|improve this answer










        answered May 25 at 20:23









        GillesGilles

        2,3471 gold badge23 silver badges33 bronze badges




        2,3471 gold badge23 silver badges33 bronze badges




























            36














            $begingroup$

            The main reason to prefer the colon notation $t : T$ to the membership relation $t in T$ is that the membership relation can be misleading because types are not (just) collections.



            [Supplemental: I should note that historically type theory was written using $in$. Martin-Löf's conception of type was meant to capture sets constructively, and already Russell and Whitehead used $epsilon$ for the class memebrship. It would be interesting to track down the moment when $:$ became more prevalent than $in$.]



            A type describes a certain kind of construction, i.e., how to make objects with a certain structure, how to use them, and what equations holds about them.



            For instance a product type $A times B$ has introduction rules that explain how to make ordered pairs, and elimination rules explaining that we can project the first and the second components from any element of $A times B$. The definition of $A times B$ does not start with the words "the collection of all ..." and neither does it say anywhere anything like "all elements of $A times B$ are pairs" (but it follows from the definition that every element of $A times B$ is propositionally equal to a pair). In constrast, the set-theoretic definition of $X times Y$ is stated as "the set of all ordered pairs ...".



            The notation $t : T$ signifies the fact that $t$ has the structure described by $T$.



            A type $T$ is not to be confused with its extension, which is the collection of all objects of type $T$. A type is not determined by its extension, just like a group is not determined by its carrier set. Furthermore, it may happen that two types have the same extension, but are different, for instance:




            1. The type of all even primes larger than two: $Sigma (n : mathbb{N}) . mathtt{isprime}(n) times mathtt{iseven}(n) times (n > 2)$.

            2. The type of all odd primes smaller than two: $Sigma (n : mathbb{N}) . mathtt{isprime}(n) times mathtt{isodd}(n) times (n < 2)$.


            The extension of both is empty, but they are not the same type.



            There are further differences between the type-theoretic $:$ and the set-theoretic $in$. An object $a$ in set theory exists independently of what sets it belongs to, and it may belong to several sets. In contrast, most type theories satisfy uniqueness of typing: if $t : T$ and $t : U$ then $T equiv U$. Or to put it differently, a type-theoretic construction $t$ has precisely one type $T$, and in fact there is no way to have just an object $t$ without its (uniquely determined) type.



            Another difference is that in set theory we can deny the fact that $a in A$ by writing $lnot (a in A)$ or $a notin A$. This is not possible in type theory, because $t : T$ is a judgement which can be derived using the rules of type theory, but there is nothing in type theory that would allow us to state that something has not been derived. When a child makes something from LEGO blocks they proudly run to their parents to show them the construction, but they never run to their parents to show them what they didn't make.






            share|cite|improve this answer











            $endgroup$











            • 1




              $begingroup$
              Andrej, great answer. Do you happen to know the historic origin of the colon notation?
              $endgroup$
              – Andreas Rossberg
              May 25 at 16:26










            • $begingroup$
              Alas, I do not. Church's type theory used subscripts, i.e., $x_alpha$ for a variable of type $alpha$. Russell and Whitehead used $epsilon$ for the relation of belonging to a class. Algol 68 puts types in front of variable names. The 1972 Martin-Löf type theory uses $in$, and so does the 1984 version, but the [1994 version] uses a colon.
              $endgroup$
              – Andrej Bauer
              May 25 at 20:39








            • 1




              $begingroup$
              So your argument is that a type is a like a group? That makes sense, but the notation $g in G$ is common in abstract algebra.
              $endgroup$
              – Björn Lindqvist
              May 25 at 21:14






            • 2




              $begingroup$
              @BjörnLindqvist: I don't think this answer is the full story. Even in standard mathematics we use "$f : S→T$" to denote that $f$ is a function from $S$ to $T$. Why did we not use "$f ∈ (S→T)$" or something like that? Well, we just didn't. Of course, there is good reason to avoid the use of "$∈$" in a presentation of certain kinds of type theories, simply because we don't want ZFC-taught people to think it's like ZFC-sets, which obviously isn't the case. But that doesn't mean that the colon hasn't already been widely used long before type theory became popular.
              $endgroup$
              – user21820
              May 26 at 11:44






            • 1




              $begingroup$
              @user21820 "Why didn't we use $fin (Sto T)$?" Just speculating: because mathematicians never thought of $Sto T$ as a set. For the history of this notation see here. I doubt that the colon from $fcolon Sto T$ was the inspiration for type theorists. More likely type theorists colon has to do with the fact that $in$ is not a ASCII character.
              $endgroup$
              – Michael
              May 27 at 14:31
















            36














            $begingroup$

            The main reason to prefer the colon notation $t : T$ to the membership relation $t in T$ is that the membership relation can be misleading because types are not (just) collections.



            [Supplemental: I should note that historically type theory was written using $in$. Martin-Löf's conception of type was meant to capture sets constructively, and already Russell and Whitehead used $epsilon$ for the class memebrship. It would be interesting to track down the moment when $:$ became more prevalent than $in$.]



            A type describes a certain kind of construction, i.e., how to make objects with a certain structure, how to use them, and what equations holds about them.



            For instance a product type $A times B$ has introduction rules that explain how to make ordered pairs, and elimination rules explaining that we can project the first and the second components from any element of $A times B$. The definition of $A times B$ does not start with the words "the collection of all ..." and neither does it say anywhere anything like "all elements of $A times B$ are pairs" (but it follows from the definition that every element of $A times B$ is propositionally equal to a pair). In constrast, the set-theoretic definition of $X times Y$ is stated as "the set of all ordered pairs ...".



            The notation $t : T$ signifies the fact that $t$ has the structure described by $T$.



            A type $T$ is not to be confused with its extension, which is the collection of all objects of type $T$. A type is not determined by its extension, just like a group is not determined by its carrier set. Furthermore, it may happen that two types have the same extension, but are different, for instance:




            1. The type of all even primes larger than two: $Sigma (n : mathbb{N}) . mathtt{isprime}(n) times mathtt{iseven}(n) times (n > 2)$.

            2. The type of all odd primes smaller than two: $Sigma (n : mathbb{N}) . mathtt{isprime}(n) times mathtt{isodd}(n) times (n < 2)$.


            The extension of both is empty, but they are not the same type.



            There are further differences between the type-theoretic $:$ and the set-theoretic $in$. An object $a$ in set theory exists independently of what sets it belongs to, and it may belong to several sets. In contrast, most type theories satisfy uniqueness of typing: if $t : T$ and $t : U$ then $T equiv U$. Or to put it differently, a type-theoretic construction $t$ has precisely one type $T$, and in fact there is no way to have just an object $t$ without its (uniquely determined) type.



            Another difference is that in set theory we can deny the fact that $a in A$ by writing $lnot (a in A)$ or $a notin A$. This is not possible in type theory, because $t : T$ is a judgement which can be derived using the rules of type theory, but there is nothing in type theory that would allow us to state that something has not been derived. When a child makes something from LEGO blocks they proudly run to their parents to show them the construction, but they never run to their parents to show them what they didn't make.






            share|cite|improve this answer











            $endgroup$











            • 1




              $begingroup$
              Andrej, great answer. Do you happen to know the historic origin of the colon notation?
              $endgroup$
              – Andreas Rossberg
              May 25 at 16:26










            • $begingroup$
              Alas, I do not. Church's type theory used subscripts, i.e., $x_alpha$ for a variable of type $alpha$. Russell and Whitehead used $epsilon$ for the relation of belonging to a class. Algol 68 puts types in front of variable names. The 1972 Martin-Löf type theory uses $in$, and so does the 1984 version, but the [1994 version] uses a colon.
              $endgroup$
              – Andrej Bauer
              May 25 at 20:39








            • 1




              $begingroup$
              So your argument is that a type is a like a group? That makes sense, but the notation $g in G$ is common in abstract algebra.
              $endgroup$
              – Björn Lindqvist
              May 25 at 21:14






            • 2




              $begingroup$
              @BjörnLindqvist: I don't think this answer is the full story. Even in standard mathematics we use "$f : S→T$" to denote that $f$ is a function from $S$ to $T$. Why did we not use "$f ∈ (S→T)$" or something like that? Well, we just didn't. Of course, there is good reason to avoid the use of "$∈$" in a presentation of certain kinds of type theories, simply because we don't want ZFC-taught people to think it's like ZFC-sets, which obviously isn't the case. But that doesn't mean that the colon hasn't already been widely used long before type theory became popular.
              $endgroup$
              – user21820
              May 26 at 11:44






            • 1




              $begingroup$
              @user21820 "Why didn't we use $fin (Sto T)$?" Just speculating: because mathematicians never thought of $Sto T$ as a set. For the history of this notation see here. I doubt that the colon from $fcolon Sto T$ was the inspiration for type theorists. More likely type theorists colon has to do with the fact that $in$ is not a ASCII character.
              $endgroup$
              – Michael
              May 27 at 14:31














            36














            36










            36







            $begingroup$

            The main reason to prefer the colon notation $t : T$ to the membership relation $t in T$ is that the membership relation can be misleading because types are not (just) collections.



            [Supplemental: I should note that historically type theory was written using $in$. Martin-Löf's conception of type was meant to capture sets constructively, and already Russell and Whitehead used $epsilon$ for the class memebrship. It would be interesting to track down the moment when $:$ became more prevalent than $in$.]



            A type describes a certain kind of construction, i.e., how to make objects with a certain structure, how to use them, and what equations holds about them.



            For instance a product type $A times B$ has introduction rules that explain how to make ordered pairs, and elimination rules explaining that we can project the first and the second components from any element of $A times B$. The definition of $A times B$ does not start with the words "the collection of all ..." and neither does it say anywhere anything like "all elements of $A times B$ are pairs" (but it follows from the definition that every element of $A times B$ is propositionally equal to a pair). In constrast, the set-theoretic definition of $X times Y$ is stated as "the set of all ordered pairs ...".



            The notation $t : T$ signifies the fact that $t$ has the structure described by $T$.



            A type $T$ is not to be confused with its extension, which is the collection of all objects of type $T$. A type is not determined by its extension, just like a group is not determined by its carrier set. Furthermore, it may happen that two types have the same extension, but are different, for instance:




            1. The type of all even primes larger than two: $Sigma (n : mathbb{N}) . mathtt{isprime}(n) times mathtt{iseven}(n) times (n > 2)$.

            2. The type of all odd primes smaller than two: $Sigma (n : mathbb{N}) . mathtt{isprime}(n) times mathtt{isodd}(n) times (n < 2)$.


            The extension of both is empty, but they are not the same type.



            There are further differences between the type-theoretic $:$ and the set-theoretic $in$. An object $a$ in set theory exists independently of what sets it belongs to, and it may belong to several sets. In contrast, most type theories satisfy uniqueness of typing: if $t : T$ and $t : U$ then $T equiv U$. Or to put it differently, a type-theoretic construction $t$ has precisely one type $T$, and in fact there is no way to have just an object $t$ without its (uniquely determined) type.



            Another difference is that in set theory we can deny the fact that $a in A$ by writing $lnot (a in A)$ or $a notin A$. This is not possible in type theory, because $t : T$ is a judgement which can be derived using the rules of type theory, but there is nothing in type theory that would allow us to state that something has not been derived. When a child makes something from LEGO blocks they proudly run to their parents to show them the construction, but they never run to their parents to show them what they didn't make.






            share|cite|improve this answer











            $endgroup$



            The main reason to prefer the colon notation $t : T$ to the membership relation $t in T$ is that the membership relation can be misleading because types are not (just) collections.



            [Supplemental: I should note that historically type theory was written using $in$. Martin-Löf's conception of type was meant to capture sets constructively, and already Russell and Whitehead used $epsilon$ for the class memebrship. It would be interesting to track down the moment when $:$ became more prevalent than $in$.]



            A type describes a certain kind of construction, i.e., how to make objects with a certain structure, how to use them, and what equations holds about them.



            For instance a product type $A times B$ has introduction rules that explain how to make ordered pairs, and elimination rules explaining that we can project the first and the second components from any element of $A times B$. The definition of $A times B$ does not start with the words "the collection of all ..." and neither does it say anywhere anything like "all elements of $A times B$ are pairs" (but it follows from the definition that every element of $A times B$ is propositionally equal to a pair). In constrast, the set-theoretic definition of $X times Y$ is stated as "the set of all ordered pairs ...".



            The notation $t : T$ signifies the fact that $t$ has the structure described by $T$.



            A type $T$ is not to be confused with its extension, which is the collection of all objects of type $T$. A type is not determined by its extension, just like a group is not determined by its carrier set. Furthermore, it may happen that two types have the same extension, but are different, for instance:




            1. The type of all even primes larger than two: $Sigma (n : mathbb{N}) . mathtt{isprime}(n) times mathtt{iseven}(n) times (n > 2)$.

            2. The type of all odd primes smaller than two: $Sigma (n : mathbb{N}) . mathtt{isprime}(n) times mathtt{isodd}(n) times (n < 2)$.


            The extension of both is empty, but they are not the same type.



            There are further differences between the type-theoretic $:$ and the set-theoretic $in$. An object $a$ in set theory exists independently of what sets it belongs to, and it may belong to several sets. In contrast, most type theories satisfy uniqueness of typing: if $t : T$ and $t : U$ then $T equiv U$. Or to put it differently, a type-theoretic construction $t$ has precisely one type $T$, and in fact there is no way to have just an object $t$ without its (uniquely determined) type.



            Another difference is that in set theory we can deny the fact that $a in A$ by writing $lnot (a in A)$ or $a notin A$. This is not possible in type theory, because $t : T$ is a judgement which can be derived using the rules of type theory, but there is nothing in type theory that would allow us to state that something has not been derived. When a child makes something from LEGO blocks they proudly run to their parents to show them the construction, but they never run to their parents to show them what they didn't make.







            share|cite|improve this answer














            share|cite|improve this answer



            share|cite|improve this answer








            edited May 28 at 8:00

























            answered May 25 at 13:43









            Andrej BauerAndrej Bauer

            22.6k1 gold badge60 silver badges108 bronze badges




            22.6k1 gold badge60 silver badges108 bronze badges











            • 1




              $begingroup$
              Andrej, great answer. Do you happen to know the historic origin of the colon notation?
              $endgroup$
              – Andreas Rossberg
              May 25 at 16:26










            • $begingroup$
              Alas, I do not. Church's type theory used subscripts, i.e., $x_alpha$ for a variable of type $alpha$. Russell and Whitehead used $epsilon$ for the relation of belonging to a class. Algol 68 puts types in front of variable names. The 1972 Martin-Löf type theory uses $in$, and so does the 1984 version, but the [1994 version] uses a colon.
              $endgroup$
              – Andrej Bauer
              May 25 at 20:39








            • 1




              $begingroup$
              So your argument is that a type is a like a group? That makes sense, but the notation $g in G$ is common in abstract algebra.
              $endgroup$
              – Björn Lindqvist
              May 25 at 21:14






            • 2




              $begingroup$
              @BjörnLindqvist: I don't think this answer is the full story. Even in standard mathematics we use "$f : S→T$" to denote that $f$ is a function from $S$ to $T$. Why did we not use "$f ∈ (S→T)$" or something like that? Well, we just didn't. Of course, there is good reason to avoid the use of "$∈$" in a presentation of certain kinds of type theories, simply because we don't want ZFC-taught people to think it's like ZFC-sets, which obviously isn't the case. But that doesn't mean that the colon hasn't already been widely used long before type theory became popular.
              $endgroup$
              – user21820
              May 26 at 11:44






            • 1




              $begingroup$
              @user21820 "Why didn't we use $fin (Sto T)$?" Just speculating: because mathematicians never thought of $Sto T$ as a set. For the history of this notation see here. I doubt that the colon from $fcolon Sto T$ was the inspiration for type theorists. More likely type theorists colon has to do with the fact that $in$ is not a ASCII character.
              $endgroup$
              – Michael
              May 27 at 14:31














            • 1




              $begingroup$
              Andrej, great answer. Do you happen to know the historic origin of the colon notation?
              $endgroup$
              – Andreas Rossberg
              May 25 at 16:26










            • $begingroup$
              Alas, I do not. Church's type theory used subscripts, i.e., $x_alpha$ for a variable of type $alpha$. Russell and Whitehead used $epsilon$ for the relation of belonging to a class. Algol 68 puts types in front of variable names. The 1972 Martin-Löf type theory uses $in$, and so does the 1984 version, but the [1994 version] uses a colon.
              $endgroup$
              – Andrej Bauer
              May 25 at 20:39








            • 1




              $begingroup$
              So your argument is that a type is a like a group? That makes sense, but the notation $g in G$ is common in abstract algebra.
              $endgroup$
              – Björn Lindqvist
              May 25 at 21:14






            • 2




              $begingroup$
              @BjörnLindqvist: I don't think this answer is the full story. Even in standard mathematics we use "$f : S→T$" to denote that $f$ is a function from $S$ to $T$. Why did we not use "$f ∈ (S→T)$" or something like that? Well, we just didn't. Of course, there is good reason to avoid the use of "$∈$" in a presentation of certain kinds of type theories, simply because we don't want ZFC-taught people to think it's like ZFC-sets, which obviously isn't the case. But that doesn't mean that the colon hasn't already been widely used long before type theory became popular.
              $endgroup$
              – user21820
              May 26 at 11:44






            • 1




              $begingroup$
              @user21820 "Why didn't we use $fin (Sto T)$?" Just speculating: because mathematicians never thought of $Sto T$ as a set. For the history of this notation see here. I doubt that the colon from $fcolon Sto T$ was the inspiration for type theorists. More likely type theorists colon has to do with the fact that $in$ is not a ASCII character.
              $endgroup$
              – Michael
              May 27 at 14:31








            1




            1




            $begingroup$
            Andrej, great answer. Do you happen to know the historic origin of the colon notation?
            $endgroup$
            – Andreas Rossberg
            May 25 at 16:26




            $begingroup$
            Andrej, great answer. Do you happen to know the historic origin of the colon notation?
            $endgroup$
            – Andreas Rossberg
            May 25 at 16:26












            $begingroup$
            Alas, I do not. Church's type theory used subscripts, i.e., $x_alpha$ for a variable of type $alpha$. Russell and Whitehead used $epsilon$ for the relation of belonging to a class. Algol 68 puts types in front of variable names. The 1972 Martin-Löf type theory uses $in$, and so does the 1984 version, but the [1994 version] uses a colon.
            $endgroup$
            – Andrej Bauer
            May 25 at 20:39






            $begingroup$
            Alas, I do not. Church's type theory used subscripts, i.e., $x_alpha$ for a variable of type $alpha$. Russell and Whitehead used $epsilon$ for the relation of belonging to a class. Algol 68 puts types in front of variable names. The 1972 Martin-Löf type theory uses $in$, and so does the 1984 version, but the [1994 version] uses a colon.
            $endgroup$
            – Andrej Bauer
            May 25 at 20:39






            1




            1




            $begingroup$
            So your argument is that a type is a like a group? That makes sense, but the notation $g in G$ is common in abstract algebra.
            $endgroup$
            – Björn Lindqvist
            May 25 at 21:14




            $begingroup$
            So your argument is that a type is a like a group? That makes sense, but the notation $g in G$ is common in abstract algebra.
            $endgroup$
            – Björn Lindqvist
            May 25 at 21:14




            2




            2




            $begingroup$
            @BjörnLindqvist: I don't think this answer is the full story. Even in standard mathematics we use "$f : S→T$" to denote that $f$ is a function from $S$ to $T$. Why did we not use "$f ∈ (S→T)$" or something like that? Well, we just didn't. Of course, there is good reason to avoid the use of "$∈$" in a presentation of certain kinds of type theories, simply because we don't want ZFC-taught people to think it's like ZFC-sets, which obviously isn't the case. But that doesn't mean that the colon hasn't already been widely used long before type theory became popular.
            $endgroup$
            – user21820
            May 26 at 11:44




            $begingroup$
            @BjörnLindqvist: I don't think this answer is the full story. Even in standard mathematics we use "$f : S→T$" to denote that $f$ is a function from $S$ to $T$. Why did we not use "$f ∈ (S→T)$" or something like that? Well, we just didn't. Of course, there is good reason to avoid the use of "$∈$" in a presentation of certain kinds of type theories, simply because we don't want ZFC-taught people to think it's like ZFC-sets, which obviously isn't the case. But that doesn't mean that the colon hasn't already been widely used long before type theory became popular.
            $endgroup$
            – user21820
            May 26 at 11:44




            1




            1




            $begingroup$
            @user21820 "Why didn't we use $fin (Sto T)$?" Just speculating: because mathematicians never thought of $Sto T$ as a set. For the history of this notation see here. I doubt that the colon from $fcolon Sto T$ was the inspiration for type theorists. More likely type theorists colon has to do with the fact that $in$ is not a ASCII character.
            $endgroup$
            – Michael
            May 27 at 14:31




            $begingroup$
            @user21820 "Why didn't we use $fin (Sto T)$?" Just speculating: because mathematicians never thought of $Sto T$ as a set. For the history of this notation see here. I doubt that the colon from $fcolon Sto T$ was the inspiration for type theorists. More likely type theorists colon has to do with the fact that $in$ is not a ASCII character.
            $endgroup$
            – Michael
            May 27 at 14:31











            5














            $begingroup$

            Björn,



            There's probably an earlier reference but for one thing, the colon was used in the Pascal programming language:



            First Google hit for Pascal






            share|cite|improve this answer









            $endgroup$











            • 2




              $begingroup$
              Weren't there any earlier programming languages that used :?
              $endgroup$
              – Andrej Bauer
              May 25 at 14:05










            • $begingroup$
              @AndrejBauer indeed, I wrote "There's probably an earlier reference but..." to guard against that likely fact.
              $endgroup$
              – Bjørn Kjos-Hanssen
              May 25 at 15:54










            • $begingroup$
              @AndrejBauer Algol didn't. Was : used in theory papers before 1970s?
              $endgroup$
              – Gilles
              May 25 at 20:24






            • 1




              $begingroup$
              Fortran has REAL :: x but I don't know if this came before Pascal.
              $endgroup$
              – Michael
              May 27 at 14:33






            • 1




              $begingroup$
              @Michael Fortran came earlier than Pascal (ca. 1955 vs. ca. 1970), but I think this specific syntax was introduced only in Fortran 90, so a lot later than Pascal. See e.g. here fortranwiki.org/fortran/show/Modernizing+Old+Fortran
              $endgroup$
              – Federico Poloni
              May 28 at 8:27


















            5














            $begingroup$

            Björn,



            There's probably an earlier reference but for one thing, the colon was used in the Pascal programming language:



            First Google hit for Pascal






            share|cite|improve this answer









            $endgroup$











            • 2




              $begingroup$
              Weren't there any earlier programming languages that used :?
              $endgroup$
              – Andrej Bauer
              May 25 at 14:05










            • $begingroup$
              @AndrejBauer indeed, I wrote "There's probably an earlier reference but..." to guard against that likely fact.
              $endgroup$
              – Bjørn Kjos-Hanssen
              May 25 at 15:54










            • $begingroup$
              @AndrejBauer Algol didn't. Was : used in theory papers before 1970s?
              $endgroup$
              – Gilles
              May 25 at 20:24






            • 1




              $begingroup$
              Fortran has REAL :: x but I don't know if this came before Pascal.
              $endgroup$
              – Michael
              May 27 at 14:33






            • 1




              $begingroup$
              @Michael Fortran came earlier than Pascal (ca. 1955 vs. ca. 1970), but I think this specific syntax was introduced only in Fortran 90, so a lot later than Pascal. See e.g. here fortranwiki.org/fortran/show/Modernizing+Old+Fortran
              $endgroup$
              – Federico Poloni
              May 28 at 8:27
















            5














            5










            5







            $begingroup$

            Björn,



            There's probably an earlier reference but for one thing, the colon was used in the Pascal programming language:



            First Google hit for Pascal






            share|cite|improve this answer









            $endgroup$



            Björn,



            There's probably an earlier reference but for one thing, the colon was used in the Pascal programming language:



            First Google hit for Pascal







            share|cite|improve this answer












            share|cite|improve this answer



            share|cite|improve this answer










            answered May 25 at 2:24









            Bjørn Kjos-HanssenBjørn Kjos-Hanssen

            3,8632 gold badges19 silver badges37 bronze badges




            3,8632 gold badges19 silver badges37 bronze badges











            • 2




              $begingroup$
              Weren't there any earlier programming languages that used :?
              $endgroup$
              – Andrej Bauer
              May 25 at 14:05










            • $begingroup$
              @AndrejBauer indeed, I wrote "There's probably an earlier reference but..." to guard against that likely fact.
              $endgroup$
              – Bjørn Kjos-Hanssen
              May 25 at 15:54










            • $begingroup$
              @AndrejBauer Algol didn't. Was : used in theory papers before 1970s?
              $endgroup$
              – Gilles
              May 25 at 20:24






            • 1




              $begingroup$
              Fortran has REAL :: x but I don't know if this came before Pascal.
              $endgroup$
              – Michael
              May 27 at 14:33






            • 1




              $begingroup$
              @Michael Fortran came earlier than Pascal (ca. 1955 vs. ca. 1970), but I think this specific syntax was introduced only in Fortran 90, so a lot later than Pascal. See e.g. here fortranwiki.org/fortran/show/Modernizing+Old+Fortran
              $endgroup$
              – Federico Poloni
              May 28 at 8:27
















            • 2




              $begingroup$
              Weren't there any earlier programming languages that used :?
              $endgroup$
              – Andrej Bauer
              May 25 at 14:05










            • $begingroup$
              @AndrejBauer indeed, I wrote "There's probably an earlier reference but..." to guard against that likely fact.
              $endgroup$
              – Bjørn Kjos-Hanssen
              May 25 at 15:54










            • $begingroup$
              @AndrejBauer Algol didn't. Was : used in theory papers before 1970s?
              $endgroup$
              – Gilles
              May 25 at 20:24






            • 1




              $begingroup$
              Fortran has REAL :: x but I don't know if this came before Pascal.
              $endgroup$
              – Michael
              May 27 at 14:33






            • 1




              $begingroup$
              @Michael Fortran came earlier than Pascal (ca. 1955 vs. ca. 1970), but I think this specific syntax was introduced only in Fortran 90, so a lot later than Pascal. See e.g. here fortranwiki.org/fortran/show/Modernizing+Old+Fortran
              $endgroup$
              – Federico Poloni
              May 28 at 8:27










            2




            2




            $begingroup$
            Weren't there any earlier programming languages that used :?
            $endgroup$
            – Andrej Bauer
            May 25 at 14:05




            $begingroup$
            Weren't there any earlier programming languages that used :?
            $endgroup$
            – Andrej Bauer
            May 25 at 14:05












            $begingroup$
            @AndrejBauer indeed, I wrote "There's probably an earlier reference but..." to guard against that likely fact.
            $endgroup$
            – Bjørn Kjos-Hanssen
            May 25 at 15:54




            $begingroup$
            @AndrejBauer indeed, I wrote "There's probably an earlier reference but..." to guard against that likely fact.
            $endgroup$
            – Bjørn Kjos-Hanssen
            May 25 at 15:54












            $begingroup$
            @AndrejBauer Algol didn't. Was : used in theory papers before 1970s?
            $endgroup$
            – Gilles
            May 25 at 20:24




            $begingroup$
            @AndrejBauer Algol didn't. Was : used in theory papers before 1970s?
            $endgroup$
            – Gilles
            May 25 at 20:24




            1




            1




            $begingroup$
            Fortran has REAL :: x but I don't know if this came before Pascal.
            $endgroup$
            – Michael
            May 27 at 14:33




            $begingroup$
            Fortran has REAL :: x but I don't know if this came before Pascal.
            $endgroup$
            – Michael
            May 27 at 14:33




            1




            1




            $begingroup$
            @Michael Fortran came earlier than Pascal (ca. 1955 vs. ca. 1970), but I think this specific syntax was introduced only in Fortran 90, so a lot later than Pascal. See e.g. here fortranwiki.org/fortran/show/Modernizing+Old+Fortran
            $endgroup$
            – Federico Poloni
            May 28 at 8:27






            $begingroup$
            @Michael Fortran came earlier than Pascal (ca. 1955 vs. ca. 1970), but I think this specific syntax was introduced only in Fortran 90, so a lot later than Pascal. See e.g. here fortranwiki.org/fortran/show/Modernizing+Old+Fortran
            $endgroup$
            – Federico Poloni
            May 28 at 8:27





















            draft saved

            draft discarded



















































            Thanks for contributing an answer to Theoretical Computer Science Stack Exchange!


            • Please be sure to answer the question. Provide details and share your research!

            But avoid



            • Asking for help, clarification, or responding to other answers.

            • Making statements based on opinion; back them up with references or personal experience.


            Use MathJax to format equations. MathJax reference.


            To learn more, see our tips on writing great answers.




            draft saved


            draft discarded














            StackExchange.ready(
            function () {
            StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcstheory.stackexchange.com%2fquestions%2f43971%2fwhy-colon-to-denote-that-a-value-belongs-to-a-type%23new-answer', 'question_page');
            }
            );

            Post as a guest















            Required, but never shown





















































            Required, but never shown














            Required, but never shown












            Required, but never shown







            Required, but never shown

































            Required, but never shown














            Required, but never shown












            Required, but never shown







            Required, but never shown







            Popular posts from this blog

            Færeyskur hestur Heimild | Tengill | Tilvísanir | LeiðsagnarvalRossið - síða um færeyska hrossið á færeyskuGott ár hjá færeyska hestinum

            He _____ here since 1970 . Answer needed [closed]What does “since he was so high” mean?Meaning of “catch birds for”?How do I ensure “since” takes the meaning I want?“Who cares here” meaningWhat does “right round toward” mean?the time tense (had now been detected)What does the phrase “ring around the roses” mean here?Correct usage of “visited upon”Meaning of “foiled rail sabotage bid”It was the third time I had gone to Rome or It is the third time I had been to Rome

            Slayer Innehåll Historia | Stil, komposition och lyrik | Bandets betydelse och framgångar | Sidoprojekt och samarbeten | Kontroverser | Medlemmar | Utmärkelser och nomineringar | Turnéer och festivaler | Diskografi | Referenser | Externa länkar | Navigeringsmenywww.slayer.net”Metal Massacre vol. 1””Metal Massacre vol. 3””Metal Massacre Volume III””Show No Mercy””Haunting the Chapel””Live Undead””Hell Awaits””Reign in Blood””Reign in Blood””Gold & Platinum – Reign in Blood””Golden Gods Awards Winners”originalet”Kerrang! Hall Of Fame””Slayer Looks Back On 37-Year Career In New Video Series: Part Two””South of Heaven””Gold & Platinum – South of Heaven””Seasons in the Abyss””Gold & Platinum - Seasons in the Abyss””Divine Intervention””Divine Intervention - Release group by Slayer””Gold & Platinum - Divine Intervention””Live Intrusion””Undisputed Attitude””Abolish Government/Superficial Love””Release “Slatanic Slaughter: A Tribute to Slayer” by Various Artists””Diabolus in Musica””Soundtrack to the Apocalypse””God Hates Us All””Systematic - Relationships””War at the Warfield””Gold & Platinum - War at the Warfield””Soundtrack to the Apocalypse””Gold & Platinum - Still Reigning””Metallica, Slayer, Iron Mauden Among Winners At Metal Hammer Awards””Eternal Pyre””Eternal Pyre - Slayer release group””Eternal Pyre””Metal Storm Awards 2006””Kerrang! Hall Of Fame””Slayer Wins 'Best Metal' Grammy Award””Slayer Guitarist Jeff Hanneman Dies””Bullet-For My Valentine booed at Metal Hammer Golden Gods Awards””Unholy Aliance””The End Of Slayer?””Slayer: We Could Thrash Out Two More Albums If We're Fast Enough...””'The Unholy Alliance: Chapter III' UK Dates Added”originalet”Megadeth And Slayer To Co-Headline 'Canadian Carnage' Trek”originalet”World Painted Blood””Release “World Painted Blood” by Slayer””Metallica Heading To Cinemas””Slayer, Megadeth To Join Forces For 'European Carnage' Tour - Dec. 18, 2010”originalet”Slayer's Hanneman Contracts Acute Infection; Band To Bring In Guest Guitarist””Cannibal Corpse's Pat O'Brien Will Step In As Slayer's Guest Guitarist”originalet”Slayer’s Jeff Hanneman Dead at 49””Dave Lombardo Says He Made Only $67,000 In 2011 While Touring With Slayer””Slayer: We Do Not Agree With Dave Lombardo's Substance Or Timeline Of Events””Slayer Welcomes Drummer Paul Bostaph Back To The Fold””Slayer Hope to Unveil Never-Before-Heard Jeff Hanneman Material on Next Album””Slayer Debut New Song 'Implode' During Surprise Golden Gods Appearance””Release group Repentless by Slayer””Repentless - Slayer - Credits””Slayer””Metal Storm Awards 2015””Slayer - to release comic book "Repentless #1"””Slayer To Release 'Repentless' 6.66" Vinyl Box Set””BREAKING NEWS: Slayer Announce Farewell Tour””Slayer Recruit Lamb of God, Anthrax, Behemoth + Testament for Final Tour””Slayer lägger ner efter 37 år””Slayer Announces Second North American Leg Of 'Final' Tour””Final World Tour””Slayer Announces Final European Tour With Lamb of God, Anthrax And Obituary””Slayer To Tour Europe With Lamb of God, Anthrax And Obituary””Slayer To Play 'Last French Show Ever' At Next Year's Hellfst””Slayer's Final World Tour Will Extend Into 2019””Death Angel's Rob Cavestany On Slayer's 'Farewell' Tour: 'Some Of Us Could See This Coming'””Testament Has No Plans To Retire Anytime Soon, Says Chuck Billy””Anthrax's Scott Ian On Slayer's 'Farewell' Tour Plans: 'I Was Surprised And I Wasn't Surprised'””Slayer””Slayer's Morbid Schlock””Review/Rock; For Slayer, the Mania Is the Message””Slayer - Biography””Slayer - Reign In Blood”originalet”Dave Lombardo””An exclusive oral history of Slayer”originalet”Exclusive! Interview With Slayer Guitarist Jeff Hanneman”originalet”Thinking Out Loud: Slayer's Kerry King on hair metal, Satan and being polite””Slayer Lyrics””Slayer - Biography””Most influential artists for extreme metal music””Slayer - Reign in Blood””Slayer guitarist Jeff Hanneman dies aged 49””Slatanic Slaughter: A Tribute to Slayer””Gateway to Hell: A Tribute to Slayer””Covered In Blood””Slayer: The Origins of Thrash in San Francisco, CA.””Why They Rule - #6 Slayer”originalet”Guitar World's 100 Greatest Heavy Metal Guitarists Of All Time”originalet”The fans have spoken: Slayer comes out on top in readers' polls”originalet”Tribute to Jeff Hanneman (1964-2013)””Lamb Of God Frontman: We Sound Like A Slayer Rip-Off””BEHEMOTH Frontman Pays Tribute To SLAYER's JEFF HANNEMAN””Slayer, Hatebreed Doing Double Duty On This Year's Ozzfest””System of a Down””Lacuna Coil’s Andrea Ferro Talks Influences, Skateboarding, Band Origins + More””Slayer - Reign in Blood””Into The Lungs of Hell””Slayer rules - en utställning om fans””Slayer and Their Fans Slashed Through a No-Holds-Barred Night at Gas Monkey””Home””Slayer””Gold & Platinum - The Big 4 Live from Sofia, Bulgaria””Exclusive! Interview With Slayer Guitarist Kerry King””2008-02-23: Wiltern, Los Angeles, CA, USA””Slayer's Kerry King To Perform With Megadeth Tonight! - Oct. 21, 2010”originalet”Dave Lombardo - Biography”Slayer Case DismissedArkiveradUltimate Classic Rock: Slayer guitarist Jeff Hanneman dead at 49.”Slayer: "We could never do any thing like Some Kind Of Monster..."””Cannibal Corpse'S Pat O'Brien Will Step In As Slayer'S Guest Guitarist | The Official Slayer Site”originalet”Slayer Wins 'Best Metal' Grammy Award””Slayer Guitarist Jeff Hanneman Dies””Kerrang! Awards 2006 Blog: Kerrang! Hall Of Fame””Kerrang! Awards 2013: Kerrang! Legend”originalet”Metallica, Slayer, Iron Maien Among Winners At Metal Hammer Awards””Metal Hammer Golden Gods Awards””Bullet For My Valentine Booed At Metal Hammer Golden Gods Awards””Metal Storm Awards 2006””Metal Storm Awards 2015””Slayer's Concert History””Slayer - Relationships””Slayer - Releases”Slayers officiella webbplatsSlayer på MusicBrainzOfficiell webbplatsSlayerSlayerr1373445760000 0001 1540 47353068615-5086262726cb13906545x(data)6033143kn20030215029