Drup

Actually, it's been proved for ... longer than PERL exists ?

The various features in PERL allow you to emulate context-free languages. There is a proof somewhere, but it's trivial to see you can use backreferences to parse languages with well-nested parens.

Languages of well-nested parens are known to be non-regular, and thus impossible to write with regular expressions.

Also note that knowing if an arbitrary context-free language is regular is undecidable. That doesn't mean you can't try to optimize down some PERL grammar to a regex, but your optimization will never be complete.

As an alternative data-point:

My firefox session is persistent (tab are restored when I open firefox again). Apparently, I'm around 500 right now, which is a bit above average for me (I usually stay around 300).

Firefox's lazy loading is very good, which means I only have 10 to 100 tabs that are actually loaded. Firefox is still fast in these conditions. Since I use tree-style-tabs, most of the tabs are neatly sorted in trees by topic.

SAT (and SMT) solvers are extremely optimized and very expressive.

Writing an encoding from problem P to SAT is usually much simpler and easier to do correctly than writing a dedicated solver for P. SAT solvers are so efficient than very often they will be competitive with dedicated ones.

At the end of the day, you want to solve your high-level problem, not writing a solver, especially when such good solvers are already available.

No it isn't: The goal is to use a specific construction with specific cards to build a universal Turing machine.

Unlike previous attempts, which used cards that leave some room for Player agenda, this new version doesn't.

And yet the Sagrada Família is being slowly built in Barcelona, and financed mostly by tourism.

