A: An interesting thought. Any is actually a final object in `\mathfrak{Scal}` because there are arrows from every type to Any, all identities...
E: But arrows won't be unique! Take (a: Int) => (a + 1 : Any) and (a: Int) => (a - 1 : Any), for instance.
A: No, they are unique, because you can't tell them apart. Tell me, how would you distinguish f, g : Int => Any?
E: I will call f(x).asInstanceOf[Int]?
A: But that implies that the `\top` type must be non-parametric.
E: I see.
A: In a sense, there is only one value of type Any, and it is any value. :stuckouttongue:
E: Right, I follow. Evil.
Π: "No, they are unique, because you can’t tell them apart." - this makes no sense.
A: Π, what can you observe about a : Any?
Π: Anything.
A: No, nothing, because it could be anything. Imagine I give you data Foo = forall a. Foo a, what can you do with it?
A: There are no outgoing arrows from Any in `\mathfrak{Scal}`, except the ones going back to Any. So it's the terminal object, and isomorphic to Unit.
E: There is, observably, a single arrow. Unless you're violating the principle of equivalence.
Π: Right. And you have uniqueness of the object, not of the arrows.
A: Why? Arrows are also unique.
Π: The definition of a terminal object is that for each object in `\mathfrak{Scal}`, you have a unique arrow to Any / Unit.
E: You can write a lot of code that represents a single arrow. Different code, same arrow.
A: They are unique up to the things you can observe. How can you tell that i => i + 1 : Int => Any is different from i => i + 2 : Int => Any? It goes back to the definition of `\mathfrak{Scal}`. Do you distinguish between different arrows that have no difference in observable behavior? Step 1: define equality on functions.
Π: That's a different argument though. That's arguing equivalence of programs, i'm saying the definition means somehting different than the statement you gave
E: They aren't different arrows. That is the problem. There is actually just one.
Π: Why aren't there different arrows?
E: Because what it means to be a distinct arrow is our choice. () => 1 + 1 : () => Int is the same arrow as () => 2 : () => Int.
Π: You don't need equality, you just needon to show isomorphism is a contradiction.
A: Please do :stuckouttongue:.
E: The only problem here is a wording problem. That's it, we are talking about two different kinds of arrows. Referenced with the same word. One kind of arrows is "Scala functions equivalent up to semantics". The other one is "scala functions equivalent up to syntax".
Π: Sure. From semantics, it's the same old halting problem
E: I don't care about the halting problem here doesn't matter, let's say they're all terminating arrows and we have an oracle, that Oracle is E. We're just talking about the usual loose "Properties I can observe". In terms of "things you can observe" all Scala functions into Any are equivalent
Π: Sure.
E: Because all Any values are equivalent. Making it a terminal object. And making Unit isomorphic to Any because both have the same observable properties, i.e. none.
Π: Yes. Well, yes and no. The stretch is calling it a terminal object, because with Unit it's easy to prove terminality. forall a. a -> (). But 2: Any and () : Any are semantically different.
A: They are the same.
Π: Under what relation.
A: Observable properties.
Π: Any modulo observability. Sure. If nothing can be observed about Any it may well be () but i'm not sure that satisfies the terminality condition.
E: How about this. I have an isomorphism, () => () and (_: Any) => (). That's a unique isomorphism if there is a unique value of type Any.
Π: I have seen literature that describes a `\top` as being not necessarily terminal, but simply as supremum, a maximal element in the type lattice.
E: Hmmm, that would be an interesting read. It's a supremum with regard to the subtyping category, not the category of functions.
Π: Sure.
A: `\top` is a terminal object in the subtyping category, as well as a supremum of the subtyping lattice.
Π: I am willing to say yes to Any and observability. That makes sense. In the same way Unit makes sense. But there can be only one terminal object per category up to unique isomorphism.
E: Which we got!
Π: But also, then same with Nothing.
E: How so?
Π: What can you say about forall a. a -> Nothing?
E: You can observe any property you want about Nothing. The arrow is unique.
A: There is no forall a. a -> Nothing for some types, e.g. Unit -> Nothing is uninhabited.
Π: Oh?
E: Nothing isn't a terminal. No introductions.
Π: Ah good point. But then Nothing -> Any?
E: Nothing -> Any had better exist. Money for nothing, etc.
A: id : Nothing -> Any.