Power Rows

Another feature on which we scratched our heads in Opa is the records (and variants, as it turns out to be) structure named Power Rows.

I wrote a couple of blog posts that detail them. The articles are intended to a less PL-savvy audience, but it might interest some of you.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Related work

After of course OCaml use of row typing in objects and polymorphic variants, a few languages have used row-typing for extensible records and variants. I'm thinking in particular of the Morrow experiment by Daan Leijen.

I think there is no coincidence that other "web-oriented languages" (than Opa) have converged towards this style of rich records and variants. This happened with Links and Ur/Web in particular. I'm not extremely familiar with those, but my impression is that Links, like Opa, aimed for concision and ease-of-use, while Ur is more concentrated on powerful type-level record computation.

Daan Leijen is still playing with row types, but using them in a different, less obvious way (than records and variants): as a convenient basis for an usable effect system. It's his new experiment, Koka, and I think it's a fairly interesting development.

Regarding ease of use and naturalness, this style reminds me of the very nice "types as structural patterns" idea of the CDuce system, where it arose as a way to type-check manipulations of XML documents -- not a very foreign application domain.

(I'm still not sold on the use of open, extensible type records as the basis for all the datastructures of the language. In my experience, the subtyping you get between types with compatible constructors is nice, but the "open" aspect can lead to painful inference behavior and error messages. I think there is a design space for closed types using row typing. The Rust team is considering this kind of things, see this blog post on "Datatype refinements".)

Still not sold

I'm still not sold on the use of open, extensible type records as the basis for all the datastructures of the language.

Neither am I. Extensible records present a number of problems in practical development, and it’s nice to be able to restrict the space of what you’re dealing with.

I recently found an interesting variant on extensible records, which for lack of a better name at the time I called “shape inference”. This cropped up while doing partial type inference in ActionScript 3, of all languages. The notion is that an object type is intuitively a union of types of the form “has field x of type T”.

Since this was CFA-based inference, assignment was non-destructive: adding a new field to an object was as simple as extending the union. Updating a field updated the type of the field, and so on. It was nice in that you got a lot of useful information “for free”, but the difficulties of dynamic type inference in general led me ultimately to reduce scope.

Still, I’d like to see a more restrictive language implementing the principles. Preferably one that isn’t defunct, like Morrow. Do you know of such a thing?

Links are borked

Your CDuce and Rust links point to urweb.

Fixed

Copy-paste is, I tell you, a hard problem. Thanks, I fixed the links.

Open, extensible records

I agree that our choice of extensible records is a strong, difficult decision to make.
Since we do our best to target developers which main language is JS, it's hard to live without it, as we still introduce many restrictions.
And still, we want to stick to type inference as much as possible (we break type principality...) for the same reason.
Of course, there are many corner cases where the Opa typechecker will require type annotations. So we both tried to work on improving errors messages and check that the language allows developers to build "real-life" applications without too much pain.