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 >
