Exactly. And an object type can be an extension of any number of other object types. And it can also be extended covariantly within each field.
> On Feb 16, 2015, at 12:23 PM, Robbert van Dalen <[email protected]> wrote: > > Mark, > > I’ve grown in knowledge during the past month. > > I now also think Avail object types *are* extensible records. > > .. but Avail objects are better, because you can dynamically dispatch them > with Avail’s multimethods. > > cheers, > Robbert. > >> On 03 Jan 2015, at 17:38, Mark van Gulik <[email protected]> wrote: >> >> Robbert, >> >> Having read the indicated section at the link you provided (and the rest of >> the page), it appears that Avail’s object types are a close fit for >> implementing extensible records. Unfortunately, we don’t currently have a >> lot of documentation online about Avail objects, so here’s a quick primer: >> >> An object type contains an immutable map, called its field type map. The >> map is from atoms, which in this role are called field keys, to types, which >> are the field types. Since maps and object types are immutable and >> identityless, an object type doesn’t *have* to actually contain a field type >> map. It can be implemented with any other representation that provides >> semantically equivalent operations. >> >> Say A and B are two object types. A is a subtype of B iff: >> (1) A’s field type map contains every key in B’s field type map >> (possibly more), and >> (2) For each key in B, A’s field type map at that key is a subtype of >> B’s field type map at that key. >> >> From this, a few properties can be derived: >> (1) An object type can be subtyped by adding a new field key (with some >> associated field type). >> (2) An object type can be subtyped by narrowing one of the field types. >> (3) The subtype relation is reflexive (x⊆x), transitive (x⊆y ∧ y⊆z → >> x⊆z), and asymmetric (x⊂y → ¬y⊂x). >> (4) The union of A and B contains the intersection of the field keys, >> and each field type is the union of the corresponding field types from A and >> B. >> (5) The intersection of A and B contains the union of the field keys, >> and each field type is the intersection of the corresponding field types >> from A and B. >> (6) The object types form a lattice which is multiply isomorphic to >> Avail's full type lattice (except ⊤ and ⊥). This is typical for an Avail >> type family, and occurs any time there is a covariant (or contravariant) >> relationship. >> >> The first property is analogous to subclassing and adding a field in object >> oriented languages. The second property is a statement about covariance of >> object types with respect to their field types (Java does not have subtyping >> of fields, due to erasure and mutability; I’m not aware whether Scala >> supports this). >> >> The second ingredient in the recipe is objects. An object contains an >> immutable map, called its field map. The map is from field keys (atoms) to >> field values (any values). An object O conforms to an object type T if each >> field key of T is present in O, and the field values in O conform to the >> corresponding field types of T, when present. It can be shown that this >> definition implies that if O conforms to T, and T is a subtype of T’, then O >> also conforms to T’, as we expect. This means that if an object is an >> instance of type T, it’s also an instance of every supertype of T. >> Similarly, if an object is not an instance of T, then it cannot be an >> instance of any subtype of T. >> >> There is another useful feature: Every object O has a most-specific object >> type T, such that O is an instance of T, but is not an instance of any >> (proper) subtype of T. Note that such a type T was not necessarily named, >> nor even mentioned prior to the construction of O. >> >> Philosophically, the object types form a lattice based on their shapes, not >> on explicit declarations of lineage. However, it’s useful to attach names >> to some points in this infinite lattice. The Avail library provides type >> declaration operations that compute an object type and synthesize a method >> to answer that type, as well as type-safely manipulate the field types of >> that object type and the corresponding field values of objects having that >> type. >> >> The “explicit” part in “Public explicit class” tells Avail to create a new >> atom and include it as an additional field key (using the atom’s type as the >> field type and the atom itself as the field value). Since nobody else could >> have mentioned the atom prior to its creation (duh), no named object types >> could be equal to the new object type. This is a useful technique for >> defining hierarchies of abstract object types that don’t add or specialize >> any useful fields. >> >> Finally, mutability. The class declaration method >> (Avail/Foundation/Objects.avail, lines 58-63, 990-1375) has quite a few >> options regarding mutability when declaring fields. Because of its length, >> we use multi-line string escapes to make it readable: >> >> "«Public»?«Explicit|explicit»?\ >> \|Class|class_extends_\ >> \|«with >> immutable⁇field|fields««public»?«reconstructible»?_:_«(accessor⁇_)»‡,»»\ >> \|«with mutable >> field|fields««public»?«shared»?«referable»?«read-only»?\ >> \|_:_«(««accessor|mutator|referrer»!_‡,»)»‡,»»\ >> \|«with reconstructor|reconstructors««public»?(«_‡,»)‡,»»", >> >> Using the “Public” keyword at the start indicates whether the type name (1st >> _ on the 2nd line) should be required to be listed in the module’s Names >> section. The explicit flag controls generation of a new field key. The >> extends clause (2nd _ on 2nd line) allows one to specify a supertype to >> specialize. If there are multiple supertypes, simply compute their >> intersection. The third line allows immutable fields to be declared or >> strengthened. Todd recently added the ability to override the accessor >> name. The fourth and fifth lines are for mutable fields. Object types >> don’t actually allow mutable fields; using a variable as the field value is >> just as effective. The mutable field declaration simply avoids the >> corresponding syntactic salt of having to reach inside the variable to get >> to the value that you want. It also generates a mutator method (which >> writes into the variable), and/or a referrer method (returns the variable >> itself). >> >> Besides the mutable syntax, the reconstructor mechanism is a way to reduce >> the syntactic cost of immutable objects. If you have a point with x=5 and >> y=6, and you wish to construct another point where y has moved to 10, a >> reconstructor allows you to say you want a new object with everything the >> same except y=10 instead of 6. More complex examples would have many more >> fields, of course. In fact, subtypes may have added fields that you’re not >> even aware of, but which you want preserved in the new object. Three >> dimensional point might subtype point with an additional z field. In that >> case, simply constructing the point (5,10) probably would not be the right >> thing to do. The reconstructor mechanism will start with the original >> object’s field map and construct a tweaked version with only y replaced by >> 10 – regardless of whether it’s a point, a three dimensional point, a >> magical colored point, or some type that hasn’t been written yet. The >> reconstructible flag in the field declaration allows an individual field to >> be replaced, and the reconstructor clauses at the end specify which >> combinations of fields may be replaced as a group. >> >> There are plenty of uses of objects, object types, and the object type >> declaration mechanism – just search the library for “Public explicit class” >> or “Public class”. I encourage you to use this mailing list to post any >> questions you may have about what you find in the library. >> >> One quick thing I noticed is that the type declarations in Object.avail tend >> to fairly heavily use the type constructors “_?”, “_*”, and “_+”, which take >> a type and create a tuple type based on it with [0..1], [0..∞), and [1..∞) >> elements, respectively. That syntax is only about a month old, if I recall. >> >> Happy spelunking! >> -Mark >> >> >>> On Jan 2, 2015, at 1:05 PM, Robbert van Dalen <[email protected]> >>> wrote: >>> >>> it’s great to hear that avail is alive and kicking! >>> >>> @todd: you have my *deepest* sympathies regarding your loss on the lvm >>> compiler stuff. >>> >>> as a personal note: avail keeps resurfacing as a possible target language >>> for my own project. >>> currently i want extensible records, which can be implemented in scala, >>> although with a lot of type hackery. >>> >>> (see >>> https://github.com/milessabin/shapeless/wiki/Feature-overview:-shapeless-2.0.0#extensible-records) >>> >>> but i now believe avail’s tuples would be a much better fit to implement >>> extensible records. not yet sure how exactly. >>> one way to know for sure is for me to try it out! >>> >>> cheers and the best wished for 2015. >>> >>> - robbert >> >
signature.asc
Description: Message signed with OpenPGP using GPGMail
