4 ms·

It's interesting that Wolfram makes a quick foray into computer science to bash type systems. (I think he couldn't be more wrong) "To resolve this, Russell int

It's interesting that Wolfram makes a quick foray into computer science to bash type systems. (I think he couldn't be more wrong) "To resolve this, Russell introduced what is often viewed as his most original contribution to mathematical logic: his theory of types—which in essence tries to distinguish between sets, sets of sets, etc. by considering them to be of different “types”, and then restricts how they can be combined. I must say that I consider types to be something of a hack. And indeed I have always felt that the related idea of “data types” has very much served to hold up the long-term development of programming languages. (Mathematica, for example, gets great flexibility precisely from avoiding the use of types.)"

ionfish 16y ago
It is a strange comment. The type theories used in programming languages, certainly in those based on the λ-cube, descend from simple type theory (via the simply-typed λ-calculus), which Russell discarded in favour of his ramified theory of types. I also wonder why Wolfram, originally a mathematician, doesn't even mention the Curry-Howard correspondence, which seems to me a fairly important result linking mathematics and computation. No one uses ramified type theory these days, at least not that I am aware, although Russell's predicativism lives on in e.g. Feferman's programme [1] (there are some interesting results in reverse mathematics relating to this; see Simpson's book [2]). Anyone missing the background I and the parent comment allude to might want to take a look at Thierry Coquand's article on type theory in the SEP [3]. Coquand is the originator of many ideas in this area, including the calculus of constructions [4] and the proof assistant Coq based on it. [1] http://math.stanford.edu/~feferman/papers/predicativity.pdf http://math.stanford.edu/~feferman/papers/predicativity.pdf [2] http://www.math.psu.edu/simpson/sosoa/ http://www.math.psu.edu/simpson/sosoa/ [3] http://plato.stanford.edu/entries/type-theory/ http://plato.stanford.edu/entries/type-theory/ [4] http://en.wikipedia.org/wiki/Calculus_of_constructions http://en.wikipedia.org/wiki/Calculus_of_constructions
- joelburget 16y ago
  Thanks for a better explanation than I could have written myself. I also like this page as a more basic introduction to type systems: http://blogs.perl.org/users/ovid/2010/08/what-to-know-before-debating-type-systems.html http://blogs.perl.org/users/ovid/2010/08/what-to-know-before...
  - ionfish 16y ago
    From a PL perspective, you can't beat Benjamin Pierce's Types and Programming Languages. http://www.cis.upenn.edu/~bcpierce/tapl/ http://www.cis.upenn.edu/~bcpierce/tapl/
    - joelburget 16y ago
      Agreed.
- xcthulhu 16y ago
  >No one uses ramified type theory these days, at least not that I am aware In the 1920s Frank Ramsey proved that the theory of ramified types + "The Axiom of Reducibility" is equivalent to the theory of simple types: http://en.wikipedia.org/wiki/Type_theory#Simple_theory_of_types http://en.wikipedia.org/wiki/Type_theory#Simple_theory_of_ty... The history I've heard is that ramified types were abandoned after this, since simple type theory is easier and has the same expressive power.
  - ionfish 16y ago
    That's certainly always the way I've heard it, although I did come across an interesting lacuna when I was reading the the SEP article earlier, which is that the effect of the axiom of reducibility was first noticed by Polish logician Leon Chwistek [1]. His article 'The Theory of Constructive Types' was published in 1924, while Ramsey's paper dates from 1926. José Ferreirós in The Princeton Companion to Mathematics mentions his name as well, albeit without much detail. Chwistek seems a fascinating character: like his contemporary Witkacy, he was an artist as well as a logician, and according to the biography of Alfred Tarski by the Fefermans [2], was appointed to a professorship at Lvov in 1930 which Tarski was also in the running for; apparently a letter of recommendation from Russell was the decisive factor (see p. 67 of the aforementioned). Bernard Linsky seems to have written a chapter on Chwistek and type theory in The Golden Age of Polish Philosophy. You can read the first page [3] but I haven't been able to find the entire thing online. [1] http://en.wikipedia.org/wiki/Leon_Chwistek http://en.wikipedia.org/wiki/Leon_Chwistek [2] http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=0521802407 http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=052... [3] http://www.springerlink.com/content/v078l3n714589036/ http://www.springerlink.com/content/v078l3n714589036/
    - xcthulhu 16y ago
      > Bernard Linsky seems to have written a chapter on Chwistek and type theory in The Golden Age of Polish Philosophy. You can read the first page [3] but I haven't been able to find the entire thing online. Try gigapedia.com ;-D

