Lambda the Ultimate

Well that's an interesting question. In the past I have always typed `Nil` as `List<A>` where `A` is ungrounded. Then if `A` gets unified with another type elsewhere the type of Nil would get updated. However I now realise that would not be compositional, so it might be better to type `Nil` `List<Bottom>`.

I've always seen nil as the value containing no value, such that any non-nil compared to nil will be false. As such, the type of nil is nil-type, which is orthogonal not only to all other types, but also to ⊥, the bottom type.

The downside is that any operation which can validly take or return a nil must involve union types. For example, cons takes arguments of [⊥ | nil] and returns pair, car takes an argument of [pair | nil] and returns [⊥, nil].

I'm probably wrong, though

Consider this: if a value is just another type which have its super-type and sub-types, there should be an ultimate type of all values, a superset of all existing sets. Then isn't Nil a complement to that ultimate type? Further, I might sound a bit crazy, but following this logic, could Nil even exist if it is out of bounds of the existng universe of types?

If our ultimate super-type is everything then Nil should be nothing. But that nothing is out of bounds of our everything, it is everything's complement. Isn't then contradictory to introduce Nil? After all, it does not exist in our everything, otherwise it wouldn't be the everything's complement.

Edit: Nil might be a dirty programmer trick to implement something that doesn't even exist.

Complement could be a function that takes two parameters, a smaller set we want to complement from and a bigger set from which we exclude the smaller set. So if we say `A \ B`, meaning `A` without `B`, we get a complement of `B` regarding to `A`.

Now, let's call our set of everything as `E`. There is no bigger set than `E`, as it is the ultimate embracing set. To reach `Nil`, we could write `E \ E`, without violating common sense. If you think about it, what we get is an empty set that resides inside `E`, the left side of `E \ E` expression.

So, after all, `Nil` might exist in the type universe. It could be an empty set, but its type depends on granulation from which we build that `Nil`. `A \ A` gets us a `Nil` of type `A`, but `B \ B` gets us a `Nil` of type `B`.

In your logic, E \ E is the empty set, but is still a set. It is not nil.

There may be an argument for typed nil, for example "the absence of a number", which could sensibly act as an identity value. But I'm not even certain about that. What should NOT boolean-nil return, for example?

In your logic, E \ E is the empty set, but is still a set. It is not nil.

I was thinking of *every* value as a superset of other values, which are in turn supersets of their own values and so on. By assigning values, those sets are narrowed down to certain values-subsets. In an extreme case, they can be narrowed down to `{}` (meaning `Nil` as their leaf node - from a certain set, you pick zero elements, resulting with an empty set).

What should NOT boolean-nil return, for example?

Neither `True`, Neither `False`, but a set `Boolean`, further narrowed to `{}`. Note that here is remembered complete path to the narrowed value.

But I'm not claiming this is the only possible logic for dealing with 'Nil'. In this logic, every value acts as a set/type for other values. Other logics might include a clear distinction between types and values. I'm still not certain what would `Nil` stand for in the former example.

Edit: It is common that `Nil`, in this or that form, is used for terminating lists in many languages, but are there any other justified examples of using `Nil`?

It's a pretty common occurrence in database applications, the value of "no value". Admittedly, about 99% of programmers can't handle it, and low level handling of nil by database engines is far from consistent, but it's a pretty major usage.

That's pretty much where my feelings about nil, and where it doesn't fit into a type system come from, viz that nil / the type of nil is totally orthogonal to all other values and types, even its own, and from that it follows that the type of nil cannot be rooted in the bottom type. This approach allows us to annotate the (rare) cases where nil is acceptable input / output.

Caging nil is a useful thing to do.

I'd create a new type `Unspecified` and put it within a sum type:

SomeField ⊆ (@Integer ∪ Unspecified)

On the other side, for terminating lists I'd use:

List ⊆ (
  Item ⊆ @Any ×
  Next ⊆ (@List ∪ EndOfList)
)

In both cases, in less expressive languages, we can utilize a null as a special value that indicates "Unspecified" or "EndOfList", but I think it is only about different interpretation of a special value that we don't regularly use, such is null. I think, in such languages, it is completely up to us how would we interpret null.

But if we search for a real example, I think we should look for languages that may interpret `Nil` as their essential piece of expression. Here come those: 0, '', false, {}, ... expressions for values, but I think the very `Nil` analogically may bound not to values, but to types, specifically types that can't contain any values (or, to open a subject, maybe can contain only: 0, '', false, {}, ...)

But these are only my observations, I don't have any references, and I might be terribly wrong about this.

What should NOT boolean-nil return, for example?

Oh, sorry, got confused about the NOT word. If you meant NOT as an operator, I think it should return the same as `integer-nil + integer-nil`. Some error or something maybe?

Or, on the other hand, `False` could be defined as identical to boolean-nil in some interpretation. Then it is easy: `NOT boolean-nil` equals `NOT False` equals `True`. Somehow I like this scenario. Then I think `Boolean` should be defined in a following manner:

Boolean ⊆ (
  True ∪
  False ⊆ {}
)

Ok, because I don't know about this, I'm qualified to comment:

In the bottom is the Any Type. Above it, the None(nil) type. Then above None is the Some and above it everything else.

let's call it the "Big-Bang" type system, because obviously before anything was none in this model (that is also my definition, as somebody that don't know about that, too).

You can get meta-logicall and claim that before the bigbang must obviously exist the something that was the base of the big-bang, but then we can agree we that is too pedantic for practical purposes, and also, this is about types, not the universe...

This sound ok? Because that is exactly how I plan to make my types! Any problem with this?

a data None and its function-counterpart: not. Combine those two and you get the Type Bang.

But we have to set up some rules, otherwise Any gets undefined. I guess we could set up some rules for functions. And then data could be an abstracted relation network depending on its origin, currently None. Maybe then we could substitute None for something else. Maybe for Any? A Type Chrunch then happens?

But this is only about not. I still think we need the other functions to build a data network, if we are going to build it that way. Allthough there could exist other ways to build up a type system, I have a feeling there is something special about None data and "not" function.

(By the way, I too don't consider myself an expert, so I hope others will have patience for a little brainstorming)

This I think is the point I was trying to get to, but not able to explain.

Currently I think quantification is preferable because:

- Subsumption by quantification is symmetrical (it doesn't matter whether an argument is an input or an output).

- Subsumption by subtyping is asymmetrical, and introduces co- and contravariance.