Implicit Arrows in Alms

Jesse A. Tov

Presented at NEPLS, March 4, 2011

Alms is a practical language with affine types, but it is not quite as practical as it could be. One thing weighing it down is the need for usage annotations on arrows. For most types, Alms infers how many times values of that type can be used (freely or only once) from the structure of the type, but in general, the domain and codomain of a function type do not determine how many times the function can be used. Thus, function arrows require annotation.

In the common case, however, arrow annotations follow regular patterns, and are therefore predictable. We can exploit this regularity to infer annotations on unadorned arrow types. In cases where the default annotation would be wrong, an explicit annotation can override it. The annotation inference rules have no effect on type soundness, but a good heuristic minimizes the annotation burden while making the implicit annotations predictable by the programmer.

Available:


Publications list | Home