## 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.

## Comment viewing options

### path dependent types

You could easily express this in Scala using path dependent typing, but you'll have to nest style handle in document:

class Document {
class StyleHandle {...}
def NewStyleHandle(style : Style) : StyleHandle;
def AddContent(content :Text, styling : Style Handle);
}


Class nesting in Scala is much more powerful than Java since the object type prefix is used rather than the class type prefix; e.g.,

val a = new Document();
val b = new Document();


will be rejected by the compiler since a and b aren't the same objects.

More generally, I've been working with "slot" based type systems where you can express object graph type relationships. See my Maze of Twisty Classes paper if you are interested in learning more. The idea is to allow us to express arbitrary type constraints within the object graph, not just ones based on one dimensional nesting.

I'd really be interested to hear about other related work that anyone knows about.

### Path dependent types seem

Path dependent types seem tailor-made for this sort of problem and my "desired" style of solution. Thanks, that sends me in the right direction of things to read up on.

I skimmed "Maze of Twisty Classes" a bit, also at the day job we have some WPF, so it was interesting to see how you've built a mechanism that among other things can be used to statically check the use of attached dependency properties (or at least things that serve that role). I need to spend some more time digesting it, but very interesting.

### Ya attached properties! The

Ya attached properties! The idea that the type of a widget could depend on the panel its placed in is pretty powerful. Unfortunately, type systems seem to get very bizarre when types are graphs rather than simple trees; I keep implementing and re-implementing :p.

### Not sure if I understand

Not sure if I understand your problem correctly, but in C# with anonymous types, a possible lightweight discipline pattern I'd suggest to handle this would be something like:

Document a = ...; // in scope, as a local, or param, or field/prop
// along with Text c, and Style s

var rendering = new {

Document = a

};



(where 'rendering' is the anonymously typed guy enforcing the correct scoped document instance)

... Maybe (?)

Just a conventional pattern. Pretty unambitious anyway, but quite simple.

EDIT
1. again, nothing thrilling really, just a pattern applicable in C# 3+ or other language with a similar notion of 'anonymous' types (anonymous to the programmer, though not to the compiler in C#'s case which does craft a class type behind the scene)

2. in the pros, besides simplicity: this notion of anonymous types a la C# makes those 'rendering.Document', etc, auto crafted properties not only statically typed but also read only, with reason; thus, no risk to have some LOC (before the AddContent call site) mischievously reassigning the document instance of concern at hands in that 'rendering.[something]' reference path, behind your back

3. in the cons: for simplicity, I assumed AddContent and NewStyleHandle are part of the Document type spec; but if those are in fact held elsewhere, this pattern will require an additional effort/LOC overhead via, e.g., extension methods in scope over 'this Document...' (another C# 3+ specific)

### Perhaps not the answer you're looking for

The second best thing is to rule out errors with a type system. The best thing is to make errors impossible to express in the first place. Perhaps there is another way to refactor your API? For example instead of making a new style handle by passing in a document, and then attach that style handle to the same document, you could have a GetStyleHandle on a document and remove NewStyleHandle. That way it's impossible to create a style handle that gets attached to the wrong document.

If you really do want to do this with types, existential types may help. They allow you to ensure that values passed back into a module are the same as you got out of the module.

The signature would become like this:

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

Now you can only pass a combination of Document[T] and StyleHandle[T] to AddContent where the T's match up, and the only way to get a StyleHandle[T] is from a Document[T]. NewDocument would have the type Void -> exists T. Document[T].

### This is another solution

This is another solution that Scala would support. Here is another spin on this using object types (like my above solution):

class StyleHandle[T : Document] {...}
class Document {
def AddContent(context : Text, styling : StyleHandle[Document.this]);
def NewStyleHandle(style : Style) : StyleHandle[Document.this];
}


### I'm not sure how

I'm not sure how GetStyleHandle would be any different than NewStyleHandle. The StyleHandle doesn't get attached to the document, the Style itself does. The StyleHandle is used to refer back to a Style added to the document to style some specific content within the document. The document will commonly have many different styles, and the same StyleHandle may be applied to different pieces of content in the document.

I know the API has issues (and the "obvious" solution is just to get rid of the StyleHandle indirection).

### I see. Then you could

I see, so you have one style per content item instead of per document. Then you could introduce a new data type Content and give that a GetStyleHandle.