Este ensayo, escrito como complemento de un texto anterior titulado 'Type Theory Weary', cuestiona la necesidad de tratar los tipos como un constructo especial dentro de la informática y la lógica. El autor sostiene que los sistemas de tipos surgieron históricamente para resolver problemas que en su mayoría eran autoprovocados, como la paradoja de Russell o la correspondencia Curry-Howard, que no es más que el reconocimiento de que los sistemas de tipos reintroducían lógica relacional ya existente.
A partir de ahí, el texto argumenta que casi toda la funcionalidad atribuida a los tipos queda subsumida trivialmente por una representación relacional adecuada. La distinción histórica entre tipo y valor se reduce a una cuestión pragmática: el valor se computa en tiempo de ejecución, mientras que el tipo se computa en tiempo de compilación. Si se difumina esa frontera, la representación unificada es preferible.
El autor identifica, no obstante, una función genuinamente propia de los tipos como constructo especial: servir como desambiguador sintáctico del lenguaje. Los tipos permiten reutilizar la misma palabra —por ejemplo, 'length'— con distintos significados según el contexto, funcionando como una forma de compresión del código. Todo lo demás que suele atribuirse a los tipos —corrección, factorización, jerarquías— es, en realidad, lógica relacional ordinaria que no requiere tratamiento diferenciado. El ensayo concluye que conviene abandonar la línea restrictiva entre tipo y valor y trabajar con una representación unificada.
