[HN Gopher] Memories: Edinburgh ML to Standard ML
___________________________________________________________________
Memories: Edinburgh ML to Standard ML
Author : todsacerdoti
Score : 87 points
Date : 2022-10-05 14:57 UTC (8 hours ago)
(HTM) web link (lawrencecpaulson.github.io)
(TXT) w3m dump (lawrencecpaulson.github.io)
| devmunchies wrote:
| I _REALLY_ want to use a native ML language[1] but they all seem
| to be catered towards academics.
|
| If you want success within companies and not universities, then
| you need to treat the language as a product, serve the customer
| by investing time into documentation, guides, and branding just
| like with any product. I say this as a fan of ML languages, posts
| that complain about another language (OCaml) being more popular
| even though it is an inferior doesn't get new users.
|
| [1]: I currently use F# daily but would be happy to switch to a
| variant of SML if it made sense.
| 3836293648 wrote:
| I thought F# was native these days?
| mhd wrote:
| I understand the need for good documentation and tooling, but
| "languages as a product" are one of the more horrible aspects
| of the current dev environment. First of all, this mostly means
| that compiler and language are the same product. Second, it
| leads to the release early/often dev cycle which seems ill-
| suited to a language and its core library (remember core
| libraries?).
|
| And language "branding"? What are we talking about here? TIOBE-
| SEO? Cute logos? Cute in-group names ("pythonist", "rustacean",
| "gopher" ...)
|
| By the way, wasn't there a "ML for the Working Programmer"
| aeons ago?
| cannam wrote:
| > By the way, wasn't there a "ML for the Working Programmer"
| aeons ago?
|
| There was. It was written by the author of this very
| submission and you can download it free from his site (follow
| the link trail from author's name at the bottom of the
| article). Great book, a real favourite, though I'm not sure
| it totally captures the anxiety-driven copy-paste frenzy of
| the true working programmer.
|
| There is one SML compiler that has an extremely cute logo -
| SML# (https://smlsharp.github.io/en/)
| gorgoiler wrote:
| In the late 90s, for me and a bunch of people here I'm guessing,
| Larry Paulson's course on ML was the first time any of us had
| written a computer program. Certainly our first introduction to
| the theories of computation.
|
| I feel very lucky to have been in the right place at the right
| time, and ML's structure was a pleasure then as it is now. The
| history of the language is indeed rather interesting.
| eatonphil wrote:
| The section on team size and funding w.r.t. Poly/ML, SML/NJ and
| OCaml is something.
|
| Regarding Poly/ML (I'm quoting): * good
| performance and fantastic debugging tools * not merely
| "saving an image", but sharable executable units, either
| including the Read-Eval-Print loop or standalone; * support
| for one hardware architecture after another (including Apple
| Silicon) * support for multi-threading (also here); they
| say that OCaml is finally catching up, 15 years later, thanks to
| having 100 times as much funding.
|
| And:
|
| > A mystery I shall never understand is the difference in
| performance between SML/NJ and Poly/ML. The former enjoyed vastly
| greater funding and had a strong team of developers compared with
| DCJM's one-man show. Benchmarks I ran for my ML book consistently
| gave SML/NJ a big performance advantage. But with Isabelle, the
| strong performer was Poly/ML. Once David got parallelism working,
| Poly/ML's advantage was so overwhelming that we dropped our long-
| standing policy of supporting both compilers.
| frou_dh wrote:
| As much of a gem as Poly/ML might be, I just use MLton*
| exclusively, because its .mlb aka MLBasis build-system seems by
| far the most sane way to actually make use of multiple source
| files when writing SML code.
|
| *another gem
| shwestrick wrote:
| MLton also has perhaps the most impressive performance of any
| existing functional language implementation. It generates
| code that easily competes with hand-optimized low-level
| C/C++/whatever.
| cannam wrote:
| MLton can't do SIMD auto-vectorisation, which unfortunately
| gives it a ceiling significantly below C++ compilers for
| the sort of thing I do. I generally use FFI calls for
| chunky, frequently-used vector stuff. It's a good compiler
| generally.
| cannam wrote:
| I also use .mlb files exclusively and agree with your general
| point - but I do make use of Poly/ML and occasionally SML/NJ
| against the same sources, using scripts to drive them from
| .mlb files: https://github.com/cannam/sml-buildscripts
|
| These scripts are really limited. They only support the
| simplest .mlb files that are really just lists of other
| files, and the semantics are technically incorrect because
| they have no way to reset the environment when beginning each
| new .mlb file in, as the spec says they should. I use them
| scrappily during development and then generally use MLton for
| production builds. But you can get quite a lot done within
| those limitations, and it's very nice to have the faster
| compilation of Poly/ML, as well as the option of seeing error
| messages from more than one compiler.
| ratmice wrote:
| I have always done the opposite using SML/NJ's
| CompilationManager, then deriving mlb with cm2mlb -D MLton
| (in the mlton repo), with mlton specific code then wrapped
| in #if (defined(MLton)).
|
| That you can use CM as a library has always been really
| handy, but otherwise the same, using MLton for production
| builds.
| frou_dh wrote:
| And you offer a nice selection of SML libraries on your
| GitHub https://github.com/cannam?tab=repositories&type=sour
| ce&langu... - Thanks for that!
| azdavis wrote:
| I've been working on a language server for Standard ML called
| Millet: https://azdavis.net/posts/millet/
|
| There was some past discussion about it on HN:
| https://news.ycombinator.com/item?id=32512715
|
| For my part, I think it's unfortunate that virtually no
| mainstream language has a formal semantics in the style of SML's
| Definition. I wrote a bit about formal programming language
| semantics in a series of posts: https://azdavis.net/posts/define-
| pl-01/
| zasdffaa wrote:
| I've had a quick look over your posts, and I will look over the
| more carefully as a refresher on these kinds of things (I have
| looked at Hoare logic which this resembles, and a couple of
| other related things). The problem is to me, the formal
| semantics aren't actually very different from what you would
| write in English, and the real problem, and this is never
| addressed, how do I use this (which includes: how do I
| manipulate these things symbolically to some useful end)? The
| reason I don't get more deeply stuck into these formal
| semantics is because they seem to have no way for me to
| actually do anything useful with them. This lack of a 'bridge'
| is a huge problem to me because I can't justify learning that
| which appears of no use.
|
| Any comments appreciated, and don't be put off by the negative
| tone of this, it's just frustration.
| azdavis wrote:
| The biggest reason why you'd want a formal semantics for your
| PL, as opposed to just a "human" language specification, is
| so that you can do proofs about the formal semantics. You can
| prove your PL, as defined, satisfies certain "safety"
| properties. And the point of doing these proofs is is to
| check that the definition of the PL "makes sense".
|
| PLs that don't have a formal semantics (aka, most mainstream
| PLs) are more likely to be in situations where implementors
| realize, after the standard has been written, that e.g. some
| of the PL's features interact in a way that doesn't make
| sense, such as this example with C++ coroutines and lambdas:
| https://news.ycombinator.com/item?id=33084431
|
| Two of the most common safety properties of interest are
| progress and preservation. (I touched on this in the last
| above linked post near the bottom.) At a high level:
|
| 1. Progress states that if you have a program that type-
| checks, then either that program is "done" or it can continue
| evaluating.
|
| 2. Preservation states that if you have a program that type-
| checks _and_ that can continue evaluating, then _as_ it
| continues to evaluate, it _continues_ to type-check.
|
| Note that the conclusion of preservation "feeds back" into
| progress: the program type-checks. And vice versa: progress
| may state as its conclusion that the program can continue
| evaluating, which then lets you apply preservation. This
| means you can keep applying the progress and preservation
| theorems in a "loop" until the program is done evaluating.
|
| For each of the 4 posts in my series about formal semantics,
| I duly translated the rules presented in the blog post into
| Lean code, and then proved that the rules do satisfy the
| safety properties. For example, for the first post linked
| above:
|
| - The syntax of the language: https://github.com/azdavis/hats
| ugen/blob/part-01/src/syntax....
|
| - The static semantics (the "typechecker"): https://github.co
| m/azdavis/hatsugen/blob/part-01/src/statics...
|
| - The dynamic semantics (the "runtime"): https://github.com/a
| zdavis/hatsugen/blob/part-01/src/dynamic...
|
| - The proofs of safety: https://github.com/azdavis/hatsugen/b
| lob/part-01/src/safety....
| deltasepsilon wrote:
| > It's sad that well into the 21st Century, Computer Science has
| so regressed that people no longer see the point of
| distinguishing between a programming language and its
| implementation.
|
| Amen. I guarantee that Rust will regret not addressing this
| sooner. It's mature enough now that defining a semantics is more
| than appropriate.
| isomorph wrote:
| The author is Larry Paulson - my (and I'm sure many others' on
| HN) Foundations of Computer Science lecturer at Cambridge back in
| 2009. I wonder if I still have a little credit at the front of
| the lecture notes (for spotting some typo or other). It's
| foreboding to see him writing up his "memories" like this. Being
| woken up into the world of functional programming (via Moscow ML)
| - after learning to code as a kid in JavaScript and Visual Basic
| 6 - was priceless. And in a way it led to my fascination with
| Scala, which has made the transition to Swift much easier.
| hanoz wrote:
| Still have my copy of ML for the Working Programmer, my one
| surviving book from back in the day (early 90s in my case).
|
| Being hit with all that stuff from day one, fresh from a
| childhood of Spectrum Basic and Turbo Pascal, was a real shock
| to the system.
|
| Still don't understand most of it to be honest, but it does
| still jar when I see the initialism used to mean machine
| learning.
| choeger wrote:
| agumonkey wrote:
| Timely topic, I was asking on a lisp/plt discord if there was a
| lineage between FP/algebraic types and lisp structural thinking
| (patterns of nested lists of symbols representing and/or) with
| destructuring bind.
|
| I see a big parallel between function to turn params into structs
| and accessors, both being mirrors of each others (cons/car/cdr as
| the root example) and the fact that a type definition encodes
| enough information to generate both at the semantic layer, with
| pattern matching as sugar.
|
| So if any early LCF team member can shed some light if I'm
| imagining things or if LCF/ML were a rewrite of older recursive
| lisp practices into a cleaner formalism, I'd be glad.
|
| ps: the fact that some LCF impl. were done in lisp also
| reinforces my belief.
___________________________________________________________________
(page generated 2022-10-05 23:00 UTC)