[Haskell-cafe] regex-applicative library needs your help! (algorithmic challenge)

[Anton Tayanovskyy]

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 at gmail.com> wrote:
> On Sat, Sep 17, 2011 at 22:11, Anton Tayanovskyy
> <anton.tayanovskyy at 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 at 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