Home

Records, sums, cases, and exceptions: Row-polymorphism at work

Video: Records, sums, cases, and exceptions: Row-polymorphism at work, Matthias Blume.

I will present the design of a programming language (called MLPolyR) whose type system makes significant use of row polymorphism (Rémy, 1991). MLPolyR (Blume et al. 2006) is a dialect of ML and provides extensible records as well as their exact dual, polymorphic sums with extensible first-class cases.

Found this to be an enjoyable and thorough overview of MLPolyR, a language created for a PL course that goes all-out on various dimensions of row polymorphism, resulting in a small yet powerful language. (previously)

By Manuel J. Simoni at 2012-11-01 10:12 | Implementation | Type Theory | other blogs | 12240 reads

Comment viewing options

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

Terminology?

Can you please explain in more detail what you mean when you say "polymorphic sums with extensible first-class cases"?

I can't make the phrase make any sense not already made by "dynamically typed variables in the presence of a runtime-extensible set of types" -- the sort of thing that could be implemented as a pointer to an allocated buffer plus a typetag, if the typetag's value is one element of a set which may acquire more members (for interactively or programmatically defined types) during runtime.

This is based mostly on the extant-if-somewhat-rare terminology for the types of records/objects as "products" of the types of their fields; I don't think I'd heard anyone use "sum" in an analogous way before. It's also based on what you said about them being dual to extensible records; If types can be dynamically defined, then it's trivial to define a typetag/case for an arbitrarily extended record -- which will be a new such "product" type -- and allocate a "sum" which is, at a given moment or in a given case, an instance of the new "product" type.

Am I guessing your meaning correctly here?

Ray Dillinger

By Ray Dillinger at Thu, 2012-11-01 16:48 | login or register to post comments

I can't make the phrase make

I can't make the phrase make any sense not already made by "dynamically typed variables in the presence of a runtime-extensible set of types"

Yes, they are indeed very similar, but row polymorphism gives you full type safety (e.g. accessing a record field that isn't there is a compile-time error) - all the while offering full type inference.

-- the sort of thing that could be implemented as a pointer to an allocated buffer plus a typetag, if the typetag's value is one element of a set which may acquire more members (for interactively or programmatically defined types) during runtime.

Yes, that is actually similar to how polymorphic variants are implemented in O'Caml. See page 4 in Programming with Polymorphic Variants.

By Manuel J. Simoni at Fri, 2012-11-02 12:22 | login or register to post comments

The second and third google

The second and third google result for "first class cases": Extensible Programming with First-Class Cases.

By naasking at Thu, 2012-11-01 17:47 | login or register to post comments

What, no lmgtfy link?

FYI, if you search for "polymorphic sums with extensible first-class cases", it's the first, second, and third links. :)

By Matt M at Thu, 2012-11-01 20:55 | login or register to post comments