7 ms·

This is why we don't microbenchmark languages. Usually if you dig a little deeper, you find that actually the difference between the languages is mostly just th

by CHY872 11y ago

This is why we don't microbenchmark languages. Usually if you dig a little deeper, you find that actually the difference between the languages is mostly just that one of them does one thing badly. This by the way is MLton's worst case scenario. MLton is designed to perform full-program optimisation (unlike almost any other compiler I've seen); the gap is supposed to grow as the code gets larger (read: more realistic). Sadly due to its design tradeoffs (it's a compiler) it's totally unsuitable for the big ML projects (interactive theorem provers).

jasperry 11y ago
Can you elaborate on why being a compiler makes MLton unsuitable for theorem provers? Is it because they are usually written on top of the interpreter's REPL, and need its reflection capabilities?
- loup-vaillant 11y ago
  I'm guessing it's the significant compilation times required by whole program optimisations. MLton doesn't do separate compilation. (I think. Citation needed. It may separate some things, then optimise after, GCC -flto style.)
- CHY872 11y ago
  It's because they use metaprogramming so extensively. As an example, HOL4 (I can only speak for that) accepts a script written by the user (as though in a REPL), compiles and runs it, and produces an sml theory file which represents their defined theory [0]. The user when they start their next theory are supposed to use this computer generated code. You would have to write your own repl, write your own way of loading, writing theories etc and by that time you've lost performance (HOL even after 20 years of progress and tweaks now has only mostly ok performance). So it would at least require some rearchitecting, which is my point; it's not a drop in replacement. [0] - This is AES, before and after building! https://gist.github.com/j-baker/244ef3e59f19d74c352b https://gist.github.com/j-baker/244ef3e59f19d74c352b
  - jasperry 11y ago
    That makes sense. It's pretty cool to think that ML was designed as a metalanguage for theorem provers, and the innovations required for that turned out to be the next step (or next several steps) in the evolution of general-purpose languages.
- more_original 11y ago
  MLton is unsuitable for LCF-style theorem provers, simply because it has no interactive toplevel. ML was originally developed as a MetaLanguage for such theorem provers. The idea is to have an abstract type thm of theorems, whose operations (like modus ponens) only allow you to construct provable theorems. To prove a theorem interactively, you would start the ML toplevel and try to construct a proof of your proposition by programming in ML. The ML type system guarantees that you can only prove valid things. The toplevel is essential if you want to prove things interactively. Modern theorem provers like Coq work differently. If Coq were written in SML rather than OCaml, then MLton should be good for Coq as well. I think people have experimented with non-interactive versions of HOL4, compiled using MLton (because it's faster than other SML compilers).
  - CHY872 11y ago
    Slight correction. LCF-style provers do not use the Curry-Howard correspondance (ML's type system is not strong enough); having something of type thm is not enough to know that it's a theorem. The type thm is just a triple of tag (to store any oracles etc), a list of assumptions and a conclusion. The main way that you prevent against fake theorems being constructed is to (I think) make the constructor private, and then have combinator functions that you've very carefully verified. You can certainly use mk_thm to make a theorem of whatever you want (it adds an oracle tag, but a single line change in Thm.sml would drop that). MLton would require you to write your own metalanguage (but this is not necessarily onerous; most Isabelle is written in thy files or Isar. I had a think about it, and I think that the actual compelling advantage of Poly is probably its saveable heaps; they really make everything a lot faster. The whole language is a bit janky though; there's a tonne of stuff totally unstandardized (production of executables, imports etc), which means that every compiler has fairly dramatic extensions (and hilariously you can't tell between them by attempting to use them because of the type system). So HOL4 will try to determine whether you're using mosml or polyml by calculating factorial 100. With mosml you overflow, polyml seamlessly switches to a bignum. tl;dr Coq implements a metalanguage on top of ML (with an undecidable type system). LCF type provers use ML as their metalanguage. Using mlton would force you to write your own metalanguage because it has no interactivity.
dman 11y ago
You might want to check out Stalin. (http://en.wikipedia.org/wiki/Stalin_%28Scheme_implementation%29 http://en.wikipedia.org/wiki/Stalin_%28Scheme_implementation...)

by CHY872 11y ago

jasperry 11y ago

Can you elaborate on why being a compiler makes MLton unsuitable for theorem provers? Is it because they are usually written on top of the interpreter's REPL, and need its reflection capabilities?

loup-vaillant 11y ago
I'm guessing it's the significant compilation times required by whole program optimisations. MLton doesn't do separate compilation. (I think. Citation needed. It may separate some things, then optimise after, GCC -flto style.)
CHY872 11y ago
It's because they use metaprogramming so extensively. As an example, HOL4 (I can only speak for that) accepts a script written by the user (as though in a REPL), compiles and runs it, and produces an sml theory file which represents their defined theory [0]. The user when they start their next theory are supposed to use this computer generated code. You would have to write your own repl, write your own way of loading, writing theories etc and by that time you've lost performance (HOL even after 20 years of progress and tweaks now has only mostly ok performance). So it would at least require some rearchitecting, which is my point; it's not a drop in replacement. [0] - This is AES, before and after building! https://gist.github.com/j-baker/244ef3e59f19d74c352b https://gist.github.com/j-baker/244ef3e59f19d74c352b
- jasperry 11y ago
  That makes sense. It's pretty cool to think that ML was designed as a metalanguage for theorem provers, and the innovations required for that turned out to be the next step (or next several steps) in the evolution of general-purpose languages.
more_original 11y ago
MLton is unsuitable for LCF-style theorem provers, simply because it has no interactive toplevel. ML was originally developed as a MetaLanguage for such theorem provers. The idea is to have an abstract type thm of theorems, whose operations (like modus ponens) only allow you to construct provable theorems. To prove a theorem interactively, you would start the ML toplevel and try to construct a proof of your proposition by programming in ML. The ML type system guarantees that you can only prove valid things. The toplevel is essential if you want to prove things interactively. Modern theorem provers like Coq work differently. If Coq were written in SML rather than OCaml, then MLton should be good for Coq as well. I think people have experimented with non-interactive versions of HOL4, compiled using MLton (because it's faster than other SML compilers).
- CHY872 11y ago
  Slight correction. LCF-style provers do not use the Curry-Howard correspondance (ML's type system is not strong enough); having something of type thm is not enough to know that it's a theorem. The type thm is just a triple of tag (to store any oracles etc), a list of assumptions and a conclusion. The main way that you prevent against fake theorems being constructed is to (I think) make the constructor private, and then have combinator functions that you've very carefully verified. You can certainly use mk_thm to make a theorem of whatever you want (it adds an oracle tag, but a single line change in Thm.sml would drop that). MLton would require you to write your own metalanguage (but this is not necessarily onerous; most Isabelle is written in thy files or Isar. I had a think about it, and I think that the actual compelling advantage of Poly is probably its saveable heaps; they really make everything a lot faster. The whole language is a bit janky though; there's a tonne of stuff totally unstandardized (production of executables, imports etc), which means that every compiler has fairly dramatic extensions (and hilariously you can't tell between them by attempting to use them because of the type system). So HOL4 will try to determine whether you're using mosml or polyml by calculating factorial 100. With mosml you overflow, polyml seamlessly switches to a bignum. tl;dr Coq implements a metalanguage on top of ML (with an undecidable type system). LCF type provers use ML as their metalanguage. Using mlton would force you to write your own metalanguage because it has no interactivity.

dman 11y ago

You might want to check out Stalin. (http://en.wikipedia.org/wiki/Stalin_%28Scheme_implementation%29 http://en.wikipedia.org/wiki/Stalin_%28Scheme_implementation...)