13
$\begingroup$

I recently realized that there is some sort of relation between Russellian type theory and type systems, as found e.g. in Haskell. Actually, some of the notation for types in Haskell seems to have precursors in type theory. But, IMHO, Russell motivation in 1908 was to avoid Russell's paradox, and I am not sure how that is related to type systems in computer science.

Is Russell's paradox in one form or another something that we would have to worry about, for example, if we didn't have a good type system in a given language?

Improve this question
$\endgroup$

3 Answers 3

Reset to default
9
$\begingroup$

``Type theory" in the sense of programming languages and in the sense of Russell are closely related. In fact, the modern field of dependent type theory aims to provide a constructive foundations for mathematics. Unlike set theory, most research in type theory based math is done in proof assistants like Coq, NuPRL, or Agda. As such, proofs done in these systems are not only "formalizable" but actually fully formal and machine checked. Using tactics and other proof automation techniques we try to make proving with these systems "high level" and thus resemble informal mathematics, but because everything is checked we have much better guarantees on correctness.

See here

Types in ordinary programming languages tend to be more limited, but the meta theory is the same.

Something similar to Russell's paradox is a major issue in dependent type theory. In particular, having

Type : Type

usually leads to contradiction. Coq and similar work by nesting universes

Type_0 : Type_1

but in Coq by default these numbers are implicit as they normally don't matter for the programmer.

In some systems (Agda, Idris), the type in type rule is enabled via a compile flag. It makes the logics inconsistent, but often makes exploratory programming/proving easier.

Even in more mainstream languages, Russell's paradox occasionally shows up. For example, in Haskell, an encoding of Russell's paradox combining impredicativity and open type case is possible, allowing one to build divergent terms with out recursion even at the type level. Haskell is ``inconsistent" (when interpret as a logic in the usual way) since it supports both type and value level recursion, not to mention exceptions. None the less, this result is rather interesting.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks for your detailed answer - as far as proof goes, there are still no tools in sight to prove the correctness of programs in imperative languages like C++ or Java, right? I would love to put my hands on one of these... I realize this is a complete tangent. I know about Coq and Agda, but they didn't seem to be the right tools to prove correctness of programs written in C++ or Java. $\endgroup$
    – Frank
    Commented Aug 15, 2013 at 3:45
  • 3
    $\begingroup$ there are some tools. A few for C, many for Java, and tons for Ada. See for example: Why (Java, C, Ada), Krakatoa (Java), or SPARK (Ada subset with very good tooling). For C++ though, not so much. You also may be interested in YNot (Coq DSL). $\endgroup$
    – Philip JF
    Commented Aug 15, 2013 at 4:02
3
$\begingroup$

You're right about Russell's motivation. His paradox plagues all theories of sets that admit unrestricted comprehension axioms to the effect that: any propositional function determines a set, namely that of all those entities that satisfy the function. Among theories of or based on sets that did have that flaw were Cantor's naive set theory and Frege's system of Grundgesetze (specifically: axiom 5).

Since types are considered to be special kinds of sets, if care is not taken, a similar paradox can creep into a type system.That being said, I'm not aware of any type systems that have suffered such a fate. I can only recall Church's early attempts at formulating lambda calculus in the 30s, which turned out to be inconsistent (Kleene-Rosser Paradox), but that one was neither due to types nor was related to Russell's paradox.

