Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Added the page Enumerated Type.
I have added a pointer to Wikipedia to the entry, to provide a minimum of substance. Also I have removed the symbols
because these denote not a finite union of unit types, but a countably infinite union. Something else needs to go here.
Whoops. That’s a dumb mistake on my part. Probably from working with nonstandard infinities too long…
Enum types as used in programming language are sometimes richer than simply a coproduct of unit types. To take Java, one can for instance associate a term of type to each element of the enum (introduction rule), which one can extract (elimination rule). One can also define methods within an enum class (i.e. add additional elimination rules).
Within type theory, I think that such extensions would no longer be regarded as “enumerated”, only more generally “inductive”. However, it might be less ambiguous to rename this page to something like “finite type”.
OK, that makes sense.
I don’t think they would necessarily only be inductive types in the usual sense, though, due to the possibility to add additional methods (elimination rules)?
Methods aren’t elimination rules; they’re just functions that happen to take one or more arguments in a different way, and sometimes have some dynamic resolution of overloading.
The methods I was referring to are part of the definition of a Java class (= type). By an elimination rule here, I was referring to any rule which is part of the definition of the type, and which takes a term of that type as its input. Whether or not you agree with the terminology, the point I was making was that these rules which may be part of the definition of an enum class (= type) are certainly not introduction or elimination rules coming from the definition of an inductive type.
Mathematically, however, they do not affect what type you are defining or what rules / universal properties govern it. You could just as well have defined them afterwards instead of as “part of the definition”; the only difference is that then Java wouldn’t allow you to use the same syntactic sugar to call them.
@4
I just made the page and plan to add more information.
That being said…
Every type, by being a type, has introduction and elimination rules. It would be redundant to say “an enumerated type is a coproduct of unit types with introduction and elimination rules.” Also, because of the equivalence between types and categories, coproducts already have introduction and elimination rules, so it would be doubly redundant.
What’s more interesting is how introduction and elimination rules of emun. types change in the presence of products. Is there strengthening? Distribution? Eliminations?
Regarding 10: This is not the case, and is exactly my point. Typically a Java class has private final variables which are set once and for all when an object (term) of that class is constructed (the introduction rule is called). These private variables can and typically are used in the methods defined in the class. They cannot be used outside the class for methods involving objects (terms) of that class. This is why I think it very apt to think of the methods inside a class as elimination rules: they are closely related to the introduction rules in the usual kind of way.
(I should perhaps say that a principal part of my job is programming in Java, so I have a fair idea of what I am talking about :-)).
Well, I’m not a PL-theory person myself, but my impression is that usually when modeling programming languages mathematically, the access-control rules like private/public markers on class members are described at a different level from the underlying data structures. Mathematically, you can do anything with the data that is determined by its universal property, and that’s what I would call the elimination rule. Whether a programming language lets you impose some further scoping restrictions is, I would say, a separate question.
In any case, for the most part nLab pages are about mathematics, not programming, and when we talk about type theory we mean formal systems for mathematics, so I think that’s the relevant context here.
I think that to ignore how type theories are implemented in or reflect actual programming languages is a very limiting perspective :-).
I’m not sure how familiar you are with Java, or object-oriented programming languages in general, but what I am describing is rather fundamental. The methods of a class are part of its universal property, if we assume that this language is appropriate. If one wishes to construct a method (function) outside the class, one has available only the methods/elimination rules it exposes, not the internal parts of the class. In other words, object oriented programming languages such as Java allow a very rich way to define types, so rich that even very basic ways to construct types from other types (product types for instance) are not part of the standard library, and have no special syntax (Java has no tuples, for instance). In particular, I don’t think there is any way to fit the possible types into a simple framework such as inductive types. The public/private distinction is not so important, the main thing is that one can define rules which take (the data of) of a term (object) of that type (class) as input. If this is not an elimination rule, I do not know what is. Note that even if one constructs a Pair class in Java, one would need to add getters (projections, i.e. elimination rules) by hand as methods of the class; there is no canonical way to obtain them, one has complete freedom to add whatever elimination rules one likes.
I’m fairly familiar with OOP, as well as with the arguments for and against it versus other approaches such as functional programming. I did not say that implementation is ignored, only that it is described at a different level. First there is a type theory that describes mathematically what the objects are; then you can add all sorts of bells and whistles on top of that. Nothing stops you from studying the bells and whistles mathematically as well, and people do – the point is just that the type theory that we’re writing about on the nLab is for the most part only about the first level, since that is, for the most part, the more relevant one to the rest of mathematics.
What I am saying is that Java’s type system does not fit into one of the standard paradigms that are studied so far on the nLab, even for something as simple as an enum type. It is not an implementation detail, it is a fundamental part of the type theory that underlies the language. I do not know a nice way to model this type theory mathematically. People may or may not find that question interesting.
If you’re interested in type systems that model more complicated aspects of programming languages like that, I believe there is a large literature on them. One place to start might be Bob Harper’s Practical Foundations of Programming Languages. Personally, I’m not very interested in that sort of type theory; since I’m a mathematician and not a programmer (at least, not by profession – I certainly do plenty of programming), I care more about the aspects of type theory that are applicable to mathematics. I expect the same is true of other nLab contributors (and after all, the nLab is billed as being about “mathematics, physics, and philosophy”, not programming (-: ). But there’s nothing intrinsically wrong with that kind of type theory.
I believe there is a large literature on them.
I imagine that there is indeed. I’ve not seen anything which views the type theory behind Java in quite the way I was suggesting, but I would not be surprised at all to find something. In general, I am rather interested in these kind of type theories, in which one adds a lot of rules by hand, rather than trying to force things into a well-known formalism. (Of course there is much more to Java’s type system than the things I mentioned. Monads have become quite well known recently, for instance, and there are some examples in the standard library (eg, the Optional class, which is basically Java’s version of the Maybe monad), although no special syntax or monadic-level stuff yet, though again it is perfectly possible to write this oneself, one just lacks syntactical sugar.)
Part of the power of category theory and type theory is to actively ignore and hide implementation details so as to focus on universal properties that occur in many areas of mathematics, programming, logic, philosophy, and in life in general.
However, that being said, why not start a page on private/public typing for us, Richard? I’m sure there a use for it mathematics, and we could all be overlooking that.
I’d be more inclined to wait on starting a page until we actually have something mathematical to say about them, or at least a reference to give.
Richard: I am mostly unfamiliar with the extensive literature on OOP, but there is an old paper by Reynolds that you might enjoy, because it articulates some distinctions which I think are related to what you are getting at:
Noam: Thanks very much, this paper was very interesting indeed. I had never come across it before. It is very much along the lines I was sketching.
Keith: I feel that the public/private modifier is not really at the heart of things, and tried to explain this a bit above. The fact that I used private variables in the example I mentioned was just to help illustrate the point I was making more clearly (and it is also what Java programmers typically do in practise).
@5 Mike, Another name for these would be Finite Pointed Types.
These things make very nice subobject/subtype classifiers.
I don’t understand. A finite type isn’t necessarily pointed.
From pointed object
If has finite coproducts, this functor has a left adjoint functor which takes an object to the coproduct 1⊔, equipped with its obvious point (this functor underlies the “maybe monad”). This is often written and called “ with a disjoint basepoint adjoined.” A pointed object is equivalently a module over a monad of this monad.
If our pointed object is some Enumerated Type of the form: , then 1⊔ is another Enumerated Type, no?
A pointed type is one that’s equipped with a point, whereas if you’re just given then none of those s is singled out as the point. Furthermore, the empty type is also finite (it’s the coproduct of zero copies of ), but of course cannot be given any point.
1 to 27 of 27