archives

Is this region typing, dependent types or something else? What do I need to be able to express this constraint?

At the day job I have an API in which part of it has a structure like so (in pseudo code):


function NewStyleHandle(doc : Document, style : Style) : StyleHandle
function AddContent(doc : Document, content : Text, styling : StyleHandle) : Void

The problem we've run into is that this mistake is pretty easy to make:

declare a : Document
declare b : Document
declare s : Style
declare c : Text

AddContent(a, c, NewStyleHandle(b, s))

The "StyleHandle"s have a sort of scope in the document they're created by. Use the wrong one, and at runtime "bad things" happen. I can check this at runtime, but by then it's too late to alert the programmer, and any default action I take will still be incorrect. I can change the interface, and have AddContent take a Style instead of a StyleHandle, but if you'd be so kind humor me and assume that's off the table.

One approach that has occurred to me is to use witness types, like Document a and StyleHandle a. I believe that could solve the problem, or at least reduce the likelihood of it, but it requires the end user to whip up a new witness type for every instance of document, and the constraint presented by the API isn't quite the one I want to express.

It seems like regions might be applicable, but I don't really need to manage the lifetime of the handles as such, just be sure that they don't get mixed up. Am I barking up the wrong tree? Should I be looking at dependent types? I don't necessarily expect to be able to actually apply a solution like this (although the type witness would be workable, for some definitions thereof), but it would be nice to be able to say "and that's how you prevent this statically" for my own satisfaction if nothing else.