The definition of standard ML
by R. Milner, Robin Milner, Mads Tofte, Harper, Robert, David MacQueen · first published 1997
15mentions
1recommended by
10HN commenters
2009–2023first – last mentioned
10% recommend80% neutral10% critical
Affiliate links. As an Amazon Associate I earn from qualifying purchases.
You would aim to prove properties of the formal semantics of a language, but that requires the language be described in a formal manner. Check out "The Definition of Standard ML" to get a sense of what a (mostly kosher) formal programming language definition might look like.
on “Petalisp: Elegant High Performance Computing” ↗Eh, I think people reading Robert Harper's blog can be expected to know that Robert Harper wrote The Definition of Standard ML.
on “Haskell Is Exceptionally Unsafe ” ↗…responsible programming language designer could have taken on board ML's lessons sincen, and it's an interesting historical question why this did not happen. [1] R. Milner, M. Tofte, R. Harper, The Definition of Standard ML. http://www.lfcs.inf.ed.ac.uk/reports/88/ECS-LFCS-88-62/
on “Yes Silver Bullet (2019)” ↗Here is a paper[1] written by Andreas Rossberg, specification author of Web Assembly, that discusses the defects in the definition of Standard ML. I believe he tried to address many of these issues with Alice ML[2]. [1] https://people.mpi-sws.org/~rossberg/papers/sml-defects-2013... [2] https://github.com/aliceml/aliceml
on “Standard ML in 2020” ↗…vocal proponents.) In all fairness, the language about type systems is often impenetrably mathematical, so I'm not surprised that the parallel isn't clear. (I really like OCaml, so I tried reading _The Definition of Standard ML_ to get a better understanding of the language family. Wham, brick wall. Then again, I'm not a mathematics grad student...I studied history.) * Which is just a different way of communicating semantic…
on “Cram your test driven development up your ass” ↗Where is a good place to get started with studying formal semantics? I've tried to follow chapters about formal semantics in LiSP, TAPL, CTM, and _The Definition of Standard ML_ with varying degrees of success (the material in TDoSML was beyond me), but I'm not sure where to start. I know part of the issue is getting familiar with the dense notation. I'm gradually getting an…
on “What are the semantics of your favourite programming language?” ↗The book "The Definition of Standard ML" is ~150 pages for a language that is simple (IMO) and rich. Bonus, the definition is not written in prose, but with typing rules and operational semantics.
on “Who Says C is Simple?” ↗…with a single row[1]), and is akin to a type variable used for parametric polymorphism, such as `'a`, and, in Standard ML with eqtypes, `''a`. To the best of my knowledge, the term "row" comes from The Definition of Standard ML, where the grammar given for the core language includes productions called "TyRow", "PatRow", and "ExpRow", which correspond to the syntax of record types, patterns, and expressions, respectively, but…
on “Typed, modular macros for OCaml” ↗…terminology used is especially math-y; There are many features ML has that programmers would find tremendously useful, except they're usually discussed using Greek letters, which is insular. I got a copy of The Definition of Standard ML from Amazon, hoping to get further insight into the language's design, and found it completely impenetrable. (Then again, I'm not a grad student.) Newer languages seem to be using type inference (finally!),…
on “The speed, size and dependability of programming languages” ↗Indeed, and Lua gets a lot simpler because it can shrug stuff outside its scope onto C. (The Definition of Standard ML is also pretty short, though... ;) )
on “Graham’s Guide to Learning Scala” ↗https://github.com/SMLFamily/The-Definition-of-Standard-ML-R... in case anyone else is hitting the GoDaddy landing page...
on “Standard ML Family GitHub Project” ↗> You don't think of lists as a string of pointers when evaluating ML, No, it's not. The Definition of Standard ML says absolutely nothing about lists or strings being implemented as pointers. Lists and strings are values. > and it's the same thing. It's not. > That's not the earthshaking difference you seem to…
on “The truth about Lisp (2006)” ↗Maybe it could be ported to SML, because: > "It is distinctive among widely used languages in that it has a formal specification, given as typing rules and operational semantics in The Definition of Standard ML (1990, revised and simplified as The Definition of Standard ML (Revised) in 1997)." https://en.wikipedia.org/wiki/Standard_ML edit, the specification itself: http://sml-family.org/sml97-defn.pdf
on “F# RISC-V Instruction Set Formal Specification” ↗…requirement for a usable SML implementation -- in which case, you see, culture matters. Big integers are great help, but they aren't considered a de facto requirement. The only requirements are those in the Definition of Standard ML and the Standard ML Basis Library. As I said above, using abstract types, you can roll your own non-leaky big integer abstraction. > While language (mis)features do sometimes contribute to the difficulty…
on “Python Lists vs. Tuples” ↗…closely as possible the actual working of the interpreter and PROG feature. (It turns out to be possible to get an even closer description with a formal notation for the semantics, as was done with the definition of Standard ML, but such formalism has yet to catch on). This emphasis on the importance of notation for the exact expression of thoughts and precice description of “ideal objects” is not particularly new, and it certainly…
on “Clear is better than clever” ↗