25

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?

Brandon Pickering
  • 315
  • 2
  • 7
  • I suppose this is more math than programming. I take it this should have been posted there instead? – Brandon Pickering Sep 22 '12 at 22:55
  • Yep. mathematics.stackexchange.com – Cole Tobin Sep 23 '12 at 03:16
  • 28
    Wait, why is this off-topic? This is a fairly common question for Agda or Coq, which although they are often used as proof assistants, are perfectly valid programming languages. His syntax even mirrors Agda, and the post has an Agda tag. It seems rather draconian to close the question as not programming when a tag lists a programming language and it's a valid question in that language. – copumpkin Sep 25 '12 at 03:30
  • 24
    This is a perfectly legitimate question about a type in a *programming language* that has a perfectly legitimate and well defined answer. How is it an off topic post? – Edward Kmett Sep 25 '12 at 03:54
  • 26
    "Is this Math or programming?" "Yes." – sclv Sep 25 '12 at 04:23

2 Answers2

18

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.

Petr
  • 62,528
  • 13
  • 153
  • 317
  • 1
    Thanks for the answer, makes sense now. I'm actually pretty sure that `Set -> A : Set` isn't problematic; they just chose to give it a type of `Set1` because it makes more sense. I'm not sure though. – Brandon Pickering Sep 23 '12 at 22:39
  • 2
    @BrandonPickering I'm not so sure. Intuitively, `Set -> Bool` is a powerset of `Set` so it is "even larger" than `Set`. So if `Set -> A : Set` for `A` with at least 2 inhabitants then it seems reasonable that also `Set : Set`. – Petr Sep 24 '12 at 06:24
  • 2
    @PetrPudlák: Allowing `Set -> A` to be in `Set` seems like it would invite [Curry's Paradox](http://en.wikipedia.org/wiki/Curry%27s_Paradox) instead, which is so devious that GHC can be tricked into attempting to inline its entire (infinitely recursive) proof, as [you've discovered yourself](http://codegolf.stackexchange.com/questions/7197/crash-your-favorite-compiler/7198#7198). – C. A. McCann Sep 26 '12 at 13:53
  • 1
    @C.A.McCann I tried that, but so far no success. It's a bit different situation - in Curry's Paradox one wraps the datatype into itself, while here one wraps `Set` into the datatype. – Petr Sep 27 '12 at 20:33
7

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.

augur
  • 341
  • 2
  • 4