So... yesterday, I was dwelling in depth on types that "cannot be implemented".
Except, that's not a completely fair statement -- you can implement a finite part of an infinite type. Some operations might fail, but maybe you do not need those operations.
There are several approaches here:
You can fall into an infinite loop when you encounter these situations.
You can introduce runtime checks -- runtime errors. These are no more logically valid than an infinite loop, but have practical advantages.
You can limit yourself to a formally defined finite subset. This can be satisfying, mathematically, but there will be operations which behave differently in this finite system than they would behave if they were members of the infinite system.
This all matters because traditionally numbers are infinite -- if I pick a number, you can add one to it.
So the above three approaches look like this:
1. Sometimes when you add two positive numbers, the system just hangs.
2. Sometimes when you add two positive numbers, you get some kind of error.
3. Sometimes when you add two positive numbers, the result is less than the peano sum of those two numbers.
Which of these is "best" can vary, depending on your own purpose and ideals -- on your own concept of "best".
* * * * *
Note also that the above options are valid in both "statically typed languages" and "dynamically typed languages". So what is the difference between these two?
The distinction between these two kinds of languages has to do with how they treat syntax, and with how people think about problems.
The syntactic distinction is that statically typed languages place an emphasis on "user defined syntax" where when users define "types" (when they describe how they will represent data) , they are also introducing new syntax that is valid for dealing with that data.
In a dynamically typed language, the user defined syntax issue still exists in some vestigial form (undefined names might be syntactically invalid), but greater emphasis is placed on performing checks when the program runs.
Let's try again... in a "statically typed language" we break up evaluation of a program into multiple stages. The last stage is the familiar "run the program" stage. An earlier stage is typically a "compilation" stage (or often a sequence of compilation stages). Runtime errors in the earlier stages are the static type checks.
Nowadays, with relatively cheap computing, compared to the days when people came up with terms like "compiler", this can get blurry. You can have multiple execution stages (compilation and running) happen nearly instantaneously. You can have editing environments (emacs, and other IDEs) that perform some execution for you.
And, you can use a "proof assistant" in the early stages of execution.
And, do not get me wrong, proof assistant's can be fabulously helpful.
But they can never be a substitute for understanding what you are talking about.
* * * * *
So... let's consider one setting where people work on understanding what they are talking about: the classroom.
The classroom is not a perfect learning situation. Just as it's easy to be glib in the context of computer programming, it's easy to be glib in the classroom. And, the professor can be glib sometimes. Hopefully not, but no one is perfect.
All professors are going to have limits on what they understand. And, how they deal with that issue is a reflection on their quality as a professor.
One *good* practice on the part of a professor, is to refer the student to some appropriate resource when the student is venturing into territory where the professor is not prepared to present the information right then. "You might want to read ____."
But this is a declaration, also, that the professor is not prepared to talk about that subject. Maybe the issue is lack of time. Maybe it's a lack of study. Maybe the professor is rusty on the subject.
... anyways, referring someone to a book in place of explaining one's point does not mean that the referrer has an adequate understanding of the subject.
* * * *
(Adendum: too small for a new post, but added after the above text)
Anyways... in some ways the kind of concept I have been labeling as a "Glib Type" is related to an "Abstract Class". The difference, though, is that implementations of an Abstract Class are full members of the abstract class.
With a glib type, you are going to have problem cases. For the peano numbers, for example, there is going to be a number which does not have a successor. (And, if you build out operations like addition, multiplication, and exponentiation, it's going to be easy to achieve problem cases, because those operations involve generating long sequences of successors.)