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: Nilone on 16 Apr 2010 06:58 On Apr 16, 10:37 am, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de> wrote: > On Fri, 16 Apr 2010 01:10:50 -0700 (PDT), 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? > > > 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. > > Egh, object is a run-time instance of a type. Class is a set of [derived] > types. IntegerType, as the name suggest, is a type. As you say, a class is a set of types. IntegerType is a specific type, so it's a member of the set, not a class. However, I disagree with "object is a run-time instance of a type". An object is an instance of a class, and a value is a token of a type. Cook's "On understanding data abstraction, revisited" equates classes with co- algebraic types, but I'm trying to model algebraic types and their tokens. I suppose I could create a NumericType class, of which IntegerType is an instance (not a subclass). However, that would not solve the issue of homomorphisms between numeric types, and I still want to define specific numeric types individually. > > > Inheritance requires that the methods of the class accept the same or > > broader set of arguments, while returning the same or narrower set of > > types, right? > > No. Inheritance is always covariant. Right, sorry, I confused inheritance with overriding. > > A covariant argument/result is of the class closure (i.e. polymorphic). An > operation defined on the class = method [in the corresponding > argument/result]. > > Contravariant = no inheritance. An operation contravariant in some > argument/result is not a method in this argument/result = it is not > inherited in there. It is just so because the type is specific > (non-polymorphic). > > > If I tried to inherit my IntegerType from a similarly > > designed RealType, it would require that IntegerType.Divide() accept > > RealValues, which isn't what I want to do at all. > > Why so? If you inherit a method of the interface: > > function "/" (Left, Right : Real) return Real; > > then all arguments and the result are covariant. I see no problem. Except > that some [broken] languages give you no control over the covariance. > > BTW, if you derived Real from Complex, you would like to have Sqrt > covariant in the argument and contravariant in the result. Are there any languages which aren't broken? Preferably imperative?
From: S Perryman on 16 Apr 2010 09:11 S Perryman wrote: > The only other issue is when errors are detected. > U2 can be only detected at runtime. U2 can be detected statically. U1 can be only detected at runtime. U2 can be detected statically.
From: Dmitry A. Kazakov on 16 Apr 2010 09:55 On Fri, 16 Apr 2010 03:58:06 -0700 (PDT), Nilone wrote: > However, I disagree > with "object is a run-time instance of a type". An object is an > instance of a class, and a value is a token of a type. I think you confuse here polymorphic and specific. Values, types and objects can be either. Polymorphic type is a closure of a class. It represents the class as a proper type in the type system. Its values are polymorphic, composed from the type tag and the specific value of. When you substitute a polymorphic value it dispatches. Object is a run-time entity of a given type. Its states correspond to some values of the type. It can be polymorphic or not depending on the type of. Objects appear because neither values nor types are run-time, but rather meanings given to certain computational states. We often ignore this difference talking about values passed, returned, meaning "the actual object has the state corresponding to the value X" etc. > I suppose I could create a NumericType class, of which IntegerType is > an instance (not a subclass). However, that would not solve the issue > of homomorphisms between numeric types, and I still want to define > specific numeric types individually. 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. It probably could be sort of: ... | Abelian_Group (abstract type) | Numeric (abstract type) / \ Integer Field (abstract type) | Real (It is not simple to coin. Of course Integer is in fact an abstract type as well, since machine types aren't integers. So concrete integer types are somewhere down the hierarchy, BTW lacking substitutability for neither true integers and true reals are computable) Now, a use of homomorphism were an ability to write something generic in terms of Abelian_Group. This would work for both Integer and Real, sometimes intermixed, which raises the eternal question of multiple dispatch. > Are there any languages which aren't broken? Preferably imperative? Ada's type system is consistent, but incomplete. 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. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: S Perryman on 16 Apr 2010 10:27 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. 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. 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. > 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) . Regards, Steven Perryman
From: Nilone on 16 Apr 2010 11:36
On Apr 16, 3:55 pm, "Dmitry A. Kazakov" <mail...(a)dmitry-kazakov.de> wrote: > Polymorphic type is a closure of a class. It represents the class as a > proper type in the type system. Its values are polymorphic, composed from > the type tag and the specific value of. When you substitute a polymorphic > value it dispatches. > > Object is a run-time entity of a given type. Its states correspond to some > values of the type. It can be polymorphic or not depending on the type of.. > > Objects appear because neither values nor types are run-time, but rather > meanings given to certain computational states. We often ignore this > difference talking about values passed, returned, meaning "the actual > object has the state corresponding to the value X" etc. Thanks for all that, although I don't really get it yet. I'll have to chew on it a bit. > > 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. > It probably could be sort of: > > ... > | > Abelian_Group (abstract type) > | > Numeric (abstract type) > / \ > Integer Field (abstract type) > | > Real > > (It is not simple to coin. Of course Integer is in fact an abstract type as > well, since machine types aren't integers. So concrete integer types are > somewhere down the hierarchy, BTW lacking substitutability for neither true > integers and true reals are computable) > > Now, a use of homomorphism were an ability to write something generic in > terms of Abelian_Group. This would work for both Integer and Real, > sometimes intermixed, which raises the eternal question of multiple > dispatch. 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. It may make more sense when I get the first part of your post. > > > 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? > > 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)? |