Why types all the way up but not all the way down?

Stream: new members

[Mr Proof]

def A:= Type 4
def B:A := Type 3
def C:B := Type 2
def D:C := Type 1
def E:D := Type
def F:E := Nat
def G:F := Nat.zero
variable(H:G) /-not work-/

In Lean everything has a type but everything can BE a type.

Out of interest I was wondering would it really break things if everything was allowed to be a type? i.e. instead of having an infinite tower of types upwards you have an infinite tower downwards. In C++ for example, every class can be inherited from. There is no restriction there. While in Lean for types there is a restriction that some things can't be the type of something else.

As an made up example supposed you defined the definition of an electron in Lean which is not a Type but which has type Particle. But then you invent supersymmetry. Well now there are two types of electrons. But since electron is not a type this means you have to redefine everything.

So I was just wondering if there was a theoretical reason for this. Or it's just how it is?

[Kyle Miller]

The inheritance relation in C++ inheritance isn't the has-type relation though. For example, if C and D are classes and D inherits from C, you wouldn't say that D has type C, but just that D inherits from C. Then, if x is an object that has type D, it can be cast to have type C (so in some sense it also has type C), but that's something about objects, not classes.

Just like in Lean, in C++ there's no such thing as something of type x when x is an object, right?

[Kyle Miller]

It's definitely confusing that we use "is a" for both relations.

[Mr Proof]

But you can do C++ without objects at all (more-or-less) just by using singleton classes and static member functions and templates. Then if you have no objects, everything is a class.

#include <iostream>

class Animal{
    public:
    static void MakeSound(){ printf("General animal sound");}
};

class Dog:Animal{
    public:
    static void MakeSound(){ printf("Woof! ");}
};
template<typename T>
void DoSomething(){
     T::MakeSound();
}

int main() {

    Dog::MakeSound();

    //passing a class like you would pass an object
    DoSomething<Dog>();

    return 0;
}