If you wonder about linux: gcolor2 (http://gcolor2.sourceforge.net/) does the job.

And for size fetishists: it weights 42KB.

Well, there are lot's of well known compiler techniques to handle closures in that context. It's a little bit out of scope of the article, but it's not very complicated either.

The constraint on the language for this to work well is fairly natural and is actually described in the article: the language should follow lexical scoping.

Unfortunately, since some dynamic languages do not respect lexical scoping, programmers in these languages tends to think of local variables and scoping as something very complicated. It doesn't need to be.

It's untyped then simply typed basic imperative language, which is more or less the first few courses of programming language theory 101.

What does that has to do with type systems? OCaml is one of the fastest compiler around, and yet it has a very rich type system. Julia also has a very rich type system, but is interpreted/JITed. Many compilers are very slow, even thought their typecheckers barely does anything.

The speed of the compiler is related to the design of both the language and the compiler as a whole, not the presence or absence of a decent type system. I would even argue that one of the point to recognize a well designed type system is that it's conceived in a way that admit fast typechecking.

That's ... actually pretty good! I'm usually quite frustrated by those, but this one is not so terrible.

Some remarks:

- Coq is not an ML at all, it's simply implemented in OCaml and has a vaguely similar syntax. I think dependently typed languages should have their own category, as they have a rich history (coming from type theory, obviously).

- Elm is almost certainly more an ML than an Haskell. The only link with Haskell is really the syntax.

- Speaking of Elm, you might want to add something on synchronous languages (You can start by looking up Lustre).

- ML languages with modules, and especially OCaml, took pretty direct inspiration from Modula 2's modules.

- Curry is half Haskell and half Prolog.

Except Perl 6 doesn't enforce it, so you have to guess yourself if you are really in the regular case. Additionally, PCRE used to be exponential for certain "bad cases", some of which were (truly) regular expressions.

My point is simply that Perl doesn't give you any guarantee except "we will try to parse it". Maybe you will hit the right case for the right version of Perl, who knows ? The Web is full of DDOS attack based on exponential PCREs.

With actual regular expression, the complexity is guaranteed.

Well, except Perl doesn't parse regular grammars (it parses much more) and is far from being "one pass" (since the complexity guarantees are not valid anymore) ....

No, Parsing expression grammar (PEG) are not regular grammars at all.

For more resources, I think the related work of my paper has the main ones. The "Kleene meets Church" project has lot's of very good publications on the topic: https://di.ku.dk/kmc/publications/

This is cute! It's basically a nice syntax for full parsing of extended regular expressions. It would make for a very nice tool. Far too often, regular expression tools only implement "matching" (i.e., extract a list of strings). Full parsing gives you the complete parsetree, and thus preserve more structural information, especially under repetitions.

I'm very much in support of anything that uses regex parsing instead of matching. Matching is nearly always the wrong tool and cause more bugs than anything. The only reason it's used is that the engines are easier to implement. I wrote a small paper on how to retrofit parsing on top of an engine that only gives you matching recently (https://gabriel.radanne.net/papers/tyre/tyre_paper.pdf).

Given the amount of prior art in the academic community, patenting this is probably worthless, but eh ...

Combinators make for a very nice Regex API.

In OCaml, most people use the re[1] library for regular expressions (example[2]). I wrote a library called tyre[3] for typed extraction that follows a similar API. Of course these APIs are much more verbose, but they are also very regular(hah!): Regular operators are normal functions of the language, typechecking and completion works, etc.

[1]: https://github.com/ocaml/ocaml-re

[2]: https://github.com/ocaml/ocaml-re/blob/master/benchmarks/ben...

[3]: https://github.com/Drup/tyre

Yes, that's why in Tyxml, we have a set of combinators and an HTML-like syntax, and you can compose them arbitrarily with each other. This way, you can use the HTML syntax (and c/c internet snipets) but still enjoy all the cool functional idioms.

As the maintainer of a similar OCaml library[1], questions to the authors:

- How compositional it is ? I have find that some of the HTML properties are very hard to verify in a compositional way, see https://github.com/ocsigen/tyxml/issues/175

- How do you handle the "subtyping" aspect that is intrinsic to HTML ? Or phrased in another way: what's your type encoding ? :)

- I suppose you desugar to a set of combinators, but you don't really expose those. Why ?

[1]: https://github.com/ocsigen/tyxml/

Regarding ocsigen, It's more appropriate to point to tyxml[1] and its syntax extension [2]!

Note that tyxml goes quite further than Rust's typed-html: the nesting is significantly more flexible, type inference is still complete, and it will verify additional properties like "don't use <a> inside <a>". It can also be used conjointly with reactive and/or isomorphic programming.

[1]: https://ocsigen.org/tyxml/ [2]: https://ocsigen.org/tyxml/4.3.0/manual/ppx

My experience is that people who think that never worked with a language where inference is principal and complete (aka, "good") and/or have poor editor support.

In languages that are still reasonably close to HM and that have decent editor tooling, like OCaml, leaving the type out in the implementation is the common practice. You only write them down in the external API (along with the documentation).

HM type inference works perfectly fine with separate compilation and/or partial files (whichever you mean). See the OCaml tooling for a concrete demosntration.

Subtyping is a fairly large domain, and it really depends what you mean. There are cases where it works fine (again, see OCaml) and other where it's more problematic (see Scala). In any case it's not really HM anymore, it needs to be more.

On that topic, I recently wrote a tool to take a PDF file, an OCaml bytecode file (OCaml can compile to both byte or native code) and smash them together to create a file that is both a valid PDF and a valid bytecode.

https://github.com/Drup/bytepdf

So, if I remember correctly Ange Albertini's nomenclature, chimeras are particular types of polyglots where a single data is disguised as different file formats. For example, consider a file that is both a JPEG of a picture and a PDF which contains the same picture, and the data of the picture is present only once in the file.

I'm not sure why this is linked. This online toplevel is very old. People who want a more modern version, with more exercises should follow the online MOOC [1] or use this website [2]. People who just want an online OCaml/Reason interpreter to play with should use https://sketch.sh/ml

1: https://www.fun-mooc.fr/courses/course-v1:parisdiderot+56002...

2: https://try.ocamlpro.com/learn-ocaml-demo/

The Mamluks are a major power stuck between the Ottomans and Persia with a weird government form that almost guarantees rulers with a 6 in paper mana.

They somehow often colonize Australia.

This probably means your code is wrong. You should not raise and catch exceptions normally in Lwt promises. You should use `Lwt.fail` and `Lwt.catch`. This is described rather precisely in the documentation: https://ocsigen.org/lwt/3.2.1/api/Lwt

Another popular solution in the OCaml community is to stop using exceptions and use Result instead: https://ocsigen.org/lwt/3.2.1/api/Lwt_result

Maybe JetBrain doesn't, but lot's of editor do, thanks to merlin, including vscode.

Most strongly typed languages have such escape hatches ("Unsafe" in haskell, "Obj" in OCaml, "trustme" in Idris,....) . It's something you always need at some point when the typing is not sufficient to properly account for what you are doing.

For instance, Coq code can be extracted to OCaml code. OCaml type system is less powerful than Coq's, so Coq needs to cheat, and the emitted code is full of "unsafe" features. But the program was typechecked with Coq's type system, and is thus perfectly safe.

Of course, the goal of the language designer is to minimize its usage. That's something the Rust people understood very well, and the unsafe blocks are an extremely good solution to this problem.

If you want to grok monads as an OCaml programmer, there is a very simple solution: do some concurrent/system programming.

Both Lwt and Async are monadic, but they are presented without requiring you to know about monads, so you can get to use them pretty easily, and after you've used them to build reasonably sized programs, then you'll have a good intuition of what's happening.

Inferring the most generic type in the presence of polymorphic recursion is not decidable. It's not that HM has a problem with it, it's just plain not possible.

OCaml and Haskell support it by requiring type annotations.

In general, polymorphic recursion is occasionally useful for some specific data structures (see Okasaki's purely functional datastructures for some examples) and when playing with GADTs.