The so-called "untyped λ-calculus": how many types does it really have?

[λ the β-Redex Reducer]

Some say that the so-called "untyped λ-calculus" has no types. But of course, Many know that it does have types. It has the universal type, and all terms are members of that type. Ignorance of that type does not mean it does not exist, it just means one is ignorant of it's existence. But even among those who recognise the universal type of the so-called "untyped λ-calculus", much ignorance exists. The ignorance that I am talking about is ignorance of the second type of the so-called "untyped λ-calculus".

That second type is the ⊥ type. Types are theorems, and terms are proof. ⊥ is the theory that λ-terms do not exist. And it has no members at all. There is no proof of this false statement.
The universal type and ⊥ are each other's respective opposites. One is the theory that λ-terms exist, and each λ-term is a proof of that theory. And the other is the theory that λ-terms do not exist, and that theory has no proof. Therefore, the universal type has all λ-terms as members and ⊥ has no members.

And therefore I would like you all to stop referring to the duotyped λ-calculus as "untyped λ-calculus" or "unityped λ-calculus" and to start referring to it by it's real description: "duotyped λ-calculus".

 

[pyrat]

Bah. Don't be manichaean.

 

[matzesu]

I dont understand anything, but i have maybe one of the lowest education backgrounds of the whole boards .. "Hauptschulabschluss whitouth an Exam" (General Certification of Secondary Education) ... Whe didnd had Math whit Keys instead of Numbers par exemple..

 

[netcat]

Applying the Bible (literally) to math?

I prefer stochastic calculus.

 

[matzesu]

Booth are stuff nobody really needs .. it is only important for you that you can count until 20 : This way you know after the work whit the Woodsaw that you have still all Fingers and Toes ^^

 

[TeDaDeS]

I don't label them based on only those two boxes, so it's multityped λ-calculus for me.

 

[Bosbeetle]

Didn't Gödel already settle that what you are saying is either incomplete or false?

 

[matzesu]

What dos this whole Start Post mean anyway? Could someone please explain it in Easy English? , It is not so that i would have an mind which dont let me understand this stuff, but i did not had this in my last 40 years even though i rode lots of "Boulevard Since Magazines" ..

 

[pyrat]

I'm not sure, but I'd say it's more about Democritus versus Parmenides than about Gödel.

 

[pyrat]

What dos this whole Start Post mean anyway? Could someone please explain it in Easy English? , It is not so that i would have an mind which dont let me understand this stuff, but i did not had this in my last 40 years even though i rode lots of "Boulevard Since Magazines" ..

