LCF77

That paper isn't showing real ML syntax itself; it's a mathematical presentation to demonstrate how the type system algorithm works. The actual original LCF/ML syntax would differ. I don't believe it used an actual lambda character, although for the life of me I can't find any evidence one way or another, not even in the LCF source code (https://github.com/theoremprover-museum/LCF77) But yes, the slash is just an ASCII stand-in for a lambda. ETA: I tracked down a copy of the Edinburgh LCF text and I have to eat crow. It doesn't use a lambda, but it does use a slash rather than a reserved word. The syntax, per page 22, is in fact, `\x. e`. Similar to Haskell's, but with a dot instead of an arrow. https://archive.org/details/edinburghlcfmech0000gord

The original ML language (the one produced as part of the LCF theorem prover), did have a `where` clause that works like the one in Haskell. See here for example: https://github.com/theoremprover-museum/LCF77/blob/master/sr... A brief skim over the revised definition of Standard ML indicates that it was abandoned at some point. I've no idea if Caml or OCaml kept it. That said, I'm reasonably sure that the syntactic construct (insofar is it is used in programming languages) originated with the ISWIM introduced in this paper, which was rather influential in its day, perhaps especially in the functional programming community.

The original ML was implemented in Lisp (Stanford Lisp) as part of the Edinburgh LCF (Logic for Computable Functions) theorem prover. Different syntax, types - but other stuff it had were easily shared in the implementation with the underlying Lisp: functions, higher-order functions, garbage collection, lists (with cons and append operators), lambda expressions, ... Here is a version of LCF with that first ML from 1977: https://github.com/theoremprover-museum/LCF77

And ML was originally written in Lisp. https://github.com/theoremprover-museum/LCF77/tree/master/sr... https://github.com/theoremprover-museum/HOL88/tree/master/sr...