mlton | FStar | |
---|---|---|
9 | 42 | |
919 | 2,570 | |
1.3% | 0.6% | |
8.3 | 9.9 | |
about 1 month ago | 7 days ago | |
Standard ML | F* | |
GNU General Public License v3.0 or later | Apache License 2.0 |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
mlton
-
Flunct: Well-typed, fluent APIs in SML
https://github.com/MLton/mlton/issues/473
Is there sufficient use of MLTon "native" backend out there to consider it mature? or Do people prefer the LLVM or C backend instead in general?
-
Simple JSON parser in c++, rust, ocaml, standard ml
Once I got the parser ready in OCaml, I thought I port it to Standard ML, since it belong to the same ML language family. I was also curious on how well mlton could optimise it. The language lacks custom let bindings, so I resorted to use Result.bind manually. This makes code much less readable and more verbose. The standard library also lacks result type, so I had to come up with my own simple implementation. There's also a lack of any hash map in the standard library, so I just used a list of key-value pairs. This isn't correct, but it's the closest I could get without inventing my own hash map. MLton's compile times are slow. It also lacks interactive REPL. Because of that I used alternative Standard ML implementation for interactive usage: PolyML. Debugging MLton binaries is also pretty hard. gdb doesn't work and there's no bundled debugger. I had to resort to debugging facilities built into PolyML. Valgrind doesn't work with mlton binaries, as it doesn't report any memory allocations. Looks like mlton uses mmap for allocation memory. Surprisingly, performance is not the best. This might be due to heavy usage of my custom Result type and bind calls. Exceptions seem to be a more natural choice for error reporting in Standard ML. I tried to make such a change, but this didn't improve the performance much.
-
old languages compilers
MLton
-
Modules: Overcoming Stockholm and Duning-Kruger
Something I’d highly recommend you do before concluding that SML’s module system is the best is to go through and read the MLton Basis library. MLton uses the module system extremely heavily in its definition of the standard, and I think it’s extremely important to understand what you may be getting yourself into when you add those features, and what you may lose in return.
-
Ante: A low-level functional language
If you’re fine with tracing GC (which depends on the situation, of course), Standard ML is a perfectly boring language (that IIUC predated and inspired Caml) and MLton[1] is a very nice optimizing compiler for it. The language is awkward at times (in particular, the separate sublanguage of modules can be downright unwieldy), and the library has some of the usual blind spots such as nonexistent Unicode support (well, not every language WG is allocated a John Cowan).
Speaking of, Scheme can also be a delightful unexciting static language; consider for example the C-producing implementation Chicken[2]. The pattern-matching / algebraic-datatype story was still rather unsatisfying last I checked, but there are other situations where it shines—it’s complementary to SML in a way.
You’re not going to be writing a kernel or a real-time renderer in either (though I’m certain people have taken that as a challenge), they son’t afford the flashy EDSLs of Tcl, Ruby, or Racket, and I can’t say I can prototype in them like I do in Python or sh+tools, but there is a comfortable middle ground where they fit well. (I hear others use Go in what seem like the same places, but to me it feels so thin and devoid of joy that I can’t really compare.)
The FFI tools in both of the mentioned implementations are excellent, though not quite at the “type in C declarations” level of LuaJIT and D.
[1] http://mlton.org/
[2] https://call-cc.org/
-
Write your own programming language in an hour with Chumsky
Unfortunately, I haven't found a ton of "easily-digestible" and, at the same time, comprehensive guides on compiling functional languages. Generally you'll find a mix of blog posts/class notes/papers covering a single step.
Some resources I like:
- Andrew Kennedy's 2007 paper Compiling with Continuations, Continued [1]. This one is the most clear IMO
- Andrew Appel's Compiling with Continuations book (a bit outdated though... assembly code is for VAX)
- Matt Might's series [2]
- MLton's source and documentation [3]
[1] https://www.microsoft.com/en-us/research/wp-content/uploads/...
[2] https://matt.might.net/articles/closure-conversion/
[3] http://mlton.org/
-
Why are imperative programs considered faster than their functional counterparts?
More broadly, they can be fast even without such extensions if they aggressively pursue optimization opportunities afforded by static typing, like MLton for example, but that also impacts compilation performance negatively.
- Coalton: How to Have Our (Typed) Cake and (Safely) Eat It Too, in Common Lisp
-
Are there any efficient key-value map/dictionary implementations in SML?
https://github.com/MLton/mlton/blob/master/lib/mlton/basic/hash-set.sig https://github.com/MLton/mlton/blob/master/lib/mlton/basic/hash-table.sig
FStar
- Lean4 helped Terence Tao discover a small bug in his recent paper
-
The Deep Link Equating Math Proofs and Computer Programs
I don't think something that specific exists. There are a very large number of formal methods tools, each with different specialties / domains.
For verification with proof assistants, [Software Foundations](https://softwarefoundations.cis.upenn.edu/) and [Concrete Semantics](http://concrete-semantics.org/) are both solid.
For verification via model checking, you can check out [Learn TLA+](https://learntla.com/), and the more theoretical [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf).
For more theory, check out [Formal Reasoning About Programs](http://adam.chlipala.net/frap/).
And for general projects look at [F*](https://www.fstar-lang.org/) and [Dafny](https://dafny.org/).
-
If You've Got Enough Money, It's All 'Lawful'
Don't get me wrong, there are times when Microsoft got it right the first time that was technically far superior to their competitors. Windows IOCP was theoretically capable of doing C10K as far back in 1994-95 when there wasn't any hardware support yet and UNIX world was bickering over how to do asynchronous I/O. Years later POSIX came up with select which was a shoddy little shit in comparison. Linux caved in finally only as recently as 2019 and implemented io_uring. Microsoft research has contributed some very interesting things to computer science like Z3 SAT solver and in collaboration with INRIA made languages like F* and Low* for formal specification and verification. But all this dwarfs in comparison to all the harm they did.
-
What are the current hot topics in type theory and static analysis?
Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.
-
Why is there no simple C-like functional programming language?
F* is a dependently typed language that can be transpiled to idiomatic C via the KReMLin compiler. It’s very ML-ish to write and you can leave out some proofs. It also has the benefit of being used to write a formally verified TLS implementation that’s in wide use throughout industry.
-
[Media] Genetic algorithm simulation - Smart rockets (code link in comments)
As I said, dependent types attempt to solve this problem. F* is a language where you can express complex logic as a type. The catch is, these types are checked by an SMT solver. If the solver can satisfy the type checking, then great, and you move on. If it can’t, you have no idea why, and either have to guess or manually write the proof anyway. Contrast this with Standard ML which has a proof of the soundness of its type system.
-
Prop v0.42 released! Don't panic! The answer is... support for dependent types :)
So kind of like F*? https://www.fstar-lang.org/
-
old languages compilers
F*
-
Pegasus spyware was used to hack reporters’ phones. I’m suing its creators; When you’re infected by Pegasus, spies effectively hold a clone of your phone – we’re fighting back.
Nevermind that academia has come up with far safer ways to do a few things but social norms & inertia prevent their wider adoption (well okay, it also has a barrier to entry in the education required to use it but I don't think someone with the knowledge to meaningfully contribute to an OS kernel can be considered uneducated nor unable to learn).
-
[Hobby] Amateur Generalist Programmer Seeking to Put Bugfixing Skills to Good Use
Maybe that's a little off topic here, but if you like fixing bugs, i suspect you might also enjoy showing that there are no bugs at all. Check out languages like F* https://www.fstar-lang.org/ It's a proof-oriented programming language. You can use it to write code that has no bugs at all. And you once you're done, can convert F* to C or other languages.
What are some alternatives?
LunarML - The Standard ML compiler that produces Lua/JavaScript
coq - Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
typed-racket - Typed Racket
lean - Lean Theorem Prover
sml-parseq - parallel sequences library in Standard ML
dafny - Dafny is a verification-aware programming language
seL4 - The seL4 microkernel
koka - Koka language compiler and interpreter
futhark - :boom::computer::boom: A data-parallel functional programming language
VisualFSharp - The F# compiler, F# core library, F# language service, and F# tooling integration for Visual Studio
tao - A statically-typed functional language with generics, typeclasses, sum types, pattern-matching, first-class functions, currying, algebraic effects, associated types, good diagnostics, etc.
stepmania - Advanced rhythm game for Windows, Linux and OS X. Designed for both home and arcade use.