Chris, Brandon, thank you for the input. I believe I understand what you are saying; to reiterate, yes, in the *general case*, neither ML nor Haskell types outrule nastiness such as non-termination. Yes I know about and use Coq a bit. However, ML has an important *special case*: not using functions. Chris, using bang patterns in Haskell do not quite help to statically rule out recursive terms, do they? They just make for a different runtime error. If I said: data Regex = ... | Seq !Regex !Regex Will it actually give the user who tries to construct a recursive value a compile-time error? I suspect not, I'll try it myself to make sure. Roman, thanks, I will try to look that thread up - this is what I am indeed curious about - how to enforce this at the type level. Yes, with a vanilla interface sharing is not observable; some libraries work with it and some do not. I am spooked out by this though: performance guarantees are very different for regular terms and terms with sharing. Consider the regex engine. The "infinite" regular expressions (well, they are not really regular), may suddenly produce an infinte NFA, so memory use may become linear in the input string. Yes, a smart user will understand this, especially in an area that is relatively well-understood such as regular expressions. However I find it extremely disturbing that library designers do not communicate requirements through the type system, and make performance guarantees for all well-typed programs. ML makes it easy, I guess I am just an ML convert :) Thanks, Anton On Sun, 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.) -- brandon s allbery allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms
-- Kind Regards, Anton Tayanovskyy WebSharper™ - type-safe JavaScript in F# http://intellifactory.com