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
