Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Why can't (Set -> Set) have type Set?

In Agda, the type of a forall is determined in such a way that the following all have type Set1 (where Set1 is the type of Set and A has type Set):

Set → A
A → Set
Set → Set

However, the following has type Set:

A → A

I understand that if Set had type Set, there would be contradictions, but I'm failing to see how, if any of the three terms above had type Set, we would have contradictions. Can those be used to prove False? Can they be used to show that Set : Set?

like image 218
Brandon Pickering Avatar asked Sep 22 '12 22:09

Brandon Pickering


People also ask

What type of set is denoted by {} or O?

The set, which has no elements, is also called a null set or void set. It is denoted by {}. Below are the two examples of the empty set. Example of empty set: Let set A = {a: a is the number of students studying in Class 6th and Class 7th}.

Can set have different data types?

A set can be of any data type: a string , int , or the boolean data types.

What does ⊕ mean in set?

The ⊕ symbol is normally used to denote "exclusive or" in (boolean) logic. More usually the △ symbol is used to distinguish between set-operation and logic-operation. A⊕B = A△B= {x:(x∈A)⊕(x∈B)}=(A∩B∁)∪(A∁∩B)= {x:((x∈A)∧(x∉B))∨((x∉A)∧(x∈B))}= (A∪B)∩(A∩B)∁= {x:((x∈A)∨(x∈B))∧¬((x∈A)∧(x∈B))} Cite.


2 Answers

It is clear that Set : Set would cause a contradiction, such as Russell's paradox.

Now consider () -> Set where () is a unit type. This is clearly isomorphic to Set. So if () -> Set : Set then also Set : Set. In fact, if for any inhabited A we had A -> Set : Set then we could wrap Set into A -> Set using a constant function:

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

and get the value whenever needed as

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

So we could reconstruct Russell's paradox just as if we had Set : Set.


The same applies for Set -> Set, we could wrap Set into Set -> Set:

data Void : Set where

unwrap2 : (Set -> Set) -> Set
unwrap2 f = f Void

wrap2 : Set -> (Set -> Set)
wrap2 v = \_ -> v

Here we could use any type of Set instead of Void.


I'm not sure how to do something similar with Set -> A, but intuitively this seems to be even more problematic type than the other ones, maybe someone else will know.

like image 173
Petr Avatar answered Oct 16 '22 05:10

Petr


I think the best way to understand this is to consider what these things are like as set-theoretic sets, as opposed to as Agda Set. suppose you have A = {a,b,c}. An example of a function f : A → A is a set of pairs, let's say f = { (a,a) , (b,b) , (c,c) } that satisfies some properties that don't matter for this discussion. That is to say, f's elements are the same sort of thing that A's elements are -- they're just values, or pairs of values, nothing too "big".

Now consider the a function F : A → Set. It too is a set of pairs, but its pairs look different: F = { (a,A) , (b,Nat) , (c,Bool) } lets say. The first element of each pair is just an element of A, so it's pretty simple, but the second element of each pair is a Set! That is, the second element is itself a "big" sort of thing. So A → Set couldn't possibly be set, because if it were, then we should be able to have some G : A → Set that looks like G = { (a,G) , ... }. As soon as we can have this, we can get Russell's paradox. So we say A → Set : Set1 instead.

This also addresses the issue of whether or not Set → A should also be in Set1 instead of Set, because the functions in Set → A are just like the functions in A → Set, except that the As are on the right, and the Sets are on the left, of the pairs.

like image 7
augur Avatar answered Oct 16 '22 06:10

augur