# Comments to Wikipedia Type theory article

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, but not so fast, please. For example, did you know that the collection of all

finitesets 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

contextorenvironmentdenoted by the symbol . Often, an environment is a list of pairs . This pair is sometimes called anassignment. The context completes the above opposition. Together they form ajudgementdenoted .How this list of pairs is not the aforementioned binary formal concept relation?

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 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

finitesets 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 Vadim on November 11, 2021, 4:18 pmdid you know that the collection of all

finitesets 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 Vadim on November 11, 2021, 5:06 pmQuote 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

finitesets 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 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

finitesets is not a set but proper class?

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 Singleton*s hints that perhaps not.

Quote from AntC on November 12, 2021, 5:07 amQuote 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

finitesets 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 aTTMtype 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`Kind`

s 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`UNION`

ing 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

contextorenvironmentdenoted by the symbol . Often, an environment is a list of pairs . This pair is sometimes called anassignment. The context completes the above opposition. Together they form ajudgementdenoted .How this list of pairs is not the aforementioned binary formal concept relation?

is a (sub-) expression from the program source. It's not a 'concept'.eis 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 Vadim on November 11, 2021, 4:18 pmA parallel, lively thread prompted some commentary on the Type theory article from wikipedia.

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

finitesets 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.

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 `Kind`

s 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 `UNION`

ing 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...

contextorenvironmentdenoted by the symbol . Often, an environment is a list of pairs . This pair is sometimes called anassignment. The context completes the above opposition. Together they form ajudgementdenoted .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 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...

contextorenvironmentdenoted by the symbol . Often, an environment is a list of pairs . This pair is sometimes called anassignment. The context completes the above opposition. Together they form ajudgementdenoted .How this list of pairs is not the aforementioned binary formal concept relation?

is a (sub-) expression from the program source. It's not a 'concept'.eis 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

is compatible with typee).τ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 amcontextorenvironmentdenoted by the symbol . Often, an environment is a list of pairs . This pair is sometimes called anassignment. The context completes the above opposition. Together they form ajudgementdenoted .How this list of pairs is not the aforementioned binary formal concept relation?

is a (sub-) expression from the program source. It's not a 'concept'.eτ

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, 8:32 pmQuote 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 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 AntC on November 12, 2021, 8:37 pmQuote from Vadim on November 12, 2021, 4:09 pmQuote from AntC on November 12, 2021, 5:07 amcontextorenvironmentdenoted by the symbol . Often, an environment is a list of pairs . This pair is sometimes called anassignment. The context completes the above opposition. Together they form ajudgementdenoted .How this list of pairs is not the aforementioned binary formal concept relation?

is a (sub-) expression from the program source. It's not a 'concept'.eτCan we just replace the colon symbol with set membership?

No.

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.e

Quote from Vadim on November 12, 2021, 4:09 pmQuote from AntC on November 12, 2021, 5:07 amcontextorenvironmentdenoted by the symbol . Often, an environment is a list of pairs . This pair is sometimes called anassignment. The context completes the above opposition. Together they form ajudgementdenoted .How this list of pairs is not the aforementioned binary formal concept relation?

is a (sub-) expression from the program source. It's not a 'concept'.eτ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 13, 2021, 12:53 amQuote from AntC on November 12, 2021, 5:07 amQuote from Vadim on November 11, 2021, 4:18 pm

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 aTTMtype 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
Tbe a regular proper supertype (see IM Prescription 20), and letT'be an immediate

subtype ofT. Then the definition ofT'shall specify a specialization constraintSC,

formulated in terms ofT, such that a value shall be of typeT'if and only if it is of typeTand

it satisfies constraintSC."The constraint

SCmust be "formulated in terms ofT" is rather wooly wording. I think D&D intend it to mean: in terms of a predicate applying to the values (elements) ofT. Anyhoo the values (elements) of subtypeT' must be a subset. And from other prescriptions,Tmust be a subset of some root typeS; and the values (elements) of each root type must be distinct.

- IM Pre 20 A
union typeis a typeTsuch that there exists no value that is of typeTand not of some

immediate subtype ofT.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.

Quote from AntC on November 12, 2021, 5:07 amQuote from Vadim on November 11, 2021, 4:18 pm

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 aTTMtype 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.

Quote from dandl on November 13, 2021, 1:38 amThe '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.

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.