Comments to Wikipedia Type theory article
A parallel, lively thread prompted some commentary on the Type theory article from wikipedia.
Between 1902 and 1908 Bertrand Russell proposed various "theories of type" in response to his discovery that Gottlob Frege's version of naive set theory was afflicted with Russell's paradox...
One may argue that this motivation is irrelevant in the context of computer programming field, but not so fast, please. For example, did you know that the collection of all finite sets is not a set but proper class?
...creating a hierarchy of types, then assigning each concrete mathematical (and possibly other) entity to a type. Entities of a given type are built exclusively from entities of those types that are lower in their hierarchy, thus preventing an entity from being assigned to itself.
Therefore, types are not just about subsets specified via properties (naive unrestricted comprehension), but they are organized into a hierarchy. Again, if we associate types with objects formally via the binary formal concept relation, then we'll obtain a concept lattice of types.
The common usage of "type theory" is when those types are used with a term rewrite system.
Terms... That is an extensive subject by itself covered in Universal Algebra. Speaking of algebras, it seems that the most useful primitive types (the ones that are located at the bottom of type hierarchy) are based upon familiar algebras...
Typing usually takes place in some context or environment denoted by the symbol . Often, an environment is a list of pairs . This pair is sometimes called an assignment. The context completes the above opposition. Together they form a judgement denoted .
How this list of pairs is not the aforementioned binary formal concept relation?
Quote from Vadim on November 11, 2021, 4:18 pmdid you know that the collection of all finite sets is not a set but proper class?
Please correct me if I am wrong, but does that not depend on which set theory you are using? For example in NFU,
Axiom of the Universal Set. { x | x = x }, also called V, exists.
Holmes calls V, "the universe, the set which contains everything."
Quote from Paul Vernon on November 11, 2021, 4:35 pmQuote from Vadim on November 11, 2021, 4:18 pmdid you know that the collection of all finite sets is not a set but proper class?
Please correct me if I am wrong, but does that not depend on which set theory you are using? For example in NFU,
Axiom of the Universal Set. { x | x = x }, also called V, exists.
Holmes calls V, "the universe, the set which contains everything."
p. 17-18:
If the reader feels that arbitrary collections of objects of our theory must
exist in some sense, he can understand the sentence “the set {x | x has
property φ} does not exist” as meaning not that there is no collection of
all objects x of our theory such that φ, but that this collection cannot be
regarded as a set in our theory; such collections which are not sets will
sometimes be discussed (we call them “proper classes”).
In other words NFU admits that the axiom of unrestricted comprehension is a no go as well. Then, the question is if
{ x | x is finite }
is legitimate (“stratified”) property... And the Axiom of Singletons hints that perhaps not.
Quote from Vadim on November 11, 2021, 4:18 pmA parallel, lively thread prompted some commentary on the Type theory article from wikipedia.
Between 1902 and 1908 Bertrand Russell proposed various "theories of type" in response to his discovery that Gottlob Frege's version of naive set theory was afflicted with Russell's paradox...
One may argue that this motivation is irrelevant in the context of computer programming field,
You'll need to be very careful whether you're talking about 'type' in a programming language -- and which language's semantics -- vs type in an abstract math sense.
but not so fast, please. For example, did you know that the collection of all finite sets is not a set but proper class?
Is there any programming language that distinguishes type vs class in that sense? Lots of languages have things called 'class'. The meaning of 'class' varies widely between languages, such that I avoid using it here unqualified. I'm pretty sure none of those meanings bear any connection with the math sense. Does anything in a programming language need to represent classes in the sense you're talking about or manipulate them?
BTW many of the types in programming language have an infinite number of elements. Arbitrary-precision Integers; relations with an arbitrary number of tuples; other data structures such as lists, streams, trees.
...creating a hierarchy of types, then assigning each concrete mathematical (and possibly other) entity to a type. Entities of a given type are built exclusively from entities of those types that are lower in their hierarchy, thus preventing an entity from being assigned to itself.
Therefore, types are not just about subsets specified via properties (naive unrestricted comprehension), but they are organized into a hierarchy.
Are there programming languages that specify types purely by properties? In my experience, you declare a type by construction: itemise the elements of a scalar; list the tags and their components for a discriminated union. Even TTM's type inheritance starts from itemising the elements. Can a TTM type predicate specify something like: 'an element is in this type providing it's not in that type'? I'm pretty sure not, because D&D wouldn't fall into that hole. Think about how hard it is in concrete terms to fall foul of Russells Paradox: with barbers who don't shave themselves or clubs that wouldn't have Groucho as a member, it's pretty easy to amend the rules to avoid paradoxes.
In nominative typing, you declare the hierarchy: values True, False are declared to be type Bool; Bool is (implicitly) declared to be of type-of-type Type -- that is the type of types carrying values. There can be other type-of-types purely for type-level manipulation and overloading. (This system of type-of-types is sometimes called Kinds in the literature.)
Again, if we associate types with objects formally via the binary formal concept relation, then we'll obtain a concept lattice of types.
I think you don't understand the 'hierarchy of types' concept for avoiding Russell's Paradox vs the 'hierarchy of sets of values' in (say) TTM's type inheritance. Addit: the hierarchy is formed by UNIONing the elements, each node is merely a set-of-values (homogenous); whereas Formal Concept hierarchies seem to be about combining attributes/predicates (heterogenous) into something like a Universal Relation -- which has a shady history in relational theory. [end of Addit] If you don't declare type-of-types by predicate (intension) but only by enumeration (extension), you don't run into Russell's Paradox. This is so even if you allow such exotica as poly-Kinded functions.
The common usage of "type theory" is when those types are used with a term rewrite system.
Terms... That is an extensive subject by itself covered in Universal Algebra.
'Terms' in programming languages refer to syntactic elements of program expressions.
Speaking of algebras, it seems that the most useful primitive types (the ones that are located at the bottom of type hierarchy) are based upon familiar algebras...
Typing usually takes place in some context or environment denoted by the symbol . Often, an environment is a list of pairs . This pair is sometimes called an assignment. The context completes the above opposition. Together they form a judgement denoted .
How this list of pairs is not the aforementioned binary formal concept relation?
e is a (sub-) expression from the program source. It's not a 'concept'. τ is the inferred type for that sub-expression, given the declarations in the program source. is the transitive closure of those declarations and the implications from them, and the derivations of the types of the sub-terms within the expression. It's very much tied to the program source and the semantics of the language. No airy-fairy 'formal concepts' at all.
Quote from AntC on November 12, 2021, 5:07 amSpeaking of algebras, it seems that the most useful primitive types (the ones that are located at the bottom of type hierarchy) are based upon familiar algebras...
Typing usually takes place in some context or environment denoted by the symbol . Often, an environment is a list of pairs . This pair is sometimes called an assignment. The context completes the above opposition. Together they form a judgement denoted .
How this list of pairs is not the aforementioned binary formal concept relation?
e is a (sub-) expression from the program source. It's not a 'concept'. τ is the inferred type for that sub-expression, given the declarations in the program source. is the transitive closure of those declarations and the implications from them, and the derivations of the types of the sub-terms within the expression. It's very much tied to the program source and the semantics of the language. No airy-fairy 'formal concepts' at all.
Can we just replace the colon symbol with set membership? After all we are talking about a binary relation in some context , when we abstract away the interpretation (the object e is compatible with type τ).
I didn't realize until today, that there is great deal of similarity between set membership relation as in the Set Theory, and compatibility relation between the two disjoint sets of entities as in FCA. In the NFU book mentioned by Paul there is a lengthy discussion about the curly brackets, as opposed to the concepts from Boolean Algebra which are very intuitive and requite much less explanation. Note how Russells Paradox is avoided in the new setting where there is no omniscient membership relation, but numerous unrelated compatibility relations between pairwise disjoint sets...
Quote from AntC on November 12, 2021, 5:07 amThink about how hard it is in concrete terms to fall foul of Russells Paradox: with barbers who don't shave themselves or clubs that wouldn't have Groucho as a member, it's pretty easy to amend the rules to avoid paradoxes.
Randall has been listening in again .
Quote from Vadim on November 12, 2021, 4:09 pmQuote from AntC on November 12, 2021, 5:07 amSpeaking of algebras, it seems that the most useful primitive types (the ones that are located at the bottom of type hierarchy) are based upon familiar algebras...
Typing usually takes place in some context or environment denoted by the symbol . Often, an environment is a list of pairs . This pair is sometimes called an assignment. The context completes the above opposition. Together they form a judgement denoted .
How this list of pairs is not the aforementioned binary formal concept relation?
e is a (sub-) expression from the program source. It's not a 'concept'. τ is the inferred type for that sub-expression, given the declarations in the program source. is the transitive closure of those declarations and the implications from them, and the derivations of the types of the sub-terms within the expression. It's very much tied to the program source and the semantics of the language. No airy-fairy 'formal concepts' at all.
Can we just replace the colon symbol with set membership?
No. e is an expression, not a value. We haven't evaluated it yet (haven't run the program), so we don't know what value it has. Of course it might have different values in different runs. It might be an infinite calculation (or poorly coded) such that it never returns a result.
Quote from AntC on November 12, 2021, 5:07 amQuote from Vadim on November 11, 2021, 4:18 pm
...creating a hierarchy of types, then assigning each concrete mathematical (and possibly other) entity to a type. Entities of a given type are built exclusively from entities of those types that are lower in their hierarchy, thus preventing an entity from being assigned to itself.
Therefore, types are not just about subsets specified via properties (naive unrestricted comprehension), but they are organized into a hierarchy.
Are there programming languages that specify types purely by properties? In my experience, you declare a type by construction: itemise the elements of a scalar; list the tags and their components for a discriminated union. Even TTM's type inheritance starts from itemising the elements. Can a TTM type predicate specify something like: 'an element is in this type providing it's not in that type'? I'm pretty sure not, because D&D wouldn't fall into that hole.
Ah yep, here you go:
- IM Pre 10 'Specialisation by Constraint' "Let T be a regular proper supertype (see IM Prescription 20), and let T' be an immediate
subtype of T. Then the definition of T' shall specify a specialization constraint SC,
formulated in terms of T, such that a value shall be of type T' if and only if it is of type T and
it satisfies constraint SC."
The constraint SC must be "formulated in terms of T" is rather wooly wording. I think D&D intend it to mean: in terms of a predicate applying to the values (elements) of T. Anyhoo the values (elements) of subtype T' must be a subset. And from other prescriptions, T must be a subset of some root type S; and the values (elements) of each root type must be distinct.
- IM Pre 20 A union type is a type T such that there exists no value that is of type T and not of some
immediate subtype of T.
So a union type can be declared in terms of the names of the immediate subtypes. But we can't declare a type in terms of values being non-members of some other type. So we've avoided Russell's Paradox.
Think about how hard it is in concrete terms to fall foul of Russells Paradox: with barbers who don't shave themselves or clubs that wouldn't have Groucho as a member, it's pretty easy to amend the rules to avoid paradoxes.
Think about how hard it is in concrete terms to fall foul of Russells Paradox: with barbers who don't shave themselves or clubs that wouldn't have Groucho as a member, it's pretty easy to amend the rules to avoid paradoxes.
The 'barbers's paradox' is trivial, as Russell himself pointed out. There is no barber.
Actually, it really is quite a lot harder to run into a paradox than you are suggesting, and there are many ways to avoid it. Relying on construction usually works. Avoiding 'not' is another good idea.
I would be surprised if you could come up with any plausible type definition that caused any difficulty of that kind.