Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorAlexisHazell
    • CommentTimeApr 25th 2020

    Create page with some initial contents.

    v1, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeApr 25th 2020

    Thanks. Could you add a lead-in sentence of the form “Object-oriented programming is…”? Before saying what category theory might have to do with it. Thsnks!

    • CommentRowNumber3.
    • CommentAuthorAlexisHazell
    • CommentTimeApr 25th 2020

    Add reference to “Objects and Classes, Co-algebraically”.

    diff, v3, current

    • CommentRowNumber4.
    • CommentAuthorAlexisHazell
    • CommentTimeApr 25th 2020

    Re. #2,

    Certainly! I’m planning to flesh out both this page and the ’functional programming’ page as I get the time. In particular, I’m planning to note that OOP and FP can be regarded as dual to each other.

    • CommentRowNumber5.
    • CommentAuthorAlexisHazell
    • CommentTimeApr 28th 2020

    Fill out ’Idea’ section, note OOP/FP duality, add references.

    diff, v4, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeApr 28th 2020

    Thanks. But itsn’t it a little circular to just say that OOP is about objects? The Idea-section needs to say what is meant by “objects” in this context. Maybe something like this:

    “The idea of ’objects’ in OOP is to group data types together with the functionalities that will read/write this data. Another key idea is that these groupings may be defined successively, with one object definition inheriting the collection of data and functions from another one, and then adding its own.”

    (?)

    And then, from the category theoretic point of view, I’d be interested in seeing a critical discussion remarking that the dichotomy between data and functions that is being unified by OOP is never there in functional programming in the first place. I suppose.

    • CommentRowNumber7.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 28th 2020
    • (edited Apr 28th 2020)

    Thanks very much for creating this page, Alexis! I have not looked much at the literature on object oriented programming, but I tend to think about it as a form of programming where one has the freedom to create one’s own types. In a functional language, one begins with certain types, and builds others out of these canonically (coproduct types, products of types, dependent products of types, etc). Whereas in an object oriented language, one has complete freedom to specify introduction rules (’constructor’), elimination rules (public methods), and computation rules (given an object of the type, how do we compute the output of a public method?) for a type (’class’).

    There are numerous practical differences, especially around object encapsulation (’private’ computation rules, for instance), and of course with regards to low-level implementation (a functional language had better have a highly optimised implementation of recursion, for example!), but the above is what I feel is the main difference type-theoretically. I don’t know how that corresponds to the literature, I will try to take a look when I get the chance.

  1. We can also compare to ’low-level’ languages like early forms of Fortran (Fortran now has object oriented structures!), where one only works with primitive types like integers, and introduces no abstractions on top of these at all; the abstractions are solely contained in the organisation of the code (definition of subroutines). One can view assembly language like this too ultimately, except that it has very few possibilities for organisation of the code.

    C has a bit more abstraction than Fortran, e.g. it does have first class functions, and also has ’structures’, which allow for limited construction of types. But it certainly could not be said to be functional, and is definitely not object oriented either.

    • CommentRowNumber9.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 28th 2020
    • (edited Apr 28th 2020)

    People tend to focus on things like mutability, side-effects, etc, but I still would feel that the point of view of #7 is more fundamental. One can work completely immutably in object oriented languages as well, it is just that one is not forced to do so. And if one really wanted one could use only ’pure functions’ as well. A functional language may have optimisations with regard to the fact that it can assume immutability and no side effects, etc, but these are practical matters of implementation of the programming language; one could just as well include such optimisations in an object oriented programming language implementation as well, there is nothing theoretically preventing this. But a computer is fundamentally not functional and is fundamentally mutable (you are not going to get very far if you cannot change a 0 to a 1!), so there is little incentive to do so!!!

  2. Some related discussion from a few years ago can be found here

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeApr 28th 2020

    Hi Richard,

    can one not emulate any given object definition with a dependently typed functional language by just writing out a big universal construction (i.e. some potentially involved fiber product of pushouts of…)?

    (Genuinely asking. And hoping that the entry could eventually explain this.)

  3. Hi Urs, interesting question! My feeling is that the answer is no. I think that what you suggest would correspond to restriction of the type theory to that of a Martin-Löf type theory. In other words, I think that you are basically asking something akin to: is every type theory a Martin-Löf type theory? To which the answer is definitely no. I would say the main difference is that in MLTT there are very few ways to construct types from existing ones. One does not have the freedom to define ’rules’ however one wishes. In an object oriented programming language, as I see it, we are in the more primeval state of being able to define whatever rules we like.

  4. In particular, one could construct MLTT in an object oriented language. Going the other way seems impossible to me.

    • CommentRowNumber14.
    • CommentAuthoratmacen
    • CommentTimeApr 28th 2020

    Hi folks. Guess I’ll throw in my two cents, since I’m interested in programming languages.

    OOP is an overloaded term. A lot of terms in computer science are overloaded, but OOP is particularly overloaded, somehow. (Doesn’t help that “object-oriented” sounds like it ought to be a synonym of “thing-centric”. Real descriptive.)

    The aspect of OOP this article is probably talking about is method dispatch. Calling a method on an object can be thought of as sending the object a message, which it interprets, and hopefully returns a result. Different objects, even of the same type (if applicable) can handle the same message in completely different ways, just like different functions of the same type can handle the same argument in completely different ways.

    In fact, in the dynamically typed case, Scheme effectively unified OOP and impure functional programming. Objects are functions, performance and convenience issues notwithstanding. Doing a better job handling both functional and OO styles seems to be basically about having serious support for both positive and negative type constructors. (Note: Even dynamically typed languages have type constructors, semantically.)

    OOP languages traditionally have weak support for positive type constructors because they fake it with things like class hierarchies (for coproducts) and accessor methods (which provide negative products, rather than positive products). Some mainstream functional programming languages have weak support for negative type constructors (other than function types, of course) simply due to having been designed in the 80’s. ¯\_(ツ)_/¯

    I’d really like it if people stopped associating functional/OO with positive/negative type constructors. There are other differences between the styles people tend to mean by “functional”/“OO”. Language-wise, yeah, there are “object-functional” languages, which have decent support for both positive and negative type constructors. Modulo performance and convenience, they are essentially the same as OO and impure functional languages, which were already essentially the same. (Higher-order imperative.)

    • CommentRowNumber15.
    • CommentAuthoratmacen
    • CommentTimeApr 28th 2020

    Re #6:

    I think that’s pretty good.

    We should probably point out that objects-and-methods are a different way of grouping operations with their data than abstract data types, modules, or type classes. (And confusingly, Simula descendants (e.g. C++, Java, C#) support both abstract data types and objects-and-methods via class definitions.)

    I don’t think inheritance is a key idea of OOP. (It’s considered by some to be a key feature of class definitions, and it’s possible without classes too, but still.)

    • CommentRowNumber16.
    • CommentAuthoratmacen
    • CommentTimeApr 28th 2020

    Re #7:

    The distinction that I think you’re making is usually referred to as structural vs nominal type systems. Typed functional languages do tend toward structural typing, and OO toward nominal typing. But ML-style datatypes (and many similar things like inductive type definitions in Coq/Agda) are actually quite nominal, in that the newly defined type is always “fresh” in terms of type equality. Aside from simple research languages, purely structural typing seems very rare. (BTW, I’m talking about judgmental type equality.)

    In terms of expressiveness, both approaches are about the same, to my intuition. There are rules about how a type definition can be formed, and these rules can all be simulated by a corresponding type constructor. These compound simulations of type definitions tend to perform poorly, but I think polarization or call-by-push-value could help a lot with this, since you can “blame” all the overhead on polarity shifts. So the type definitions, if you think about it, are schemas for type expressions that are well-polarized without needing shifts. I think these are called “dipoles”. For intuitionistic logic, there seem to be essentially only two kinds of dipoles: the positive ones, which are a lot like ML datatypes, and the negative ones, which are a lot like Java interfaces. (I know, I haven’t addressed class definitions. Problem is: their semantics can be quite different in different languages.)

    The different handling of type equality makes structural and nominal typing different though. They’re both nice. As a consideration for dynamic languages, nominal typing seems like a more practical basis for run-time type checks, since the type comparisons are naturally very fast.

    • CommentRowNumber17.
    • CommentAuthoratmacen
    • CommentTimeApr 28th 2020
    Re #8: C has function pointers, not first-class functions. You can only define functions in the empty context.
    • CommentRowNumber18.
    • CommentAuthoratmacen
    • CommentTimeApr 28th 2020

    Re #9:

    I think allowing mutation is actually pretty important to the difference between OOP and functional programming. It’s not just that mutation is real. It’s also that OOP provided a new way of organizing stateful systems, based on decomposing them into smaller stateful systems that communicate with one another. (This kind of decomposition was not new, but OOP made it much easier.) This is different from “procedural programming”, where a bunch of procedures tend to share a big data structure. They are both imperative programming, but the way you reason about them is very different. Without state, OOP does not seem to me like a compelling alternative.

    • CommentRowNumber19.
    • CommentAuthoratmacen
    • CommentTimeApr 28th 2020

    Re #11: Basically yes, provided the type definition in question actually has a (weak) universal property. In many dynamic languages, it actually doesn’t. You might want to look into the polarization and dipole stuff I was getting at. Basically, a dipole can also be understood as a big complicated type constructor with a big complicated universal property. As for why dynamic languages often don’t get you universal properties, briefly, a major aspect of a language design is: what partial solutions to the expression problem do you support? The partial solutions that are compositionally well-defined are basically positive and negative type constructors. Many dynamic languages combine the flexibility of these two solutions into one notion, and end up with the guarantees of neither. (Wikipedia makes it sound as if the problem is completely solved. I don’t believe it. Those are all partial solutions that work by giving up guarantees, I figure.)

    Re #12,13: So it sounds like Richard has in mind a solution that’s more flexible than MLTT, and presumably less well behaved.

    • CommentRowNumber20.
    • CommentAuthoratmacen
    • CommentTimeApr 28th 2020

    Re #13:

    You could easily interpret the computational content of MLTT in almost any language. But the static type guarantees of MLTT are not available in most languages. As you suggest, MLTT is computationally rather weak, so it can’t computationally interpret most programming languages. It can mathematically interpret them, though.

    Wouldn’t it be nice if there were an approach that tried to conveniently combine both kinds of interpretive strength? ;)

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2020
    • (edited Apr 29th 2020)

    Okay, thanks. So in view of #15 I have added to the very beginning of the Idea-section this:

    An object in the sense of object-oriented programming languages (OOP) is a language construct that groups data types together with function types of functionalities (“methods”) that read/write this data. Often there is an emphasis on the possibility of defining such object specifications successively (“inheritance”), with one object definition inheriting the collection of data and functions from another one, and then adding its own.

    diff, v5, current

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2020

    By the way, my impression is that, historically, the rise to prominence of OOP goes along with the rise of graphical user interfaces: The archetypical example use of inheritative OOP-objects is for coding a zoo of widgets.

    If that’s right, it might be worth adding to the entry, for illustration. But I will not further edit here myself.

    • CommentRowNumber23.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 29th 2020
    • (edited Apr 29th 2020)

    Re #17: That is strictly true, of course, but I don’t feel that the distinction is very relevant here; one could say the same about arrays.

    Re #21: I don’t think the quoted lines are optimal. Firstly, it ignores the distinction between classes and objects. Secondly, methods are definitely not function types, they are more like certain rules. Thirdly, one typically today does not ’write’ the data. Let me try to give an example below.

    Re #16: I don’t think this is exactly what I’m getting at. Again, let me try to give an example.

    Here is a quick example. We might define in Java a class of natural numbers sufficient to define addition as follows.

    public final class NaturalNumber {
        private final NaturalNumber successorOf;
    
        private NaturalNumber(final NaturalNumber successorOf) {
            this.successorOf = successorOf;
        }
    
        public static NaturalNumber zero() {
            return new NaturalNumber(null);
        }
    
        public NaturalNumber successor() {
            return new NaturalNumber(this);
        }
    
        public boolean isZero() {
            return successorOf == null;
        }
    
        public NaturalNumber getSuccessorOf() {
            return successorOf;
        }
    
        public NaturalNumber add(final NaturalNumber n) {
            NaturalNumber remainingPartToAdd = n;
            NaturalNumber withAddedPart = this;
            while (!remainingPartToAdd.isZero()) {
                withAddedPart = withAddedPart.successor();  
                remainingPartToAdd = remainingPartToAdd.getSuccessorOf();   
            }
            return withAddedPart;
        }    
    }
    

    Let us discuss the differences between this example and a definition of the natural numbers in a functional language. Firstly, note that I have not defined any objects in the above code, I have defined a class. I have provided two ways to actually construct an object of this class, i.e. two introduction rules, namely the methods zero and successor. Both of these rely on the actual constructor of the class, i.e. another introduction rule, which is not exposed. So what we can say at a very basic level is that classes correspond to types, and objects to terms. But we can say much more than this. There is no notion of ’inductive type’ that I am relying on there, I am writing down the introduction rules by hand. This is what I am trying to get at: we have the freedom to ’construct’ a type theory with whatever rules we like, we are not using ’canonical’ constructions.

    Note in particular that the ’successor’ introduction rule is a method. It is certainly not a function type; it is more like a rule of the form n:s(n):\frac{n : \mathbb{N}}{s(n) : \mathbb{N}}.

    I view the method ’add’ as an elimination rule, or, better, a collection of elimination rules plus computation rules. Again, it is certainly not a function type. It is not really recursion either, I am using mutability instead, as one usually would in an object oriented language.

    I view the method ’getSuccessorOf’ as akin to a computation rule.

    Finally, note that I do not rely at all on any pre-existing or primitive data types, so one can hardly say that this class is ’grouping data types’ in some way.

    Hopefully this helps illustrates what I mean: in an object oriented language, when we define a class, we essentially write down the introduction, elimination, and computation rules for a type. In other words, we are constructing the rules of a type theory by hand. This is very different in flavour from a functional language. It is not necessarily a question of expressability, i.e. one can of course encode the natural numbers in a functional language as well; the point is that the way of proceeding is very different.

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2020

    All right. It seemed close enough to what any OOP programmer thinks they are doing. But please edit as you see fit.

    • CommentRowNumber25.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 29th 2020
    • (edited Apr 29th 2020)

    I’m not quite sure what best to write; in particular, I am not sure that the point of view I am describing is in the literature. It may be helpful to discuss in detail the example I wrote down vs an implementation in a functional language to see why I feel that what was added in #21 is not quite right, and to see if we can arrive together at something which is a bit more accurate, whether or not it follows the point of view I am suggesting.

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2020

    It’s just about the very first sentence in an informal exposition of what OOP is all about.

    We don’t need literature of sophisticated points of view at this point. Just a first idea. Just so that our entry on OOP does not start out circularly with saying that “Object oriented programming is concerned with objects.”

    Try to get into a mood of informal explaining. Imagine an audience of educated intelligent people who, however haven’t heard of OOP yet. Give them one or two sentences that gives then a rough idea of the subject – enough for them to decide if they are interested in spending the energy to read the more sophisticated account that you will provide further down in the entry!

    • CommentRowNumber27.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 29th 2020
    • (edited Apr 29th 2020)

    I’d like to say something like ’Object oriented programming is a programming language paradigm which emphasises the definition of types (’classes’) and rules (’methods’) for working with and constructing terms (’objects’) of these types by the programmer, rather than by means of canonical constructions as in a functional language (product types, etc)’. But I am hesistant to write such a thing if it is heavily my point of view rather than something appearing in the literature.

    • CommentRowNumber28.
    • CommentAuthorAlexisHazell
    • CommentTimeApr 29th 2020

    This discussion is moving far too quickly for me to keep up with given my current constraints, but one thing I’d like to quickly mention is that, just as OOP doesn’t need to involve object inheritance (cf. composition over inheritance), it also doesn’t need to involve classes - cf. prototype-based inheritance, as seen in JavaScript (which was influenced by Self).

    • CommentRowNumber29.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 29th 2020
    • (edited Apr 29th 2020)

    Good point, Alexis, but I don’t feel this changes the essence of things. E.g. in newer versions of javascript, one does have ’classes’ as syntactic sugar, i.e. I think that javascript does fundamentally follow the same paradigm as I described, just without an explicit notion of class.

    • CommentRowNumber30.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 29th 2020
    • (edited Apr 29th 2020)

    To illustrate this, here is a Javascript version of my Java example above.

    function NaturalNumber(successorOf) {
      if (successorOf == undefined) {
        this.successorOf = null;
      } else if (!(successorOf instanceof NaturalNumber)) {
        throw "A natural number must be constructed either as zero or as the successor of a natural number";
      }
      this.successorOf = successorOf;
    }
    
    NaturalNumber.prototype.isZero = function () {
      return this.successorOf == null;
    }
    
    NaturalNumber.prototype.successor = function () {
      return new NaturalNumber(this);
    }
    
    NaturalNumber.prototype.add = function(n) {
      if (!(n instanceof NaturalNumber)) {
        throw "Can only add a natural number to a natural number";
      }
      var remainingPartToAdd = n;
      var withAddedPart = this;
      while (!remainingPartToAdd.isZero()) {
        withAddedPart = withAddedPart.successor();
        remainingPartToAdd = remainingPartToAdd.successorOf;
      }
      return withAddedPart;
    }
    

    The NaturalNumber prototype plays essentially the same role as a class. In modern versions of Javascript one could make this look even more like the Java version by using the ’class’ syntactic sugar.

    • CommentRowNumber31.
    • CommentAuthoratmacen
    • CommentTimeApr 29th 2020

    I think #21 made it worse. Now it sounds like we’re saying objects are elements of abstract data types, which is wrong. #27 seems like it’s introducing a different meaning of OOP than the rest of the article is about.

    How about:

    An object in the sense of object-oriented programming languages (OOP) is an encapsulated unit of state and behavior that operates on this state. Given an object, you cannot directly access its state, but only invoke its behavior by calling its “methods”. When constructing an object (or defining a class that constructs objects), you have direct access to the state when implementing the methods.

    OOP should be contrasted with the use of abstract data types (ADTs), since they are deceptively similar. Both involve a distinction between a private implementation and a public interface, but with ADTs, the implementation is “private to the type”, while with OOP it’s “private to the object”, and an object is not a type. Assuming the language in question has types, different objects of the same type generally have different implementations of the same interface.

    Many OOP languages allow class definitions, which are a way to share the implementations of methods among the objects “instantiated” from the class (constructed by it). In some languages, classes are treated as types, while in others, they’re only used for object construction.

    Often there is an emphasis on the possibility of constructing objects successively (“inheritance”), with one object inheriting the implementation and interface from another one, and then typically adding more. This is usually managed via the class definitions, which can have a “superclass”. But in some languages it can be done directly between objects, where an object can have a “prototype”. Some languages also support multiple inheritance, which tends to greatly complicate the semantics.

    Sometimes subtyping is thought of as inheritance of an interface, with no associated implementation. Accordingly, typed object-oriented languages often support subtyping. Multiple inheritance of interfaces has less complicated semantics than multiple inheritance of implementations, since there are no coherence issues.

    • CommentRowNumber32.
    • CommentAuthoratmacen
    • CommentTimeApr 29th 2020

    Re #22: That might be just a historical accident, since both OOP and many idioms of GUIs were developed by the Smalltalk project at Xerox. I don’t know if OOP is objectively (no pun intended) a good paradigm for implementing GUIs, and it sounds way too complicated to help illustrate OOP itself.

    • CommentRowNumber33.
    • CommentAuthorAlexisHazell
    • CommentTimeApr 29th 2020

    Well, sure, if one wants to define an instance as implicitly a class, even though a language might not make that distinction (cf. Io), your definition certainly works by fiat. :-)

    Anyway, my big concern here - reading not only this discussion but also the previous discussion in the “Enumerated Types” thread - is the elaboration of the ’OOP’ and ’FP’ pages getting bogged down in definitional debates. The definitions of ’OOP’ and ’FP’ are fundamentally sociological constructs, and are not going to be decided by discussion here; there are regularly debates (ranging from civil discussion through to flamefests) about their definitions. The reason I hadn’t (yet!) elaborated on the definition beyond what I’ve already written is that I’d been thinking about how to describe the various meanings that ’OOP’ has in practice, without making decrees about what OOP ’is’ that might cause fruitless debates (and possibly edit wars).

    What I was hoping is that the OOP and FP pages talk about people’s work on analysing those paradigms from the nPOV: to not only elaborate on CT’s connection to FP (as particularly demonstrated in the Haskell world), but to also show that CT is applicable to more than just FP. (And to have an nLab entry to point to in discussions when this issue comes up, as it did on the CT Zulip recently.) It seemed odd to me that the FP page is so underdone, and that an OOP page didn’t even exist; but if any discussion about the content of such pages is going to end up in definitional debates, I can understand why that might be the case.

    So I’m going to bow out of any further discussion around the definition of OOP (or FP), and instead only make edits to those pages which are about CT in the context of OOP and FP. I’m certainly nowhere near knowledgeable enough about CT to go into all the details, but I figure if I at least make edits backed by references, those in the know can work on elaboration and exposition. :-)

  5. Re #33: absolutely! I should have clarified that what I am trying to do is indicate some aspects of OOP from a point of view that may be helpful from an nPov. In particular, I am trying to indicate what I feel an OOP looks like ’type theoretically’, at least in some cases, in a way that may be comprehensible from the nLab’s material on type theory. In particular, I am not trying to define language features of an OOP, just a few type theoretic ideas that I think are present even in languages without static typing, like Javascript.

    So definitely don’t let’s be dogged down in definitions, and please do not feel inhibited in any way, Alexis! I’ll add something to the entry later, and people can edit or remove as they see fit. In the meantime just proceed however you wish, I’m sure anything you add will be valuable.

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2020

    The definitions of ’OOP’ and ’FP’ are fundamentally sociological constructs, and are not going to be decided by discussion here

    But it must be possible to give a rough informal Idea of the subject – or else we claim it’s an unspeakable?!

    All I was – and am – asking for is that when you create a new entry, to please add a line or two at the very beginning that gives a decent lead-in. Just a kind of mental hand-shake for the reader.

    This just so that a random reader happening onto the page gets the impression that somebody is trying to communicate with them, instead of the impression of having accidentally tuned into the middle of an inner monologue not addressed to anyone.

    This is not about doing any justice to the subject, this is about doing justice to the communication with the reader in the first lines of an entry.

    Given the situation here, I gather maybe it’s best if the Idea-section here is not written by an expert, but by somebody who still remembers what it is like not to be an expert on this subject :-)

    But for the time being, I have copied atmacen’s #31 into the Idea-section.

    • CommentRowNumber36.
    • CommentAuthoratmacen
    • CommentTimeApr 29th 2020

    Re #23:

    Re #17: That is strictly true, of course, but I don’t feel that the distinction is very relevant here; one could say the same about arrays.

    I don’t understand the analogy. I would’ve said C does have first-class arrays. The lack of first-class functions in C makes it harder for C to imitate functional programming than it is for OOP languages, so it’s somewhat relevant.

    Here is a quick example…

    This does indeed define a type of natural numbers (plus null), but the reason is rather fragile. For example, you couldn’t define general W-types in Java. (Or ML, or any mainstream programming language.)

    I don’t know why you included add in the class definition. This doesn’t help your case, since it’s not part of the definition of the natural numbers. Luckily, it didn’t need to be a method. (Also why isn’t successorOf just called predecessor?)

    The main point, for OOP, is that this example isn’t OOP. You’ve defined the natural numbers as an abstract data type whose operations are zero, succ, isZero, and pred. In the presence of general recursion, these happen to be sufficient. To see that the (non-null) elements do in fact all correspond to natural numbers, and that the operations are correct, you need to inspect the implementation.

    This isn’t OOP in any non-degenerate sense because there’s no real method dispatch; the methods all have exactly one implementation, due to the class being final. (And the final is necessary to statically guarantee that the type does not have bogus elements.) I know “OOP” isn’t always meant in a way that implies method dispatch, but that’s the meaning that I think the article is about.

    Let us discuss the differences between this example and a definition of the natural numbers in a functional language…

    Why so much emphasis on the difference between rules and functions? Sure, rules are not first-class, while functions are, in a functional language. But in many languages, functions are not first-class, and even in functional languages, the “first-classness” is usually optimized out. It doesn’t lead to a semantic difference, since nothing stops you from wrapping any old method in a function object.

    But perhaps more importantly, the style you’re demonstrating is functional programming. Specifically, you define a pure functional abstract data type. (I consider it unimportant that you used mutable local variables in add, because the mutation is obviously not observable to the caller.) The reason you don’t ordinarily see natural numbers defined that way in a functional language is because there always seems to be an easier way to do it. (Like ML-style datatypes.)

    I view the method ’getSuccessorOf’ as akin to a computation rule.

    This seems wrong. Intuitions aside, computation rules are technically equality axioms. Do you really want to get into equality of Java objects? :)

    In other words, we are constructing the rules of a type theory by hand.

    There’s an important grain of truth to this. Language itself is an approach to abstraction, and abstract data types deliberately imitate this with a mechanism within a fixed language. This is very powerful. (And has very little to do with OOP.) I mentioned in #15 that class definitions in Simula descendants, including Java, can be used to define abstract data types, and that this is confusing. Maybe you fell for it?

    This is very different in flavour from a functional language.

    But it’s not! Hopefully I’ve said that enough. :)

  6. Hi Matt, I don’t wish to enter into a long discussion here, I just want to say that the following is nonsense.

    The main point, for OOP, is that this example isn’t OOP.

    How on earth is writing something in an object oriented language not object oriented programming?

    With regard to the following…

    I don’t know why you included add in the class definition.

    This is how one does things in object oriented programming! In some sense the whole point of the example is that add should be a method in the class. That you wrote this makes me wonder the extent to which you have hands on experience in working in an object oriented language! I’ll say no more here; as I wrote to Alexis, I wish to add something to the entry, and then people can take it from there.

    • CommentRowNumber38.
    • CommentAuthoratmacen
    • CommentTimeApr 29th 2020

    Re #37:

    How on earth is writing something in an object oriented language not object oriented programming?

    They say you can write Fortran in any language. Meaning you can imitate all the antipatterns of pre-structured Fortran code. So I think writing something in a certain style of language does not automatically give the code you wrote any particular style.

    That you wrote this makes me wonder the extent to which you have hands on experience in working in an object oriented language!

    I’m not a professional programmer, but I’ve written a fair bit of Java code. I do not consider myself a strong proponent of any variant of OOP. I’m not against it; I just don’t think any methodology has a monopoly on good ideas.

    I don’t think having add as a method is a good idea. It’s harmless, in this case, but it does no good, and is completely arbitrary. You can’t put all functions on nats in the class. If the class definition is supposed to be a definition of the natural numbers, addition should not be included, since it’s a consequence of the universal property.

    If OOP says it should be included anyway (which I’m not convinced of), then there’s something silly about OOP.

    • CommentRowNumber39.
    • CommentAuthoratmacen
    • CommentTimeApr 29th 2020

    Re #33:

    The reason I hadn’t (yet!) elaborated on the definition beyond what I’ve already written is that I’d been thinking about how to describe the various meanings that ’OOP’ has in practice, without making decrees about what OOP ’is’ that might cause fruitless debates (and possibly edit wars).

    I like this idea. I’m not sure, but I think the stuff on the article so far is about “Smalltalk-like” OOP. That’s what I’ve been basing my comments on. There’s also “Simula-like” OOP, which seems more like what Richard’s talking about. These are my own labels, possibly stupid, for a difference in emphasis I’ve noticed. I hope I didn’t come across as too insistent about what “OOP” is supposed to mean.

    • CommentRowNumber40.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 29th 2020

    Thanks everyone for making the effort to convey this subtle idea. I’ve no doubt it’s all more subtle than I could imagine, but still I wonder if we could achieve some more clarity:

    An object in the sense of object-oriented programming languages (OOP) is an encapsulated unit of state and behavior that operates on this state. Given an object, you cannot directly access its state, but only invoke its behavior by calling its “methods”. When constructing an object (or defining a class that constructs objects), you have direct access to the state when implementing the methods.

    The first two sentences sound they’re straight from the world of coalgebra as the study of black-box machines via their behaviour streams observed under operations while the unseen internal states change. This is taken up in section 2.

    But then what is the third sentence that I quoted saying? Can the coalgebraic story still be told?

    • CommentRowNumber41.
    • CommentAuthoratmacen
    • CommentTimeApr 29th 2020
    Yes! With the corecursion principle, you construct an element by picking the type of states, and using it to define the behavior.
    • CommentRowNumber42.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 29th 2020
    • (edited Apr 29th 2020)

    I have substantially edited the page to try to incorporate my contributions to the above discussion in a new section ’Examples’. I hope people find this useful :-). I have also rewritten the ’Idea’ section to try to make it a little more user friendly and also more precise in a few places, and I have extracted the comparison with abstract data types to a separate section at the end; I have not read carefully or checked the details of this comparison.

    diff, v7, current

    • CommentRowNumber43.
    • CommentAuthorAlexisHazell
    • CommentTimeApr 29th 2020
    • (edited Apr 29th 2020)

    All I was – and am – asking for is that when you create a new entry, to please add a line or two at the very beginning that gives a decent lead-in. Just a kind of mental hand-shake for the reader.

    I don’t disagree! However, in this particular case, you can see from this discussion, and from the comments on your suggestion as to what such a lead-in might involve, that the extensive diversity of OOP makes this a non-trivial exercise. (And I note that the ’functional programming’ page, which was created several years ago, still doesn’t have an ’Idea’ section, perhaps for similar reasons?) It wasn’t that I thought such a lead-in wasn’t needed, but that, as I wrote:

    I hadn’t (yet!) elaborated on the definition beyond what I’ve already written is that I’d been thinking about how to describe the various meanings that ’OOP’ has in practice, without making decrees about what OOP ’is’ that might cause fruitless debates (and possibly edit wars).

    What I was trying to do was create the overall structure of the page, and then gradually work on filling out the various sections, making small contributions as I had the time and space to do so. At no point have I meant to imply with a given edit that “this is all that needs doing, this entry is basically complete”. In retrospect, I should have explicitly added something like ’[WIP]’ (’Work In Progress’) to each edit message, to indicate that I was actively continuing to work on filling out the page, just in small chunks.

    That said, if you’re saying “Please don’t create a page until you at least have a basic ’Idea’ section, which can then be debated if necessary” - I can certainly do that, and will keep that in mind in the future.

    • CommentRowNumber44.
    • CommentAuthorRichard Williamson
    • CommentTimeApr 29th 2020
    • (edited Apr 30th 2020)

    I hope that what I have written in the entry now explains why the following is not at all accurate.

    I don’t think having add as a method is a good idea. It’s harmless, in this case, but it does no good, and is completely arbitrary. You can’t put all functions on nats in the class. If the class definition is supposed to be a definition of the natural numbers, addition should not be included, since it’s a consequence of the universal property.

    If OOP says it should be included anyway (which I’m not convinced of), then there’s something silly about OOP.

    It is great that you are enthusiastic about the discussion, Matt, but it would be good not to make strong assertions about things that you do not know well from experience, as appears from what you have written to clearly be the case here. Having add as a method here is exactly how things are typically done, and there are good reasons for that. I have elaborated in the entry on this, and given another example from the Java standard library (which is one of hundreds if not thousands).

    This seems wrong. Intuitions aside, computation rules are technically equality axioms. Do you really want to get into equality of Java objects? :)

    I have elaborated in the entry. I exactly have in mind a rule involving equality, as you will see, and it has nothing to do with equality of Java objects. Throughout the discussion, I see some confusion; what I am trying to get at is the type theory behind the code. You are mixing this with programming language constructs, which is absolutely not what I am getting at. Again, I hope the entry now has made this clear.

    I do not consider myself a strong proponent of any variant of OOP. I’m not against it; I just don’t think any methodology has a monopoly on good ideas.

    I wish to clarify here that I am not, and have not been at any point in the discussion, advocating use of OOP rather than functional programming or any other style. I am simply trying to indicate the type theory behind it, and trying to give an accurate description of various points in practise.

    So I think writing something in a certain style of language does not automatically give the code you wrote any particular style.

    I agree, but I can assure you that what I wrote is very typical object oriented code, and I deliberately chose something which should illustrate some of the main points about the OOP style. Though I disagree, I am not interested in debating whether this is really functional programming in disguise; the important point here is that if you give my code to any professional Java programmer, they will have no problem whatsoever understanding it and treating it as perfectly normal OOP code.

    For example, you couldn’t define general W-types in Java.

    I think that you still are trying to think of my implementation of natural numbers in Java as a special case of a general construction, i.e. an inductive type, whereas my point is precisely the opposite, that if we see past the code and look at the type theory behind, we are not making any kind of general type construction, we are just writing down the rules by hand. Actually as I have written it there is no general elimination rule corresponding to induction, so this is not quite, as written, the natural numbers in the same sense as the usual inductive type one. If you tell me which specific W-type you would like with your favourite use of its elimination rule, I am pretty sure I will be able to give you an implementation of it in Java. For that matter, I think one could work completely generally as well using ’generics’, but I have no real interest in doing that.

    • CommentRowNumber45.
    • CommentAuthorUlrik
    • CommentTimeApr 30th 2020

    Added a reference to William Cook’s On Understanding Data Abstraction, Revisited.

    diff, v8, current

    • CommentRowNumber46.
    • CommentAuthorUlrik
    • CommentTimeApr 30th 2020

    Added another paragraph on the differences between objects and ADTs: adding data variants vs adding operations.

    diff, v8, current

    • CommentRowNumber47.
    • CommentAuthorUlrik
    • CommentTimeApr 30th 2020

    Added a short note on the so-called “expression problem” (or “extension problem”) in programming (and verification).

    diff, v8, current

    • CommentRowNumber48.
    • CommentAuthorUlrik
    • CommentTimeApr 30th 2020

    Added a reference to Reynolds’ chapter from 1978 on complementarity of user-defined types and objects (as procedural data abstractions).

    diff, v8, current

    • CommentRowNumber49.
    • CommentAuthoratmacen
    • CommentTimeApr 30th 2020

    I hope that what I have written in the entry now explains why the following is not at all accurate.

    I don’t think having add as a method is a good idea…

    I’m afraid not. Java’s addAll seems to me like quite a different situation than adding natural numbers, since it’s declared in an interface, and mutates the subject.

    I exactly have in mind a rule involving equality, as you will see, and it has nothing to do with equality of Java objects.

    Most of those rules are gibberish to me. If we’re going to discuss this, we’ll need to get those rules into a form I understand. The first two seem OK. In the third, is SS supposed to be the same as ss, or is it a metavariable? It’s unusual to have this equation about successorOfsuccessorOf without a typing rule for the latter. Was this deliberate? It looks like nn ought to be a variable, but then it’s used in the conclusion where it’s not in scope. This looks like a mistake.

    I wish to clarify here that I am not, and have not been at any point in the discussion, advocating use of OOP rather than functional programming or any other style. I am simply trying to indicate the type theory behind it, and trying to give an accurate description of various points in practise.

    And I should clarify that I do not contest your understanding of a certain notion of OOP. I’ve been saying that it’s not the same notion as what the article was previously about. Now it seems to be about two different things without saying so, and I think this is bad.

    I’m also happy to argue about what is a sensible definition of natural numbers, as well as discuss those mysterious typing rules you put up. :)

    For example, you couldn’t define general W-types in Java.

    I think that you still are trying to think of my implementation of natural numbers in Java as a special case of a general construction, i.e. an inductive type…

    I was remarking on the fact that the objects of NaturalNumber do in fact implement natural numbers, in a sense, and that you cannot get an analogous correspondence for all W-types. The problem is not with the computational content. Like I said, MLTT is computationally weak, but it can have W-types. The problem is that W-types are infinitary well-founded, and Java cannot enforce this. (Other than by writing your own type checker in Java, which doesn’t count.) I shouldn’t have brought it up, in hindsight, since it’s totally off topic.

    Actually as I have written it there is no general elimination rule corresponding to induction, so this is not quite, as written, the natural numbers in the same sense as the usual inductive type one.

    You don’t need to (and cannot) postulate an induction principle, since Java doesn’t have propositions. The non-dependent special case of induction is already definable in Java from zero, succ, isZero, and pred. So you don’t need to add that to the definition either. (Or special cases of it, like add.)

    The reason why you have, in fact, implemented a natural numbers type (plus null) has to do with the semantics of Java. The analogous code in Ocaml (using an optional predecessor, say) would also be an implementation of the natural numbers. (Without null!) The analogous code in Haskell (assuming you can encode ADTs somehow, which I’m not sure about) would not be an implementation of the natural numbers, since Haskell constructors aren’t strict.

  7. Tweaking the labels for some terms in the rules in the Java example, to be the same as in the methods.

    diff, v9, current

  8. Hi Matt, regarding the following…

    Most of those rules are gibberish to me

    Though I felt it to be next to impossible to misunderstand, I have now used the same labels for terms in the rules as in the code. Otherwise I’ll not respond to anything else except one point below, as I don’t really feel there’s a discussion to be had along the lines you are trying to draw; I have written things down in the entry now in the form I see them, and feel that what I have written speaks for itself.

    I’m afraid not. Java’s addAll seems to me like quite a different situation than adding natural numbers, since it’s declared in an interface, and mutates the subject.

    Please try to have a little humility and not make blanket assertions, especially when from what you have written it does not seem at all clear that you really know the details of what you are asserting. The fact that List is an interface has absolutely nothing to do with it; I could just as well have formulated a natural numbers interface as follows.

    public interface NaturalNumber {
        NaturalNumber add(final NaturalNumber n);
    }
    

    And then the class I wrote down would implement this interface.

    About ’mutating the subject’: firstly, an interface method has no concrete implementation, so it does not make any sense to say that it is doing anything. It is perfectly possible to have an implementation of the List interface which does not ’mutate the subject’. Secondly, one could obviously change the definition of add in my class slightly to ’mutate the subject’ and have a boolean or void return type, to make the analogy exact. Thirdly, there are plenty of other examples, see for example concat for strings here. I will change the page to use this example.

    • CommentRowNumber52.
    • CommentAuthoratmacen
    • CommentTimeMay 1st 2020

    I’m afraid not. Java’s addAll seems to me…

    Please try to have a little humility and not make blanket assertions…

    This is getting annoying. Is “seems to me” such an outrageous “blanket assertion”? You’ve been speaking as though I came along professing about something I don’t know. I feel that I have done no such thing. I’ve been careful in my comments to try and be precise about what I’m claiming, and I do not claim any more than that.

    especially when from what you have written it does not seem at all clear that you really know the details of what you are asserting.

    Actually, I know exactly how things seem to me, of course. I don’t see any reason why you would doubt my statement about my own perceptions. Correcting my understanding is fine, but remarks like the one I quoted do not help.


    Since it looks like we’re not getting along, I’ll resist the temptation to respond to your technical points for now. It probably wouldn’t do either of us any good.

    • CommentRowNumber53.
    • CommentAuthoratmacen
    • CommentTimeMay 1st 2020

    Do Richard’s typing rules make sense to anyone else? I see that he changed the names, and this resolves my ss vs SS question. But there are still many issues for me. From before (#49):

    It’s unusual to have this equation about successorOfsuccessorOf without a typing rule for the latter. Was this deliberate? It looks like nn ought to be a variable, but then it’s used in the conclusion where it’s not in scope. This looks like a mistake.

    And more similar issues in the later rules. I ask because if they only make sense to Richard, then perhaps they should not be on this page.

    I’m also concerned that Richard’s examples—while they may well be OOP in the sense of the working programmer—are not OOP in the sense studied by e.g. Bart Jacobs and William Cook, which we cite. So more generally, I’m concerned that this page is now talking about two different meanings of “OOP” without distinguishing them.

    I would like it if these concerns are addressed, but I don’t want to unilaterally override Richard’s edits.

    • CommentRowNumber54.
    • CommentAuthorRichard Williamson
    • CommentTimeMay 1st 2020
    • (edited May 1st 2020)

    Hi Matt, regarding #52, the thing is that you persistently, not just in this thread but in others which I am not involved in, make very strong assertions as though they are fact, which are at best your own personal view on things, and are often quite tangential to the main points under discussion; at worse, those assertions are simply wrong, but because you assert them strongly as fact, this forces me or whoever is involved in the discussion to take time to respond. You also, as far as I see, have a tendency to make mountains out of molehills. For me at least, I have extremely limited time, and it is frustrating to me to have to use that time to constantly respond to this kind of thing; thus I felt I had to say something to this effect at times in this thread, though I do not like to do so. Again, I can only go off what you write.

    Regarding mountains out of molehlls, #53 is an example: the rules are supposed to be indicative, perhaps helpful to the category theorist or person who knows some type theory but is not an expert, or whoever. The minutiae are not that important. I don’t mind discussing them, but not further with you at this point.

    As I have already pointed out, it is simply completely ridiculous to suggest that code written in a couple of mainstream OOP languages is not OOP; I am not going to debate this. Certainly you should please not remove my edits at this point; this would not be appropriate for any nLab page without discussion.

    • CommentRowNumber55.
    • CommentAuthorRichard Williamson
    • CommentTimeMay 1st 2020
    • (edited May 1st 2020)

    For what it’s worth, have a look at how Martin-Löf gives the rules for addition of natural numbers on page 40 (page 46 in the pdf) of these notes. Note that I did not consult these notes before writing down my rules; but they are basically exactly the same. It seems a bit unlikely that what Martin-Löf writes is ’gibberish’ too.

    One could strictly speaking give an elimination rule for getSuccessorOf as well as the computation rule I have written, but it hardly seems necessary.

    • CommentRowNumber56.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 25th 2020

    Added a reference

    • Anton Setzer, Object-oriented programming in dependent type theory, in Henrik Nilsson (Ed.): Trends in Functional Programming. Volume 7, Series Trends in Functional Programming, Intellect, Intellect, Bristol and Chicago, 2007, pp. 91 – 108. ISBN 978-184150-188-8, (pdf)

    diff, v12, current

    • CommentRowNumber57.
    • CommentAuthorUrs
    • CommentTimeAug 14th 2023

    added cross-link with lens (in computer science) and pointer to:

    diff, v14, current