В Agda тип forall определяется таким образом, что все следующие имеют тип Set1 (где Set1 - тип Set, а A - тип Set):
Set → A
A → Set
Set → Set
Однако следующее имеет тип Set:
A → A
Я понимаю, что если бы Set имел тип Set, возникли бы противоречия, но я не понимаю, как, если бы у любого из трех терминов выше был тип Set, у нас были бы противоречия. Могут ли они использоваться для доказательства лжи? Можно ли их использовать, чтобы показать это Set : Set?
Ясно, что Set : Set вызовет противоречие, например Парадокс Рассела.
Теперь рассмотрим () -> Set, где () - это тип единицы. Это явно изоморфно Set. Итак, если () -> Set : Set, то также Set : Set. Фактически, если бы для любого жилого A у нас было A -> Set : Set, тогда мы могли бы обернуть Set в A -> Set, используя постоянную функцию:
wrap1 : {A : Set} -> Set -> (A -> Set)
wrap1 v = \_ -> v
и получайте значение, когда это необходимо, как
unwrap1 : {A : Set}(anyInhabitant : A) -> (A -> Set) -> Set
unwrap1 anyInhabitant f = f anyInhabitant
Таким образом, мы могли реконструировать парадокс Рассела так же, как если бы у нас было Set : Set.
То же самое касается Set -> Set, мы могли бы обернуть Set в Set -> Set:
data Void : Set where
unwrap2 : (Set -> Set) -> Set
unwrap2 f = f Void
wrap2 : Set -> (Set -> Set)
wrap2 v = \_ -> v
Здесь мы могли бы использовать любой тип Set вместо Void.
Я не уверен, как сделать что-то подобное с Set -> A, но интуитивно кажется, что это даже более проблемный тип, чем другие, возможно, кто-то еще узнает.
Set -> A : Set не проблема; они просто решили присвоить ему тип Set1, потому что это имеет больше смысла. Хотя я не уверен.
- person Brandon Pickering; 24.09.2012
Set -> Bool - это набор мощности Set, поэтому он даже больше, чем Set. Таким образом, если Set -> A : Set для A с минимум 2 жителями, то кажется разумным, что также Set : Set.
- person Petr; 24.09.2012
Set -> A находиться в Set похоже на то, чтобы вместо этого пригласить Парадокс Карри, что настолько коварно, что GHC можно обманом заставить попытаться встроить все его (бесконечно рекурсивное) доказательство, как вы открыли себя.
- person C. A. McCann; 26.09.2012
Set в тип данных.
- person Petr; 28.09.2012
Я думаю, что лучший способ понять это - рассмотреть эти вещи как теоретико-множественные множества, а не как Agda Set. предположим, у вас есть A = {a,b,c}. Примером функции f : A → A является набор пар, скажем f = { (a,a) , (b,b) , (c,c) }, который удовлетворяет некоторым свойствам, которые не имеют значения для этого обсуждения. Другими словами, элементы f - это то же самое, что и элементы A - это просто значения или пары значений, ничего слишком "большого".
Теперь рассмотрим функцию F : A → Set. Это тоже набор пар, но выглядят его пары иначе: F = { (a,A) , (b,Nat) , (c,Bool) } так. Первый элемент каждой пары - это просто элемент A, поэтому это довольно просто, но вторым элементом каждой пары является Set! То есть второй элемент сам по себе является «большим». Таким образом, A → Set не может быть установлен, потому что, если бы это было так, то у нас могло бы быть несколько G : A → Set, которые выглядят как G = { (a,G) , ... }. Как только мы получим это, мы сможем получить парадокс Рассела. Поэтому вместо этого мы говорим A → Set : Set1.
Это также решает вопрос о том, должен ли Set → A также быть в Set1 вместо Set, потому что функции в Set → A такие же, как функции в A → Set, за исключением того, что As справа, а Sets слева, пары.
