types - school - ¿Por qué(Set-> Set) no puede tener el tipo Set?

steam runescape

Question

En Agda, el tipo de forall se determina de tal manera que todos los siguientes tienen el tipo Set1 (donde Set1 es el tipo de Set y A tiene el tipo Set ):

Set → A
A → Set
Set → Set

Sin embargo, lo siguiente tiene tipo Set :

A → A

Entiendo que si Set tuviera el tipo Set , habría contradicciones, pero no veo cómo, si alguno de los tres términos anteriores tuviera el tipo Set , tendríamos contradicciones. ¿Se pueden usar para probar lo falso? ¿Se pueden usar para mostrar ese Set : Set ?

Answer 1

Creo que la mejor manera de entender esto es considerar cómo son estas cosas como conjuntos teóricos de conjuntos, a diferencia de Set Agda. supongamos que tienes A = {a,b,c} . Un ejemplo de una función f : A → A es un conjunto de pares, digamos f = { (a,a) , (b,b) , (c,c) } que satisface algunas propiedades que no importan para esto discusión. Es decir, los elementos de f son el mismo tipo de cosas que los elementos de A: son solo valores, o pares de valores, nada demasiado "grande".

Ahora considere la función a F : A → Set . También es un conjunto de pares, pero sus pares se ven diferentes: F = { (a,A) , (b,Nat) , (c,Bool) } digamos. El primer elemento de cada par es solo un elemento de A , así que es bastante simple, ¡pero el segundo elemento de cada par es un Set ! Es decir, el segundo elemento es en sí mismo un tipo de cosa "grande". Por lo tanto, es posible que A → Set no se pueda configurar, porque si lo fuera, entonces deberíamos poder tener algo de G : A → Set que se parece a G = { (a,G) , ... } . Tan pronto como podamos tener esto, podemos obtener la paradoja de Russell. Así que decimos A → Set : Set1 lugar.

Esto también aborda la cuestión de si Set → A también debe estar en Set1 en lugar de Set , porque las funciones en Set → A son como las funciones en A → Set , excepto que los A s están a la derecha, y Set s están a la izquierda, de los pares.

Answer 2

Está claro que Set : Set causaría una contradicción, como la paradoja de Russell .

Ahora considere () -> Set donde () es un tipo de unidad . Esto es claramente isomorfo para Set . Así que si () -> Set : Set entonces Set : Set . De hecho, si para cualquier A habitada teníamos A -> Set : Set entonces podríamos ajustar Set en A -> Set usando una función constante:

wrap1 : {A : Set} -> Set -> (A -> Set)
wrap1 v = /_ -> v

y obtener el valor cuando sea necesario como

unwrap1 : {A : Set}(anyInhabitant : A) -> (A -> Set) -> Set
unwrap1 anyInhabitant f = f anyInhabitant

Así podríamos reconstruir la paradoja de Russell como si tuviéramos Set : Set .

Lo mismo se aplica para Set -> Set , podríamos ajustar Set en Set -> Set :

data Void : Set where
unwrap2 : (Set -> Set) -> Set
unwrap2 f = f Void
wrap2 : Set -> (Set -> Set)
wrap2 v = /_ -> v

Aquí podríamos usar cualquier tipo de Set lugar de Void .

No estoy seguro de cómo hacer algo similar con Set -> A , pero intuitivamente esto parece ser un tipo aún más problemático que los otros, tal vez alguien más lo sepa.