Type Theory and Principia Mathematica Part IV "Relation Arithmetic"
relational databases are among the highest value, most researched applications of computer science
  


James, what do relational databases have to do with the question? And why have you tagged this q with 'relational-algebra'? It seems to me entirely gratuitous.

Just because databases are 'relational' does not mean they have much to do with whatever Russell meant by 'relation-arithmetic'.

Relational database theory sticks to simple set theory and FOPL. Precisely because it wants to avoid getting into higher-order complications (and type theory).

Similarly just because historically Russell's theory of types kicked off an area of research, does not mean that everything these days to do with type theory must therefore derive from Russell, or that his later musings would necessarily help.


  Is Russell's theory of relation-arithmetic still largely unnoticed even in modern computer science based on type theory, despite the critical role computers play in bringing mathematical understanding of the empirical world into practical use? If so, why?


I'd say yes, entirely unnoticed.

Again what relevance does the "critical role computers play" have wrt Russell?

On looking at a few of the standard early works in programming language type theory, I see no citations of Russell: Landin 1965 on the semantics for ALGOL; Strachey 1967; Reynolds 1983.

The Reynolds paper has the word "relations" in the abstract. And cites a paper Morris 1973 'Types are not Sets'. And mentions [Dana] "Scott's discovery of how to construct sufficiently rich universes without encountering Russell's paradox".

Modern type theory derives mostly from typing models for Lambda Calculus; of which Russell had no inkling. That could be why.

BTW your opening link to the answer on type theory, which mentions "Russell's paradox occasionally shows up" then points to some results in Haskell I think is again drawing a very long bow. Also those results back in 2010 are for some early developments of then-new type-level features. I'd classify them as bugs. They rely essentially on Impredicativity about which the compiler's user guide says "GHC has extremely flaky support for impredicative polymorphism, ..."; indeed I think the feature is to be blocked as a 'very hard problem to get right'.