Codd 1970 'domain' does not mean Date 2016 'type' [was: burble about Date's IM]
Quote from dandl on November 1, 2019, 4:45 amThe compiler view: various constructs (variables, operators, literals) are declared to have some type.
"Static type" is a better term than "declared type", because static types can be inferred as well as declared. As you point out, a compiler can and does infer that the static type of 1 + 2 is an integer. Type inference ranges from the minimal (C++ auto and Java var declarations) to full Hindley-Milner unification (ML and Haskell).
Erlang's Dialyzer and Python's mypy are both static type checkers layered onto dynamically typed languages (which means languages whose expressions have only one static type, namely Any). Dialyzer works solely by type inference and rejects only programs that can be proved to be not well-typed, as opposed to most type checkers, which reject programs that cannot be proved to be well-typed. Python, like Common Lisp, supports optional type declarations that are ignored at run time: in Python they are used only for build-time static type checks, whereas in Common Lisp they may also be used by the compiler to remove dynamic type checks.
The runtime view: every value belongs to some type, or (given the IM) more than one.
Indeed, and these are precisely dynamic types. They may be checked at run time, as usually in dynamically typed languages, though Common Lisp has a standard "remove all type checks, full speed ahead" declaration in monomorphic contexts. In C they cannot be.
Note that dynamic types and static types are two completely different matters. The value of an expression with static type T must have a dynamic type that is a subtype of T, and that's that, although even that can be false in languages with covariant/contravariant type constructors.
The declared type is long gone -- only the compiler knew that.
Again that varies with the language. Haskell has an under-the-table runtime representation of static types, which are otherwise erased, so that functions may be polymorphic without all instances sharing an implementation, as they must in ML.
Quote from johnwcowan on November 1, 2019, 1:23 pmQuote from dandl on November 1, 2019, 4:45 amThe compiler view: various constructs (variables, operators, literals) are declared to have some type.
"Static type" is a better term than "declared type", because static types can be inferred as well as declared. As you point out, a compiler can and does infer that the static type of
1 + 2is an integer. Type inference ranges from the minimal (C++autoand Javavardeclarations) to full Hindley-Milner unification (ML and Haskell).
I agree, and I was about to say the same. The 'declared type' mentioned throughout TIRT can always be read as the 'static type'. It's what the compiler sees and acts on.
Erlang's Dialyzer and Python's
mypyare both static type checkers layered onto dynamically typed languages (which means languages whose expressions have only one static type, namelyAny). Dialyzer works solely by type inference and rejects only programs that can be proved to be not well-typed, as opposed to most type checkers, which reject programs that cannot be proved to be well-typed. Python, like Common Lisp, supports optional type declarations that are ignored at run time: in Python they are used only for build-time static type checks, whereas in Common Lisp they may also be used by the compiler to remove dynamic type checks.The runtime view: every value belongs to some type, or (given the IM) more than one.
Indeed, and these are precisely dynamic types. They may be checked at run time, as usually in dynamically typed languages, though Common Lisp has a standard "remove all type checks, full speed ahead" declaration in monomorphic contexts. In C they cannot be.
No, they most certainly are not. In TTM terms every value is immutable, has always existed, is 'selected' rather than 'created' and is a permanent member of a set of values that comprise a type.In the case of the IM, the sole difference is that the value is a member of one or more types that are themselves part of a type hierarchy. There is nothing dynamic about it, and as far as I know, no type failure can occur at runtime (except through the explicit use of a cast).
Note that dynamic types and static types are two completely different matters. The value of an expression with static type T must have a dynamic type that is a subtype of T, and that's that, although even that can be false in languages with covariant/contravariant type constructors.
They are, but not relevant here. The value of an expression with static ('declared') type T will be a member of one or more types, each of which is T or 'below' T in a type hierarchy.Note that a member of INT can also be a member of ODD and PRIME, although PRIME is not a subtype of ODD. The value 2 belongs to INT and PRIME but not ODD. There are plenty of other examples.
TIRT does mention co/contravariance, but not in a positive way. I'll leave you to read it for yourself.
The declared type is long gone -- only the compiler knew that.
Again that varies with the language. Haskell has an under-the-table runtime representation of static types, which are otherwise erased, so that functions may be polymorphic without all instances sharing an implementation, as they must in ML.
Again, I'm only talking TIRT. The IM has only values at runtime, from which an MST can be inferred, but there is no declared type.
Quote from johnwcowan on November 1, 2019, 12:57 pmQuote from Brian S on November 1, 2019, 3:55 amNow, there are two kinds of elements in the Universe: those that can have a location in time or in time and space, and those that cannot. Those that can have a location in time are called "concrete." Those that cannot are called "abstract." Don't read anything else into it. An abstract domain contains only abstract elements of the Universe.
While I know what you mean, that definition isn't really well formed. It relegates Sherlock Holmes and Frodo Baggins to the realm of abstracta, whereas they are plainly as concrete as you or me. What's worse is that the physical universe itself (as distinct from the Universe of Discourse) winds up as abstract, as it has no location in time and space: one may say it is time and space.
You're confusing what is fictional with what is abstract. If the Universe of Discourse includes Middle Earth, then what populates Middle Earth is just as concrete as what populates your living room. The main distinction between what is abstract and what is concrete is that abstract objects are independent of time, and as a consequence exist necessarily--that is, at all possible worlds. Holmes, on the other hand, exists only at those possible worlds where Sir Arthur Conan Doyle exists; likewise, Frodo exists only at those possible worlds where J.R.R Tolkien exists.
If the physical universe is being discussed, then it is by definition part of the Universe of Discourse. Moreover, time has a beginning, and the physical universe did not exist prior to the beginning of time; therefore, the physical universe has a location--namely, the interval from the beginning of time up through the current time.
It may be more precise to say that what is concrete exemplifies the property "possibly being located in time" as opposed to the property "possibly having a location in time" because that location in time is an essential part as opposed to something merely related.
Brian
I think what you're saying has a reasonable basis, that the principle is worthy but the naming is at issue.
It's clearly an aspect of philosophy, which means that it must surely have been discussed endlessly since the time of the Greeks (without the need for any conclusion, of course). Do you have a reference?
Quote from dandl on November 2, 2019, 1:23 amQuote from johnwcowan on November 1, 2019, 1:23 pmThe runtime view: every value belongs to some type, or (given the IM) more than one.
Indeed, and these are precisely dynamic types. [...]
No, they most certainly are not. In TTM terms every value is immutable, has always existed, is 'selected' rather than 'created' and is a permanent member of a set of values that comprise a type.
I don't see what any of that has to do with it. Most languages have mutable objects as well as immutable values, but both belong to dynamic types. If you want to call 3 a selector rather than a literal (per usual) or a constructor for an immutable type (which it is), that's fine; the difference is terminological. (In Scheme, 3+4i is obviously a literal, for that's not how Lisps express addition; in Common Lisp the status of #C(3 4) is considerably more ambiguous: literal or constructor?)
In the case of the IM, the sole difference is that the value is a member of one or more types that are themselves part of a type hierarchy. There is nothing dynamic about it, and as far as I know, no type failure can occur at runtime (except through the explicit use of a cast).
It's a mistake to think that dynamic types occur only in dynamically typed languages. Java classes are dynamic types; so are C types (and they correspond exactly to the static types of the expressions that return them). The term dynamically typed language is a bit of a misnomer, for it refers to static typing: it is (as I said above) a language with just one static type to which all expressions belong.
They are, but not relevant here. The value of an expression with static ('declared') type T will be a member of one or more types, each of which is T or 'below' T in a type hierarchy.
Quite so. And what variety of types are these "one or more types" that you mention? Dynamic types! They certainly are not static types.
Again, I'm only talking TIRT. The IM has only values at runtime, from which an MST can be inferred, but there is no declared type.
Okay, like Java.
Quote from johnwcowan on November 3, 2019, 6:42 pmQuote from dandl on November 2, 2019, 1:23 amIn the case of the IM, the sole difference is that the value is a member of one or more types that are themselves part of a type hierarchy. There is nothing dynamic about it, and as far as I know, no type failure can occur at runtime (except through the explicit use of a cast).
It's a mistake to think that dynamic types occur only in dynamically typed languages. Java classes are dynamic types; so are C types (and they correspond exactly to the static types of the expressions that return them). The term dynamically typed language is a bit of a misnomer, for it refers to static typing: it is (as I said above) a language with just one static type to which all expressions belong.
Is that a type-theoretic interpretation?
In type-system terms, Java classes are static types. Depending on use, determining the type safety of a given assignment or expression may be purely static -- all type-checking is done at compile-time -- or partly static (the expression resolves to a particular inheritance hierarchy of classes/interfaces at compile-time) and partly dynamic (the expression resolves to specific class/interface x at run-time and we dispatch or throw an exception accordingly.)
Quote from Dave Voorhis on November 3, 2019, 7:33 pmQuote from johnwcowan on November 3, 2019, 6:42 pmIt's a mistake to think that dynamic types occur only in dynamically typed languages. Java classes are dynamic types; so are C types (and they correspond exactly to the static types of the expressions that return them). The term dynamically typed language is a bit of a misnomer, for it refers to static typing: it is (as I said above) a language with just one static type to which all expressions belong.
Is that a type-theoretic interpretation?
Insofar as I understand type theory (which as I have said is mostly a theory of static types), then yes.
In type-system terms, Java classes are static types.
We are both speaking rather loosely. To tighten up: The name of a Java class like String is also the name of a static type (the type of an expression) and the name of a dynamic type (the type of a value/object). Because static and dynamic types are incommensurable, there is no problem using the same names for instances of them. In Java, the static type of an expression only partly specifies the dynamic type of its value, so one can reflect on a value to determine its dynamic type. (I am omitting all consideration of generic types, which should really be called type generators as in other languages.)
By the same token, a primitive type name like int names both a static type and a dynamic type. In this case, the static type of an expression fully determines the dynamic type of its value. In C this is true of all types, so there is no need for any sort of run-time reflection.
Quote from johnwcowan on November 3, 2019, 7:48 pmQuote from Dave Voorhis on November 3, 2019, 7:33 pmQuote from johnwcowan on November 3, 2019, 6:42 pmIt's a mistake to think that dynamic types occur only in dynamically typed languages. Java classes are dynamic types; so are C types (and they correspond exactly to the static types of the expressions that return them). The term dynamically typed language is a bit of a misnomer, for it refers to static typing: it is (as I said above) a language with just one static type to which all expressions belong.
Is that a type-theoretic interpretation?
Insofar as I understand type theory (which as I have said is mostly a theory of static types), then yes.
In type-system terms, Java classes are static types.
We are both speaking rather loosely. To tighten up: The name of a Java class like
Stringis also the name of a static type (the type of an expression) and the name of a dynamic type (the type of a value/object). Because static and dynamic types are incommensurable, there is no problem using the same names for instances of them. In Java, the static type of an expression only partly specifies the dynamic type of its value, so one can reflect on a value to determine its dynamic type. (I am omitting all consideration of generic types, which should really be called type generators as in other languages.)By the same token, a primitive type name like
intnames both a static type and a dynamic type. In this case, the static type of an expression fully determines the dynamic type of its value. In C this is true of all types, so there is no need for any sort of run-time reflection.
In that sense (at least), we are in agreement.
Quote from johnwcowan on November 3, 2019, 6:42 pmQuote from dandl on November 2, 2019, 1:23 amQuote from johnwcowan on November 1, 2019, 1:23 pmThe runtime view: every value belongs to some type, or (given the IM) more than one.
Indeed, and these are precisely dynamic types. [...]
No, they most certainly are not. In TTM terms every value is immutable, has always existed, is 'selected' rather than 'created' and is a permanent member of a set of values that comprise a type.
I don't see what any of that has to do with it. Most languages have mutable objects as well as immutable values, but both belong to dynamic types.
I don't see what any of that has to do with it. Objects are values, you're just confusing things. Mostly, I suspect, it's because you think 'dynamic types' means something, or at least something we would all agree on.
To me, a dynamic type is a type that can be created at runtime. A few languages have that, but very few, and certainly not TTM/D. TTM/D with or without the IM has static types, all well known to the compiler. The values are dynamic, in the sense that they are chosen at runtime from a large but finite set of possible values as the result of the evaluation of some expression. Without the IM, every value belongs to a single known type. With the IM a value belongs to one or more types, and the set of types to which a value belongs is statically determined, known to the compiler.
The compiler knows that J is an INT variable, 2 is a value of type INT, 3 is a value of types INT and ODD. Only the runtime knows whether J is currently holding the value 2 or 3. The compiler knows that J and J+1 belong to INT, but only the runtime knows whether they also belong to ODD. The values and types are all static, the current value computed by J and J+1 are the only dynamic things.
If you want to call
3a selector rather than a literal (per usual) or a constructor for an immutable type (which it is), that's fine; the difference is terminological. (In Scheme,3+4iis obviously a literal, for that's not how Lisps express addition; in Common Lisp the status of#C(3 4)is considerably more ambiguous: literal or constructor?)In the case of the IM, the sole difference is that the value is a member of one or more types that are themselves part of a type hierarchy. There is nothing dynamic about it, and as far as I know, no type failure can occur at runtime (except through the explicit use of a cast).
It's a mistake to think that dynamic types occur only in dynamically typed languages. Java classes are dynamic types; so are C types (and they correspond exactly to the static types of the expressions that return them). The term dynamically typed language is a bit of a misnomer, for it refers to static typing: it is (as I said above) a language with just one static type to which all expressions belong.
Java classes are not dynamic types per my definition. The classes are static, the instances are dynamic. The classes cannot be changed once created (by the compiler), but the instances can. [I'm wary about the term object, since it has different meaning in C and C++].
They are, but not relevant here. The value of an expression with static ('declared') type T will be a member of one or more types, each of which is T or 'below' T in a type hierarchy.
Quite so. And what variety of types are these "one or more types" that you mention? Dynamic types! They certainly are not static types.
They certainly are static types, and they are well known at compile time.
Again, I'm only talking TIRT. The IM has only values at runtime, from which an MST can be inferred, but there is no declared type.
Okay, like Java.
No, not like Java. A Java class instance carries around a pointer to its class. It only ever belongs to a single type, but it inherits behaviour from the superclass. It can be substituted for values of its superclass, without ever being a value of that superclass.
The IM is fundamentally different. Values do not carry a single type around with them. They simultaneously belong to one or more types, of which one will be the MST for that value.
Quote from dandl on November 4, 2019, 12:15 amTo me, a dynamic type is a type that can be created at runtime.
Okay, then we really are on different tracks. By "dynamic type" I mean "type of a value or, in languages with mutable objects (a superset of values) of an object".
A few languages have that, but very few,
Languages with reflection certainly do: you can create new classes out of nothing on the JVM using ASM at the level of bytecode (equivalent to System.Reflection.Emit on the CLR) or Janino at the level of Java 1.4. Of course you have to declare them as implementing a statically known interface. libtcc makes the same things possible in the C world.
So do languages with eval, which is also reflective: you can for example eval a class definition in Python that you have constructed.
Finally, there are actual meta-object protocols, where the class/method/etc. system is exposed directly to the user through ordinary method calls. This is semi-standard in Common Lisp (it was removed from the actual standard at the last minute), available in all Smalltalks (though the ANSI standard, which is based mostly on standard interfaces rather than standard classes, doesn't have it).
I wrote:
In the case of the IM, the sole difference is that the value is a member of one or more types that are themselves part of a type hierarchy. There is nothing dynamic about it, and as far as I know, no type failure can occur at runtime (except through the explicit use of a cast).
Now that you know what I mean by dynamic type, perhaps you can see its relevance: the dynamic type of a value is its MST (I think).