Lambda the Ultimate

I don't think, particularly for real-world XML grammars, you would necessarily hit the worst case very often -- that is, if you pick a more clever algorithm than the one you've proposed. ;)

DFA minimization yields the unique DFA and runs in O(n³) (that's just the naive algorithm; faster ones exist). So if you wanted to see if Language(DFA1) is a subset of Language(DFA2), you could do: Minimize(DFA1 - DFA2), then check the result to see if it's the minimal empty DFA.

[EDIT: I just realized that going through DFA minimization to check for emptiness is kind of silly. What's wrong with just doing a graph reachability test (see if you can reach any of the DFA accept states from the start state)? That should be O(states + transitions).]

But like pkhuong said, getting the DFA is the hard part. Going regex to NFA to DFA isn't great because NFA to DFA is potentially exponential time (though in practice it'll probably work fine).

However, I think NFAs are slightly more "expressive" than regexes for the same size (somebody please correct me if I'm wrong here). So maybe there's a way to go from regex to DFA directly that is more efficient than going through an NFA?

Right, it's probably NFA-emptiness testing that's PSPACE-complete then. Either way, you can hit really bad cases, if only when converting NFAs to DFAs... Not that atrocious worst-case performance has ever stopped Hindley-Milner with let-polymorphism from being adopted.

However, I think NFAs are slightly more "expressive" than regexes for the same size (somebody please correct me if I'm wrong here). So maybe there's a way to go from regex to DFA directly that is more efficient than going through an NFA?

By "regex" I assume that you mean alphabet, kleene star, and alternation. In particular, we're leaving out some operators we don't need but that can shorten patterns like intersection or complement.

A minimal DFA from a regex can be exponentially larger than the regex.

A minimal regex from a DFA can be exponentially larger than the DFA.

In that sense, regexs are not more expressive than DFAs and DFAs are not more expressive than regexs - and the lower bound on conversion between them is exponential.

Every DFA of size K is trivially an NFA of size K.

There exist NFAs, therefore, whose corresponding minimal regex is exponentially larger.

Every regex trivially corresponds to an NFA of the same size.

Therefore, you are correct that, in that sense, NFAs are more expressive, for given every such regexp a same sized NFA can be produced - but given some NFAs, an exponentially larger regex is needed.

Suppose that we allow intersection and complement operators in our regexs:

Then there will exist regexs whose minimal NFA is exponentially larger.

I don't know (but it is an interesting puzzle for some rainy day) whether or not there exist DFAs whose corresponding minimal regexs using intersection and complement are exponentially larger. Supposing that there are, then none of the three forms is more expressive than the others. Supposing that there are not, then such regexs (with intersection and complement) are maximally expressive - which (conjecturing, now) seems rather unlikely.

In any event, a lower worst-case bound on direct regex to DFA conversion with or without intersection and complement is exponential so, no, you don't have any short-cut there that is more efficient (in that sense) than going through an NFA.

What I was referring to when I mentioned disallowing nontrivial patterns applies more to testing a single string for membership than it does to construction of such languages. What excited me about this topic was the prospect of parsing for free, but that is clearly not what these languages are about.

In XDuce or XOBE or XHaskell, constructing a regular type refers to constructing a type that describes the parse tree corresponding to a string in that language, not the string itself. Removing that limitation would certainly make static guarantees harder to come by, but such is the fate of any dependent typing scheme.

Rather than thinking about parse trees, it might be more productive to think of "XML Types" as representing guarantees over the values that parser or generator code can accept or create (a transformer does both at once). Those guarantees can be applied by the type system regardless of how the value is represented internally, which may be a parse tree but could just as well be a stream of SAX-style events or a string literal.

What do you mean by "parsing for free"? It's easy to automatically derive a parser from a type signature: that's the status quo out in the 'real world' for dealing with SOAP web services, after all.