behaviour vs. data first
in [OOP]
|
Prev: Informatics 2010: 1st call extension - 30 April 2010
Next: The Eiffel Compiler tecomp version 0.22 released
From: Dmitry A. Kazakov on 16 Apr 2010 12:56 On Fri, 16 Apr 2010 15:27:48 +0100, S Perryman wrote: > Dmitry A. Kazakov wrote: > >> I see it as the greatest challenge of the contemporary language >> construction to make the type system consistent, complete and efficient. >> Expressing the hierarchy like above [checkable in a static way!] were a >> good test. > > There is a lot that can be checked statically. Yes. > But the type checking system will IMHO have to be more like a > mathematician in applying what is known about a type system to > discern correctness. Hmm, I would like it discerning incorrectness. I mean the type system should have a minimum of false negatives, even at the cost of more false positives. > My belief is that a type checker that has the general mathematical > ability that I had at 18 (ie pre university undergrad level - that > would be mid 1980s UK - not UK now :-( :-) ) regarding proofs, would be > able to allow/prove some very interesting programs using more flexible type > regimes. Do you have any contacts to the Praxis (SPARK Ada)? They are British. >> It requires many things presently unsolved, e.g. multiple dispatch. > > Multiple dispatch is a solved problem from the correctness viewpoint. > For a type system S, and an op M for which multiple dispatch can > occur, the type checker has to show (informally) : > > Regardless of what type of input/output parameters are > used for an invocation of M, there is at least one implementation of > M in S that can be used with said parameters. > > Obviously this requires analysis of a program (S) as a whole. > You cannot do this in a piecemeal way (separate compilation etc) . But that would kill the idea. Clearly, modularity is a too important feature to be thrown away. I still hope that multiple dispatch can be done modular, when the contexts of type declarations were appropriately limited. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Dmitry A. Kazakov on 16 Apr 2010 13:20 On Fri, 16 Apr 2010 08:36:42 -0700 (PDT), Nilone wrote: > On Apr 16, 3:55�pm, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de> > wrote: >> You need them inherit from NumericType in order to be in the class of. If >> you want certain relations (homomorphisms) between them, you need to define >> further classes in the hierarchy. You cannot use concrete types like >> IntegerType as the roots of these classes because they would have >> operations one does not want to have. E.g. integer division. > > My aim wasn't to create a class hierarchy, but to recreate something > like the integer types of procedural languages in an OO context, in > order to study both. In fact, IntegerType as I defined it should be > sealed and final. Hmm, I am trying to understand this. It seems that you presume that there exist some difference between "classes" as known in OO and built-in primitive types like Integer. I think that this is an artefact of type system designs in OOPL. There were many reasons to this. One of them was confusion between class types and types, which led to inability to distinguish them. Another is lack of multiple dispatch. However if Integer is isolated you need not to worry about the either. But then you have to forget about type relations (homomorphisms). > My mind is still pervaded by the algebraic/coalgebraic duality > described by William Cook and Bart Jacobs. I don't see any sense in a > class hierarchy of numerical types, same as I don't see any sense in > composing behaviour in a tuple. Well, but then you need some vehicle to express type relations. The only existing in OOPL is subsumption. To get it you need interfaces to inherit. Hierarchy merely is a byproduct of a relation. In fact, any binary relation is a directed graph and conversely. >>> Are there any languages which aren't broken? �Preferably imperative? >> >> Ada's type system is consistent, but incomplete. > > I definitely need to study Ada. BTW, can you give me a quick pointer > to where the incompleteness lies? 1. not all types can have classes 2. no interface inheritance from concrete types 3. no multiple dispatch 4. no multiple implementation inheritance 5. no supertypes (interface export) 6. no abstract interfaces to arrays, records, pointers etc >> I see it as the greatest challenge of the contemporary language >> construction to make the type system consistent, complete and efficient. >> Expressing the hierarchy like above [checkable in a static way!] were a >> good test. It requires many things presently unsolved, e.g. multiple >> dispatch. > > Wouldn't a consistent and complete type system necessarily be too > limited (i.e. G�del's incompleteness theorem)? It already is in that sense. The program semantics cannot be exhaustively mapped onto types. A type system is weaker than the language as a whole. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: S Perryman on 16 Apr 2010 14:14 Dmitry A. Kazakov wrote: > On Fri, 16 Apr 2010 15:27:48 +0100, S Perryman wrote: >>But the type checking system will IMHO have to be more like a >>mathematician in applying what is known about a type system to >>discern correctness. > Hmm, I would like it discerning incorrectness. I mean the type system > should have a minimum of false negatives, even at the cost of more false > positives. All I am saying is that IMHO a type checking system has to have as a minimum (in order to be useful for developers in general) , the intellectual/proving equivalence of kids whose maths ability is at a particular level. > Do you have any contacts to the Praxis (SPARK Ada)? They are British. No. I was taught "industrial VDM" many years ago as an undergrad, by someone from my university who also worked with/for Praxis. >>Multiple dispatch is a solved problem from the correctness viewpoint. >>For a type system S, and an op M for which multiple dispatch can >>occur, the type checker has to show (informally) : >>Regardless of what type of input/output parameters are >>used for an invocation of M, there is at least one implementation of >>M in S that can be used with said parameters. >>Obviously this requires analysis of a program (S) as a whole. >>You cannot do this in a piecemeal way (separate compilation etc) . > But that would kill the idea. Clearly, modularity is a too important > feature to be thrown away. You aren't discarding modularity. Merely ensuring that multiple dispatch cannot fail for M (whenever the type system detects the possibility) for any given end program using M. This requires system-wide analysis (the end programs in C, Ada etc - where S is static) . You need some "closed world assumptions" in order to be certain that all combinations of input/output types will map to at least one impl of M. For other envs (the dynamic loading / VM of Java etc) , you may not be able to do so. Although I think someone once mentioned here a prog lang called "Nice" (extensions to Java) which supported multiple dispatch and was able to check whether the closure of M covered all the types seen in use as input/output parameters of M (cannot recall if twas done at ".class" load time or not) . Regards, Steven Perryman
From: Nilone on 16 Apr 2010 14:46 On Apr 16, 7:20 pm, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de> wrote: > On Fri, 16 Apr 2010 08:36:42 -0700 (PDT), Nilone wrote: > > My aim wasn't to create a class hierarchy, but to recreate something > > like the integer types of procedural languages in an OO context, in > > order to study both. In fact, IntegerType as I defined it should be > > sealed and final. > > Hmm, I am trying to understand this. It seems that you presume that there > exist some difference between "classes" as known in OO and built-in > primitive types like Integer. I think that this is an artefact of type > system designs in OOPL. There were many reasons to this. One of them was > confusion between class types and types, which led to inability to > distinguish them. Perhaps you can point me in the right direction from my current position. My view at the moment is that interfaces are co-algebraic types aka co- domains, or more simply, an interface describes the features of the objects that will fulfill a particular need or idea, without specifying implementation. Classes are (partial) implementations of interfaces. Objects are state machines built from the code in classes (in a class-based language). On the other hand, a primitive type is an algebraic domain, i.e. a set of values and associated operators via which we can derive these values. Both types are recursively composable. Tokens of both types can be held in variables. Algebraic values can be seen as static immutable objects created and manipulated by static immutable objects (their types). An object's identity can be seen as a unique value in a dynamic domain. In this way, objects and values can be related. As usual, my terminology is probably sloppy. I'll appreciate any insight you can provide. > Another is lack of multiple dispatch. However if Integer > is isolated you need not to worry about the either. But then you have to > forget about type relations (homomorphisms). > > > My mind is still pervaded by the algebraic/coalgebraic duality > > described by William Cook and Bart Jacobs. I don't see any sense in a > > class hierarchy of numerical types, same as I don't see any sense in > > composing behaviour in a tuple. > > Well, but then you need some vehicle to express type relations. The only > existing in OOPL is subsumption. To get it you need interfaces to inherit.. > Hierarchy merely is a byproduct of a relation. In fact, any binary relation > is a directed graph and conversely. Going off into the realm of pure speculation, I'd like to find a way to integrate OO and the relational model. Do I need to duck and run for cover? ;) > > 1. not all types can have classes > 2. no interface inheritance from concrete types > 3. no multiple dispatch > 4. no multiple implementation inheritance > 5. no supertypes (interface export) > 6. no abstract interfaces to arrays, records, pointers etc Thank you, I'll look into that.
From: Thomas Gagne on 16 Apr 2010 17:45
Nilone wrote: > On Apr 16, 8:38 am, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de> > wrote: > >> On Thu, 15 Apr 2010 14:36:37 -0700 (PDT), Nilone wrote: >> >>> OO inheritance doesn't seem to suit algebraic structures. Isn't the >>> co- and contravariance rules on algebraic domains reversed as compared >>> to co-algebraic domains? >>> >> What rules do you mean? >> >> -- >> Regards, >> Dmitry A. Kazakovhttp://www.dmitry-kazakov.de >> > > My view of IntegerType is that it's an object, not a class, and I made > it as much so as the language allowed, hence the static methods and > lack of constructor. You could reference a language which has already figured this out, like Smalltalk. If what you mean by "real" is the primitive data type beneath IntegerType, then how IntegerType implements itself is supposed to be hidden, isn't it? |