[polyml] The History of Standard ML: Ideas, Principles, Culture