On Sep 18, 2011, at 11:28 AM, Brandon Allbery <allbery.b@gmail.com> wrote:

On Sat, Sep 17, 2011 at 22:11, Anton Tayanovskyy <anton.tayanovskyy@gmail.com> wrote:
By the way, can Haskell have a type that admits regular expression and
only those? I mostly do ML these days, so trying to write up a regex
types in Haskell I was unpleasantly surprised to discover that there
are all sorts of exotic terms inhabiting it, which I did not have to
worry about in ML. Besides `undefined` you can have for terms that try
to define a grammar with nested parentheses. Using regex-applicative
syntax:

expr = ... <|> pure (\ _ x _ -> x) <*> sym "(" <*> expr <*> sym ")"

The general case for this is solving the Halting Problem, so neither Haskell nor any other language can do it.  You can disallow infinite values by encoding the length into the type, but (a) in Haskell this is painful and (b) runtime values now require runtime types, which you can accommodate but at the price of reintroducing the problems you are trying to prevent.  (Dependently typed languages work better for this, but I suspect the result is rather more draconian than you intend.)

You needn't solve the halting problem. Any reasonable total language can prevent this case and there is no need to keep types as simple as these around at runtime. See the Agda total parser combinator library for an example, but yes, dependent types are overkill.

I usually enforce constraints like this with ! patterns in the constructors, which lets me enforce the fact that at least I know that any attempt to define a cycle like this will bottom out, so I can safely think only inductive thoughts from there out.

Another way is to just define a template Haskell regex quasi quoter, and enforce the limitation there. That of course costs you runtime generation.

-Edward Kmett