Update: See Philip's response for an actual answer to your question.

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ Thanks for your answer. There are probably alternatives to types-a-la-Russell to avoid Russell paradox. Would any of these alternative solutions have anything interesting to contribute to computer languages? Mundane types are very useful to clearly specify contracts between parts of the code, and even before that, to give semantics to programs at all. Would there be other semantics that could be obtained with something else than types? (I have NO idea what that would be :-) $\endgroup$
    – Frank
    Commented Aug 15, 2013 at 3:48
  • 1
    $\begingroup$ Yes, lots of alternatives (Quine's NF, ZFC, etc), but I can't see any direct connections between the foundational crisis and programming languages. If you consider Martin Lof's type theory as a programming language, there might be some connection there reaching back to intuitionism. As regards the semantics of programming languages, there are some basic languages like PDL (Propositional Dynamic Logic) which have Kripke (or possible worlds) semantics. But types seem to me so fundamental that they might just be behind the scenes :) $\endgroup$
    – Hunan Rostomyan
    Commented Aug 15, 2013 at 4:28
  • 1
    $\begingroup$ But types are kind of a bummer: you want and need them, but you'd love to not have to specify them (hence, IMHO, why we have type inference systems in languages like Haskell or Ocaml (I love those languages)). At the other end of the spectrum, Python feels very intuitive and it is pleasant (and efficient in terms of coding time) to not have to worry too much about types in that language. Maybe type inference is the best of both world - but that's the engineer talking. I was just daydreaming that maths could contribute another significant concept (like types) to computer science :-) $\endgroup$
    – Frank
    Commented Aug 15, 2013 at 4:38
  • 1
    $\begingroup$ @Frank Every time I use a language without static types (mostly Ruby) I hate the experience, because I hate avoidable runtime errors. So, that seems to be a matter of taste mostly. I agree that powerful type inference can give you the best of both worlds. Which is, probably, why I like Scala so much. $\endgroup$
    – Raphael
    Commented Aug 15, 2013 at 10:19
  • $\begingroup$ I am not convinced that not having types "automatically" leads to runtime errors, as you seem to imply :-) I never had a problem in Python. $\endgroup$
    – Frank
    Commented Aug 15, 2013 at 14:37
3
$\begingroup$

Since you mention Python the question is not purely type-theoretic. So I try to give a broader perspective on types. Types are different things to different people. I've collected at least 5 distinct (but related) notions of types:

  1. Type systems are logical systems and set theories.

  2. A type system associates a type with each computed value. By examining the flow of these values, a type system attempts to prove or ensure that no type errors can occur.

  3. Type is a classification identifying one of various types of data, such as real-valued, integer or Boolean, that determines the possible values for that type; the operations that can be done on values of that type; the meaning of the data; and the way values of that type can be stored

  4. Abstract data types allow for data abstraction in high level languages. ADTs are often implemented as modules: the module's interface declares procedures that correspond to the ADT operations. This information hiding strategy allows the implementation of the module to be changed without disturbing the client programs.

  5. Programming language implementations use types of values to choose the storage the values need and algorithms for operations on the values.

The quotes are from Wikipedia, but I can provide better references should a need arise.

Types-1 arose from Russel's work, but today they are not merely protect from paradoxes: the typed language of homotopy type theory is a new way to encode mathematics in a formal, machine-understandable language, and a new way for humans to understand foundations of mathematics. (The "old" way is encoding using an axiomatic set theory).

Types 2-5 arose in programming from several different needs: to avoid bugs, to classify data software designers and programmers work with, to design large systems and to implement programming languages efficiently respectively.

Type systems in C/C++, Ada, Java, Python did not arose out of Russel's work or a desire to avoid bugs. They arose out of needs to describe different kinds of data out there (e.g. "last name is a character string and not a number"), modularize software design and to choose low-level representations for data optimally. These languages have no types-1 or types-2. Java ensures relative safety from bugs not by means of proving program correctness using type system, but by a careful design of language (no pointer arithmetic) and runtime system (virtual machine, bytecode verification). Type system in Java is neither a logical system nor a set theory.

However, type system in Agda programming language is a modern variant of Russel's type system (based on later work or Per Martin-Lof and other mathematicians). The type system in Agda is designed to express mathematical properties of program and proofs of those properties, it is a logical system and a set theory.

There are no black-white distinction here: many languages fit in between. For example, type system of Haskell language has roots in Russel's work, can be viewed as a simplifed Agda's system, but from mathematical standpoint, it's inconsistent (self-contradictory) if viewed as a logical system or a set theory.

However, as a theoretical vehicle to protect Haskell programs from bugs, it works pretty well. You even can use types to encode certain properties and their proofs, but not all properties can be encoded, and the programmer can still violate the proved properties if he uses discouraged dirty hacks.

Type system of Scala is even further from Russel's work and Agda's perfect proof language, but still has roots in Russel's work.

As for proving properties of industrial languages whose type systems were not designed for that, there are many approaches and systems.

For interesting but different approaches, see Coq and Microsoft Boogie research project. Coq relies on type theory to generate imperative programs from Coq programs. Boogie relies on annotation of imperative programs with properties and proving those properties with Z3 theorem prover using a completely different approach than Coq.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.