**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*. :stuck__out__tongue:

**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 :stuck__out__tongue:.

**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`

.