Here I might use the language that Dog "a type of " Animal. (Maybe not with the exact words Dog hasType Animal.

[Mitchell Lee]

What would it mean for something to have the type Nat.zero? That doesn't make sense to me.

[Mr Proof]

I can make an artificial example if you like:

Imagine Gaussian Integers. It is perfectly possible to define them in such a way that x+iy has a "type" of the the natural number x for all y. e.g. 3+4i would have type Nat.3 and so would 3+72i. Therefor every Gaussian integer of the form 0+xi would have type Nat.zero.

This is of course a very silly example. But goes to show you can make sense of it. (Well maybe??? )

[Mitchell Lee]

If I wanted to say that the real part of z is 3, I would write z.re = 3, not z : 3. It's not clear from the notation z : 3 that the statement z : 3 has anything to do with the real part of z. Also, the statement that the real part of z is 3 should be a proposition, not a type judgment.

[Shanghe Chen]

Maybe the setup for "everything term has a type whereas some term is not a type" is for being consistent with the mathematical intuition. But using inductive families one can do things like

inductive TermAsType {α : Type u} : α -> Type u where
| term : (a : α) -> TermAsType a

[Shanghe Chen]

Then TermAsType.term 3 has type TermAsType 3

[Mitchell Lee]

What's the point of doing that, though?

[Shanghe Chen]

I don’t know if there’s any real case for this too hhhh… I asked this before too https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/term.20of.20a.20type.20cannot.20be.20a.20type.3F

[Mr Proof]

I thought of another example.

You could define both +3 and -3 as of type Nat.3 since they are both "types" of 3's. (yeah, no-one would actually do this probably as it would be confusing!)

There's not much point to that, it would only become useful when instead of 3's you have some much more complicated object that you realise actually there's more than one instance of.

[Mitchell Lee]

The type of -3 is Int. (This is written -3 : Int.) The type of -3 is not 3. It can't be both.

[Mr Proof]

Yep. That's where it breaks down i suppose :)

[Mitchell Lee]

If n : 3 could mean n = 3 ∨ n = -3 (which it can't, because the former is a type judgment and the latter is a proposition), then you would end up with theorems like this, where it is impossible to tell what the theorem statement actually means just by looking.

example (n : 3) : n * n = 9 := ...

[Mr Proof]

BTW mainly I was just wondering if making every term a type would break something fundamental. Not really if it was useful. Just as a mathematical curiosity. The TermAsType inductive type seems to suggest it wouldn't break anything but I can't be sure.

[Shanghe Chen]

Making all terms a type maybe get back to set theory as all things are set there. As Kevin said in xena:

Now $\pi$ is a term but it’s not a type. In Lean, $x : \pi$ makes no sense. In set theory, $x\in\pi$ does happen to make sense, but this is a weird coincidence because everything is a set.

[Mr Proof]

:thinking: My intuition says that it would break if terms don't fit in a strict computable hierarchy. If you could show that by letting all terms be types you can create a circular loop of types, or a type that is a type of itself then it would prove it would fail.

[Mitchell Lee]

If you wanted to, you could create your own extension of the type theory that Lean uses. In this extension, 1, 2, 3 are still natural numbers (1 : Nat, 2 : Nat, 3 : Nat). However, now, you can also write n : 1 to mean that n is an element of the monster group, and you can write n : 2 to mean that n is a binary tree, and you can write n : 3 to mean that n is a complex number. This would, of course, not "break anything". All you have done is introduce some new (and bad) notation.

[Mitchell Lee]

You could even decide, totally arbitrarily, that n : 4 means that n is a natural number. Then you'd have 4 : 4. There would be nothing wrong with this, except that no one would understand what you mean.

[Mr Proof]

OK. But what about this. You are an object right? But if I clone you, then I will say there are two objects of type Mitchell Lee. So the object has become a type.

But then we have introduced two new objects. So there are still objects there but what was once an object is now a type.

But nothing that was done has made anything inconsistent, so would it have mattered if everything was a type to start with?

[Mitchell Lee]

If you were to clone me, the result would be two people. The type of each of them would be Person, not Mitchell Lee.

[Mitchell Lee]

You seem to be familiar with C++. It, similarly, does not have "types all the way down". Consider the following code snippet:

int x;
3 y;

Of course, this doesn't make any sense. The first line compiles because int is a type. But the second line doesn't compile because 3 is not a type. You could theoretically make an extension to C++ where the notation 3 y; means whatever you want it to mean. This would not affect any currently existing C++ programs. However, there would be little point in doing so.

[Mitchell Lee]

As Kyle pointed out, the C++ version of the Lean notation x : A is not class x : A {}, but rather A x;.

[Mr Proof]

Yeah, I think you're right. I keep thinking in terms of inheritance where things can have more than one type. It's hard to get forget all that and get into the Type Theory mindset! :smile:.

[Mitchell Lee]

Things cannot have more than one type in C++, either. Like Lean, it has a coercion (casting) system whereby a term of one type can be reinterpreted as another type.

[Dean Young]

3.0+.

[Dean Young]

0 0.
*+

[Kevin Buzzard]

I think that in fact lean would be easier to understand if instead of making "everything can be a type" true (which has been pointed out to be kind of meaningless) we could in fact make "everything has a type" false. In my mental model of lean there are three levels: terms like 37 (which aren't supposed to have elements), types like Nat and Real (things which are supposed to have elements) and then universes like Type and Prop (which are just there to be collections of everything and that we don't use as variables, and "term of type Type" is just a silly way of saying "type"). I think that the fact that Prop has type Type is an artifact of type theory and is not used in our mental model (we don't think of sets as functions, we have API to make it look like this is not happening), and the fact that we use the same notation for t : T and T : Type is not actually necessary because in practice we know whether our objects are "sets" or "elements".

[Notification Bot]

This topic was moved here from #maths > Why types all the way up but not all the way down? by Johan Commelin.

[Jason Rute]

@Kevin Buzzard what you are describing reminds me of simple type theory / HOL like in HOL-Light or Isabelle/HOL.

[Mark Fischer]

This isn't the most related thing ever (It's not about Lean at all actually), but there's this old post by Mike Shulman about Martin-Löf dependent type theory that goes into some philosophy on the topic of foundational systems.

link

Thus, we ought to seek a foundational system which:

1. contains structural-sets and their elements as basic things, but also subsets of these which behave like material-sets;
2. contains both the structural quantifier-bounding membership and the material membership proposition; and
3. allows elements of structural-sets to have some internal structure, but doesn’t force them to always have a particular kind of internal structure. The elements of a structural-set should have different structure depending on what that structural-set is: they may be material-sets, or functions, or ordered pairs, or natural numbers.

In fact, such a foundational system already exists: it is called Martin-Löf dependent type theory (MLTT)

I think that third point sort of hints toward a reason that you may not want all terms to also be types. It's simply nice to think of 27 as a Natural number without also having to think about it as a Type/Set/Etc.

[Eric Wieser]

Mr Proof said:

You could define both +3 and -3 as of type Nat.3 since they are both "types" of 3's. (yeah, no-one would actually do this probably as it would be confusing!)

Note that you can make this work, but it's not "types all the way down":

import Mathlib

instance : CoeSort ℕ Type where
  coe n := {z : ℤ // z = n ∨ z = -n}

instance (n : ℕ): OfNat (n : Type) n where ofNat := ⟨n, .inl rfl⟩

-- 3 : { z // z = ↑3 ∨ z = -↑3 }
#check (3 : (3 : Nat))

[Eric Wieser]

Here you're not telling Lean that 3 : Nat is a type, you're telling it how to convert it to a type

[Mark Fischer]

I guess another way to look at this is that Types all the way up is a solution to a problem.

If you just enjoy reading/thinking about this topic, a good subject to get into may be to learn why Lean's Type Universes are the way they are. As far as I understand it, we'd prefer not to have Types all the way up but it's there as a solution to Girard's Paradox.

Types all the way down may or may not break things (I'm not really sure), but it would certainly complicate things which means you'd need a good reason for its presence rather than a reason for its absence.

As far as I understand it; you can't (given the current system) always have an Types all the way down forever. For example 1 = 2 : Prop : Type : Type 1 : Type... is a Proposition for which there must be no inhabitants (If there were, it would be interpreted to be a proof of 1 = 2). Which means at least sometimes the downward direction must just stop.

[Mario Carneiro]

I think this is not quite accurate, because it's mixing two things. 1 = 2 is a false proposition, so it has no inhabitants, but it is a type so h : 1 = 2 is well formed. That means you could have this as a hypothesis or lambda/pi binder, even though it happens to be a false supposition. Compare this to x : h (for such an h : 1 = 2), which is not even well formed: if you write example := fun (h : 1 = 2) (x : h) => trivial you get an error, because h is not a type and so cannot be used in the type position of a lambda.