Comment by wk_end

1 year ago

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

Well if you're going to eat crow, I may as well eat pigeon, for I didn't realise that paper wasn't showing real source.

Thanks for the link to the LCF text though :^)