I'm at a loss at where to start from. I'm not even sure I understand it, because I never formally studied type theory (and much less λ-calculus than I'd like, and I cherish lisp like some youth love affair, even if lisp is not FP).
I think the gist of it is whether you attribute existence to falsehood or you decide that what is false doesn't exist, and so it can't be counted.
You may think there are lots of different types of things or you could think that isn't so important, so basically there are things, and there's just one type of things, that of existing things, or provable things. And we start from here.

Then, @λ the β-Redex Reducer basically says that the type of existing things is just one type, and there's also the type of non-existing things. Since there are no non-existing things, that second type is empty, but an empty type is still a type. It's just that nothing exists of that type.But you still have 2 types, even when trying/pretending to have just one.
But then, it becomes a semantic problem, more than anything fundamental. The counterargument, if I can go out on a limb, could be something like:

Saying there's just one type, is saying that one type exists. If something exists, it needs to be distinguishable from anything else, or from everything in general.
So in fact, saying a type exists implies there are going to be members and non-members, and even if the number of non-members is 0, that would still define a trivial type by intension.
So saying a type exists is implying that the (potentially empty) type of non-members exists.
So saying there's one type is the same as saying there are two types and the second type is the negation of the first. There is no possible way for a single type to exist without the existence of its trivial negation. So it's not worth talking of the trivial negation.
If (at least) membership defines a type, then non-membership is implied, so @λ the β-Redex Reducer second type is implied in the doctrine @λ the β-Redex Reducer criticizes.
He's not talking of something working different, just talking about the names people use to call notions. Some people just choose not to speak of something that is trivially implied, and @λ the β-Redex Reducer demands to name it.

In other words, there can not be any universal type without ⊥because then the universal type would lack meaning. So saying there's one type implies there's ⊥. And saying there are two types, the universal type and ⊥ means the same as saying there's one universal type.

No set can exist without a membership relation, and no membership can exist without non-membership.

If some people said there is the blue set and the red set, we could argue what's in each, whether there's something in both or something in none. But if someone says it's all the same set, then saying that or saying there's everything in that set and nothing out of it, is not saying a different thing.

 

[matzesu]

My IPad did screw up this post


Gesendet von iPad mit Tapatalk Pro

 

[λ the β-Redex Reducer]

Didn't Gödel already settle that what you are saying is either incomplete or false?

Indeed, he did not.

What dos this whole Start Post mean anyway? Could someone please explain it in Easy English? , It is not so that i would have an mind which dont let me understand this stuff, but i did not had this in my last 40 years even though i rode lots of "Boulevard Since Magazines" ..

Some people claim that the so-called "untyped" λ-calculus has no types. But it does have types, it has the universal type, which all their data is a member of. But that is old news.

But what occured to me recently is that actually "untyped" λ-calculus has even more types. It has the empty type, which is often called "⊥" and which has no members.

Also, there is a view on type theory which sees types as mathematical theories and programs as proofs of those theories.
If we take that view of the "untyped" λ-calculus, then the universal type is the theory that λ-terms exist in the λ-calculus and the empty type is the theory that falsity is true. The latter has no members because false is not true.

And thus the empty type is also represented in the "untyped" λ-calculus, but you never see it because it has no members. And you never see the universal type because it is implicit.

Some people just choose not to speak of something that is trivially implied, and @λ the β-Redex Reducer demands to name it.

The name often used is wrong, not implicitly right. Implying the duotype λ-calculus to be untyped just betrays one's own folly.

 

[pyrat]

The name often used is wrong, not implicitly right. Implying the duotype λ-calculus to be untyped just betrays one's own folly.

It's a duotype only if you count trivial types as types.
If you speak more candidly, nobody cares about those two types, and you can't have anything with fewer types than the untyped λ-calculus, so "untyped" is not a misnomer. There're no meaningful types.
The universal type and ⊥ are there because they can't not be. And I believe they're not used. The theory does not exclude them, because it would have no meaning, but it does not use them.
If you want me to speak weird: "untyped" doesn't mean "untypable", doesn't mean types are forbidden, because you can always define those two types, it just means they're not used, they're not playing a role.
"untyped" doesn't mean "typeless" either. It means the users of that λ-calculus don't go about defining types and using them, they do other things, and can't help the fact that the universal type and ⊥exist.
In fact, in most cases, many other types exist, as in they could be defined and used, they just aren't defined and used because people focus on something else.

An unsorted list is not a list you can't sort. It's a list you haven't sorted. You could, if you cared, or maybe you couldn't, but if you can and don't it's still unsorted.

Types are for classifying, for focusing on some trait of other of members (and thence deducing things). If the only trait you use to define types is existence, then you won't deduce much, so the type, may be formally a type, but is not useful.

Terms are untyped because they're not assigned to a type that sets them apart from other terms. So the λ-calculus of those untyped terms is the untyped λ-calculus. All those terms belong to the universal type. So what? That does not give any information about the terms.

If you say "duotype" people will think there are members in each of the types and you can play with them. So they'll think there are two types besides universal and ⊥.

 

[TeDaDeS]

The historical argument in this discussion was that the use of untyped was to show the focus was on the lack of explicit types and not so much on the two implied types.
Gödel did like to show implicit structures, like you would have with the ⊤ and ⊥ discussion, but I think he never did mention this specific topic explicitly (did he?).

If I would have a time-machine I could go back in time and visit Church and discuss how I prefer Python over Haskell for most programming tasks.

 

[λ the β-Redex Reducer]

An unsorted list is not a list you can't sort. It's a list you haven't sorted. You could, if you cared, or maybe you couldn't, but if you can and don't it's still unsorted.

An unsorted sortable list makes sense but an untyped typed λ-calculus does not. Unsorted and sortable are not opposites of each other like typed and untyped are.

Calling a sortable list an "unsortable list" because we intent to not sort it is like calling a typed λ-calculus an "untyped λ-calculus" because we intent to not use it's types.

If you speak more candidly, nobody cares about those two types, and you can't have anything with fewer types than the untyped λ-calculus, so "untyped" is not a misnomer. There're no meaningful types.

I care about these types but did not know about them because people implied they did not exist.

The historical argument in this discussion was that the use of untyped was to show the focus was on the lack of explicit types and not so much on the two implied types.
Gödel did like to show implicit structures, like you would have with the ⊤ and ⊥ discussion, but I think he never did mention this specific topic explicitly (did he?).

So the right name is "un-explicitly-typed λ-caclulus".

 

[netcat]

duck typing... da best.

 

[TeDaDeS]

An unsorted sortable list makes sense but an untyped typed λ-calculus does not. Unsorted and sortable are not opposites of each other like typed and untyped are.

Calling a sortable list an "unsortable list" because we intent to not sort it is like calling a typed λ-calculus an "untyped λ-calculus" because we intent to not use it's types.


I care about these types but did not know about them because people implied they did not exist.


So the right name is "un-explicitly-typed λ-caclulus".

or "implicitly-typed λ-calculus".

 

[pyrat]

I care about these types

Oh! These types are so happy now they know someone does that they changed their avatars:

but did not know about them because people implied they did not exist.

It may just be my ignorance of type theory, but I can't figure out how could you imagine the universal and bottom type not to exist...
And how can one imply everything doesn't exist or nothing doesn't exist ?

 

[λ the β-Redex Reducer]

It may just be my ignorance of type theory, but I can't figure out how could you imagine the universal and bottom type not to exist...
And how can one imply everything doesn't exist or nothing doesn't exist ?

I just saw the terms without types like how many people fail to see the real types in so-called "dynamically typed" languages. We all start ignorant, and there are no royal roads to type theory.

 

[pyrat]

I just saw the terms without types like how many people fail to see the real types in so-called "dynamically typed" languages.

I don't know any better than you, but I think you did right.
You didn't see the type you're not supposed to look at because it's untyped λ-calculus
Just like when you look at typed terms when working with typed λ-calculus you are supposed to look at their particular types, not to keep thinking they also belong to ⊤and don't belong to ⊥.
You're supposed to ignore lots of true facts when they don't help in what you're doing.
When one builds abstractions for others to use, those others are supposed to think in terms of the abstractions, not "look behind the curtain".
When you need to fix the interpreter or whatever then you need to think both in whats behind the curtain and what's in front of it (the implementation and the interface).

We all start ignorant, and there are no royal roads to type theory.

Sure. But ignorance of things that are not relevant is good. You seem to worry about things you did right.
Once you know the definition of the top and bottom type, then you already know everything belongs to top and nothing to bottom. You don't have to keep remembering it.
You know those types exist, you just don't think about them because you don't need to.
That's different from thinking those types don't exist.
Before you know the definition of the top and bottom type, well, you don't know all terms belong to top and none to bottom, but that's not like thinking those types don't exist.
It's more like not thinking they exist and not thinking they don't exist.
In fact, before you know about types and relations between types, you don't need a top and bottom type.
Once you define ⊤and ⊥, then thinking they don't exist is odd because it's against the definition, but not thinking about them is normal, at least most of the time.

It's like when they teach you square roots, they may tell you there's no square root of negative numbers. That's true, but only for real numbers (real roots).
Once they teach you complex numbers they redefine things. You can still do lots of things only with real numbers. So that's a perfectly valid road.
But if you say you thought i can't be the square root of a negative number, then that's shocking, because once you know what i is you normally know it's the square root of -1 and -1 is a negative number.

In any case, I didn't mean to criticize or belittle you in any way. It's just that I wondered about your reasoning. Maybe we simply describe things different but mean the same or almost the same.