Purely Functional Ephemeron Tables

Modulo challenges regarding heterogeneous types and garbage collection, it is not difficult to model variable systems from purely functional languages: variable references can be represented by integers, variable states using a table mapping from integers to values. If we restrict or avoid copying (perhaps using substructural or uniqueness types) we can further support in-place mutation.

I’m willing to accept specialized type extensions to safely interact with such tables. There’s a lot of relevant research on heterogeneous or dependent types that I won’t reiterate here. But this leaves the challenge of garbage collection: ideally, a runtime should be able to remove entries from a table that are no longer referenced.

A compiler could easily support special opaque tables with a limited API, such that we cannot observe removal of elements. However, this still leaves the possibility that we construct identical tables with a common origin. Under referential transparency, constructions of the same table should support the same variable reference values. To support garbage collection, we must therefore sacrifice either referential transparency OR our freedom to use values in arbitrary ways.

Reducing our freedom to use values in arbitrary ways is reminiscent of substructural type systems. However, the separation of variable references and variable state tables requires some form of divided or associative substructural type that I haven’t encountered before, and that I’m uncertain how to formalize.

I could easily develop some ad-hoc static safety analysis that covers common use cases for ephemeron tables. But I’d be very interested if anyone has a good idea for formalizing these divided substructural types in general.

Advertisements
This entry was posted in Language Design. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s