4 ms·

> Caml Light, Standard ML, pure lambda calculus The first two being based lisp, and the third being what inspired lisp. It's like saying: I learned low level

> Caml Light, Standard ML, pure lambda calculus The first two being based lisp, and the third being what inspired lisp. It's like saying: I learned low level imperative programming from using Go, C++, and register machines. Which, sure, but the C language was hugely influential to all of that.

kristianp 9y ago
>The first two being based lisp Really?
pjmlp 9y ago
What does ML, initially developed for theorem proving, have to do with Lisp?
- SolarNet 9y ago
  Because lisp is good at anything? But especially alternative evaluation systems (of which theorem proving is one). Because they took lisp and added types to it; via the ISWIM language document ("The Next 700 Programming Languages") which was based off of the original lisp. Because the lisp language family is a formulation of lambda calculus and has first class functions, unlike any other language family at the time, and that is necessary for theorem proving that is based on lambda calculus. Because they likely prototyped the system in a set of lisp macros before writing the language (all the authors knew lisp and had taught each other it).
  - pjmlp 9y ago
    Can you point me to a good reference paper about this?
    - SolarNet 9y ago
      No one has really written a paper about the history of all this (I also mentioned this paper [1] in one of my other comments). But if you read the original ML paper [0] you'll see how they developed the language (notably by using ISWIM's syntax as a base). Note also that they are solving a problem with LISP (and dismissing Algol languages entirely) by building in strong types. [0] http://www.sciencedirect.com/science/article/pii/0022000078900144 http://www.sciencedirect.com/science/article/pii/00220000789... [1] https://archive.alvb.in/msc/11_infomtpt/papers/the-next-700_Landin_dk.pdf https://archive.alvb.in/msc/11_infomtpt/papers/the-next-700_...

kristianp 9y ago

>The first two being based lisp Really?

pjmlp 9y ago

What does ML, initially developed for theorem proving, have to do with Lisp?

SolarNet 9y ago
Because lisp is good at anything? But especially alternative evaluation systems (of which theorem proving is one). Because they took lisp and added types to it; via the ISWIM language document ("The Next 700 Programming Languages") which was based off of the original lisp. Because the lisp language family is a formulation of lambda calculus and has first class functions, unlike any other language family at the time, and that is necessary for theorem proving that is based on lambda calculus. Because they likely prototyped the system in a set of lisp macros before writing the language (all the authors knew lisp and had taught each other it).
- pjmlp 9y ago
  Can you point me to a good reference paper about this?
  - SolarNet 9y ago
    No one has really written a paper about the history of all this (I also mentioned this paper [1] in one of my other comments). But if you read the original ML paper [0] you'll see how they developed the language (notably by using ISWIM's syntax as a base). Note also that they are solving a problem with LISP (and dismissing Algol languages entirely) by building in strong types. [0] http://www.sciencedirect.com/science/article/pii/0022000078900144 http://www.sciencedirect.com/science/article/pii/00220000789... [1] https://archive.alvb.in/msc/11_infomtpt/papers/the-next-700_Landin_dk.pdf https://archive.alvb.in/msc/11_infomtpt/papers/the-next-700_...