ionfish 16y ago

It is a strange comment. The type theories used in programming languages, certainly in those based on the λ-cube, descend from simple type theory (via the simply-typed λ-calculus), which Russell discarded in favour of his ramified theory of types. I also wonder why Wolfram, originally a mathematician, doesn't even mention the Curry-Howard correspondence, which seems to me a fairly important result linking mathematics and computation. No one uses ramified type theory these days, at least not that I am aware, although Russell's predicativism lives on in e.g. Feferman's programme [1] (there are some interesting results in reverse mathematics relating to this; see Simpson's book [2]). Anyone missing the background I and the parent comment allude to might want to take a look at Thierry Coquand's article on type theory in the SEP [3]. Coquand is the originator of many ideas in this area, including the calculus of constructions [4] and the proof assistant Coq based on it. [1] http://math.stanford.edu/~feferman/papers/predicativity.pdf http://math.stanford.edu/~feferman/papers/predicativity.pdf [2] http://www.math.psu.edu/simpson/sosoa/ http://www.math.psu.edu/simpson/sosoa/ [3] http://plato.stanford.edu/entries/type-theory/ http://plato.stanford.edu/entries/type-theory/ [4] http://en.wikipedia.org/wiki/Calculus_of_constructions http://en.wikipedia.org/wiki/Calculus_of_constructions

joelburget 16y ago
Thanks for a better explanation than I could have written myself. I also like this page as a more basic introduction to type systems: http://blogs.perl.org/users/ovid/2010/08/what-to-know-before-debating-type-systems.html http://blogs.perl.org/users/ovid/2010/08/what-to-know-before...
- ionfish 16y ago
  From a PL perspective, you can't beat Benjamin Pierce's Types and Programming Languages. http://www.cis.upenn.edu/~bcpierce/tapl/ http://www.cis.upenn.edu/~bcpierce/tapl/
  - joelburget 16y ago
    Agreed.
xcthulhu 16y ago
>No one uses ramified type theory these days, at least not that I am aware In the 1920s Frank Ramsey proved that the theory of ramified types + "The Axiom of Reducibility" is equivalent to the theory of simple types: http://en.wikipedia.org/wiki/Type_theory#Simple_theory_of_types http://en.wikipedia.org/wiki/Type_theory#Simple_theory_of_ty... The history I've heard is that ramified types were abandoned after this, since simple type theory is easier and has the same expressive power.
- ionfish 16y ago
  That's certainly always the way I've heard it, although I did come across an interesting lacuna when I was reading the the SEP article earlier, which is that the effect of the axiom of reducibility was first noticed by Polish logician Leon Chwistek [1]. His article 'The Theory of Constructive Types' was published in 1924, while Ramsey's paper dates from 1926. José Ferreirós in The Princeton Companion to Mathematics mentions his name as well, albeit without much detail. Chwistek seems a fascinating character: like his contemporary Witkacy, he was an artist as well as a logician, and according to the biography of Alfred Tarski by the Fefermans [2], was appointed to a professorship at Lvov in 1930 which Tarski was also in the running for; apparently a letter of recommendation from Russell was the decisive factor (see p. 67 of the aforementioned). Bernard Linsky seems to have written a chapter on Chwistek and type theory in The Golden Age of Polish Philosophy. You can read the first page [3] but I haven't been able to find the entire thing online. [1] http://en.wikipedia.org/wiki/Leon_Chwistek http://en.wikipedia.org/wiki/Leon_Chwistek [2] http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=0521802407 http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=052... [3] http://www.springerlink.com/content/v078l3n714589036/ http://www.springerlink.com/content/v078l3n714589036/
  - xcthulhu 16y ago
    > Bernard Linsky seems to have written a chapter on Chwistek and type theory in The Golden Age of Polish Philosophy. You can read the first page [3] but I haven't been able to find the entire thing online. Try gigapedia.com ;-D