home *** CD-ROM | disk | FTP | other *** search
/ ftp.pasteur.org/FAQ/ / ftp-pasteur-org-FAQ.zip / FAQ / meta-lang-faq < prev    next >
Encoding:
Internet Message Format  |  2003-03-21  |  56.8 KB

  1. Path: senator-bedfellow.mit.edu!bloom-beacon.mit.edu!newsfeed.utk.edu!elk.ncren.net!arclight.uoregon.edu!newsfeed.srv.cs.cmu.edu!wolfberry.srv.cs.cmu.edu!leaf
  2. From: leaf@cs.cmu.edu (Leaf Eames Petersen)
  3. Newsgroups: comp.lang.ml,comp.answers,news.answers
  4. Subject: Comp.Lang.ML FAQ [Monthly Posting]
  5. Followup-To: poster
  6. Date: Thu, 20 Mar 2003 20:30:14 +0000 (UTC)
  7. Organization: Carnegie Mellon Univ. -- Computer Science Dept.
  8. Lines: 1492
  9. Sender: leaf@cs.cmu.edu
  10. Approved: comp-lang-ml@cs.cmu.edu
  11. Expires: Sun, 04 May 2003 00:00:00 GMT
  12. Message-ID: <b5d8cm$gdp$1@wolfberry.srv.cs.cmu.edu>
  13. Reply-To: comp-lang-ml-request@cs.cmu.edu
  14. NNTP-Posting-Host: kazoo.concert.cs.cmu.edu
  15. X-Trace: wolfberry.srv.cs.cmu.edu 1048192214 16825 128.2.181.69 (20 Mar 2003 20:30:14 GMT)
  16. X-Complaints-To: abuse@cs.cmu.edu
  17. NNTP-Posting-Date: Thu, 20 Mar 2003 20:30:14 +0000 (UTC)
  18. Summary: This posting contains a list of Frequently asked questions (and their
  19.          answers) about the family of ML programming languages, including 
  20.          Standard ML, CAML, Lazy-ML, and CAML-Light.  This post should be read 
  21.          before asking a question on the comp.lang.ml newsgroup.
  22. Xref: senator-bedfellow.mit.edu comp.lang.ml:5780 comp.answers:53191 news.answers:248376
  23.  
  24. Archive-name: meta-lang-faq
  25. Last-modified: Mar 20, 2003
  26.     
  27.  
  28.          COMP.LANG.ML Frequently Asked Questions and Answers 
  29.        (compiled by Dave Berry, Greg Morrisett and Rowan Davies)
  30.            (maintained by Leaf Petersen) 
  31.  
  32. Please send corrections, additions, or comments regarding this list to
  33. comp-lang-ml-request@cs.cmu.edu.  
  34.  
  35. Changes since last posting:
  36.     - Added question on OCaml/SML comparison (Andreas Rossberg)
  37.     - Updated ProofPower entry (Rob Arthan)
  38.     - Changed link for Elementary Standard ML (Greg Michaelson)
  39.     - Updated MLton entry (Stephen Weeks)    
  40.     - Added entry on HaMLet (Andreas Rossberg)
  41.     - Updated basis entry (Andreas Rossberg)
  42.     - Added SML.Net (Andreas Rossberg)
  43.  
  44. Contents:
  45. ---------
  46.     1. What is ML?
  47.     2. Where is ML discussed?
  48.         a. Comp.Lang.ML
  49.         b. SML-LIST
  50.         c. CAML-LIST
  51.     3. What implementations of ML are available?
  52.         a. quick summary (by machine/OS)
  53.          b. Standard ML of New Jersey (SML/NJ)
  54.         c. sml2c
  55.         d. Caml Light
  56.                 e. Objective Caml
  57.                 f. Bigloo
  58.                 g. Camlot
  59.         h. Moscow ML
  60.         i. ML Kit
  61.                 j. Edinburgh
  62.         k. MicroML
  63.         l. Poly/ML
  64.         m. Poplog ML
  65.                 n. MLWorks
  66.                 o. MLJ
  67.                 p. MLton
  68.         q. HaMLet
  69.         4. Unsupported SML/NJ Ports
  70.         a. OS/2
  71.         b. NEXTSTEP
  72.          c. SVR4
  73.         5. Where can I find documentation/information on ML?
  74.         a. The Definition
  75.         b. Textbooks
  76.         c. Information on the Internet
  77.     6. Where can I find ML library code?
  78.                 a. The Standard ML ('97) Basis Library
  79.         b. The Edinburgh SML Library
  80.         c. The SML/NJ Library
  81.         d. SML_TK
  82.                 e. Caml-light libraries
  83.         f. The Qwertz Toolbox (for AI)
  84.     7. Theorem Provers and ML
  85.         8. Miscellaneous Questions
  86.         a. How do I write the Y combinator in SML?
  87.         b. Where can I find an X-windows interface to SML?
  88.         c. How do I call a C function from SML/NJ?
  89.         d. Where can I find an emacs mode for SML?
  90.         e. What is the value restriction?
  91.         f. What is the difference between OCaml and Standard ML?
  92.  
  93. --------------------------------------------------------------------------
  94.  
  95. 0. Where can I find the latest copy of this FAQ?
  96.  
  97.   This document can be retrieved via anonymous ftp from
  98.     ftp://pop.cs.cmu.edu/usr/rowan/sml-archive/faq.txt
  99.   or from rtfm.mit.edu.  There is an HTTP version with active links at
  100.     http://www.cis.ohio-state.edu/hypertext/faq/usenet/meta-lang-faq/faq.html
  101.  
  102. --------------------------------------------------------------------------
  103.  
  104. 1. What is ML?
  105.  
  106.   ML (which stands for Meta-Language) is a family of advanced programming 
  107.   languages with [usually] functional control structures, strict semantics, 
  108.   a strict polymorphic type system, and parametrized modules.  It includes 
  109.   Standard ML, Lazy ML, CAML, CAML Light, and various research languages.  
  110.   Implementations are available on many platforms, including PCs, mainframes,
  111.   most models of workstation, multi-processors and supercomputers.  ML has 
  112.   many thousands of users, is taught at many universities (and is the first
  113.   programming language taught at some).
  114.  
  115. --------------------------------------------------------------------------
  116.  
  117. 2. Where is ML discussed?
  118.  
  119. COMP.LANG.ML
  120. ------------
  121. comp.lang.ml is a moderated usenet newsgroup.  The topics for discussion
  122. include but are not limited to:
  123.  
  124.    * general ML enquiries or discussion 
  125.    * general interpretation of the definition of Standard ML 
  126.    * applications and use of ML 
  127.    * announcements of general interest (e.g. compiler releases)
  128.    * discussion of semantics including sematics of extensions based on ML
  129.    * discussion about library structure and content
  130.    * tool development
  131.    * comparison/contrast with other languages
  132.    * implementation issues, techniques and algorithms including extensions
  133.      based on ML
  134.  
  135. Requests should be sent to:
  136.  
  137.     comp-lang-ml@cs.cmu.edu
  138.  
  139. Administrative mail should be sent to:
  140.  
  141.     comp-lang-ml-request@cs.cmu.edu
  142.  
  143. Messages sent to the newsgroup are archived at CMU.  The archives can be
  144. retrieved by anonymous ftp from internet sites.  Messages are archived
  145. on a year-to-year basis.  Previous years' messages are compressed using
  146. the Unix "compress" command.  The current year's messages are not
  147. compressed.
  148.  
  149.     ftp pop.cs.cmu.edu
  150.     username: anonymous
  151.     password: <username>@<site>
  152.     binary
  153.     cd /usr/rowan/sml-archive
  154.     get sml-archive.<year>.Z
  155.     quit
  156.     zcat sml-archive.<year>.Z
  157.  
  158. (Pop's IP address is 128.2.205.205).
  159.  
  160. Individual messages can also be accessed in the directories
  161. /usr/rowan/mh-sml-archive/<year>-sml.
  162.  
  163. SML-LIST
  164. --------
  165. The SML-LIST is a mailing list that exists for people who cannot
  166. (or do not want to) read the Usenet COMP.LANG.ML newsgroup. 
  167. Messages are crossposted from COMP.LANG.ML to the SML-LIST and
  168. vice-versa.  You should ask to join the SML-LIST _only if_ you cannot
  169. (or do not want to) read the Usenet COMP.LANG.ML newsgroup.
  170.  
  171. To send a message to the SML-LIST distribution, address it to:
  172.  
  173.     sml-list@cs.cmu.edu
  174.  
  175. (sites not connected to the Internet may need additional routing.)
  176.  
  177. Administrative mail such as requests to add or remove names from the
  178. distribution list should be addressed to 
  179.  
  180.     sml-list-request@cs.cmu.edu
  181.  
  182.  
  183. CAML-LIST
  184. ---------
  185. The Caml language, a dialect of ML, is discussed on the Caml mailing
  186. list.  To send mail to the Caml mailing list, address it to:
  187.  
  188.     caml-list@inria.fr
  189.  
  190. Administrative mail should be addressed to:
  191.  
  192.     caml-list-request@inria.fr
  193.  
  194. ALT.LANG.ML
  195. -----------
  196. No longer used.
  197.  
  198. --------------------------------------------------------------------------
  199.  
  200. 3. What implementations of ML are available and where can I find them?
  201.  
  202.  
  203. Quick Summary:
  204.  
  205. System    full SML?  contact                        Platforms
  206. ------    ---------  ------------                 ------------------------------
  207. SML/NJ       yes     sml-nj@research.bell-labs.com 
  208.       SML'97       http://cm.bell-labs.com/cm/cs/what/smlnj
  209.  
  210.                         Alpha - OSF/1 3.2, DUX 4.0
  211.                         Mips - Irix 4.0.x, 5.x, 6.x
  212.                         x86 - Linux, Solaris, FreeBSD, 
  213.                           NetBSD, Windows95, WindowsNT    
  214.                         Sparc - SunOS, Solaris
  215.                         RS/6000 - AIX
  216.                         PowerPC - AIX
  217.                         HPPA - HPUX 10
  218.  
  219. sml2c       yes                     32-bit Unix machines (C code)
  220.            http://www.funet.fi/pub/languages/ml/sml2c/
  221.  
  222.  
  223. Caml Light coreish caml-light@inria.fr         Unix, Mac, PC 80386,
  224.            ftp ftp.inria.fr         (bytecode)
  225.  
  226. Objective  own     caml-light@inria.fr         Unix and Windows NT/95
  227.   Caml    modules  ftp ftp.inria.fr              (bytecode)
  228.                                                  Alpha, Sparc, x86, Mips,
  229.                                                  HPPA, Power (native code)
  230.  
  231. Bigloo    coreish  Manuel.Serrano@inria.fr.      Unix (compiles caml-light 
  232.                    ftp ftp.inria.fr                    to native code)
  233.  
  234. Camlot    coreish  Regis.Cridlig@ens.fr          Any 32-bit (compiles
  235.                    ftp ftp.inria.fr                    caml-light to C)
  236.  
  237. Moscow ML  yes       sestoft@dina.kvl.dk         
  238.        SML'97  http://www.dina.kvl.dk/~sestoft/mosml.html
  239.  
  240.                         Intel- Windows,OS/2,Linux,FreeBSD
  241.                         Alpha - DUX
  242.                         Sparc - Solaris,SunOS
  243.                         HP9000 - UX 9,UX 10
  244.                         SGI MIPS - IRIX 5
  245.                         Mac(68k and PPC) 
  246.                           - MacOS,MkLinux,
  247.                             MacOS X
  248.  
  249. Kit       yes       ftp ftp.diku.dk         (Requires another SML compiler
  250.            ftp ftp.dcs.ed.ac.uk         to build binaries)
  251.  
  252. Edinburgh  core       ftp.dcs.ed.ac.uk             32-bit machines (bytecode)
  253.            ftp.informatik.uni-muenchen.de  PC 80386SX+, Amiga
  254.  
  255. MicroML    core    Olof.Johansson@cs.umu.se      PC 8086+ (bytecode)
  256.            ftp ftp.cs.umu.se
  257.  
  258. Poly/ML       SML 97  http://www.polyml.org         Intel - Linux, Windows
  259.                          Sparc - Solaris
  260.                          Mac   - MacOS X
  261.  
  262. PoplogML   yes     isl@isl.co.uk                 Sparc/Solaris, Intel/Solaris,
  263.                                                  Intel/Linux, PowerPC/AIX,
  264.                                                  Alpha/DUX, Intel/Windows
  265.  
  266. MLWorks    No longer available
  267.  
  268. MLJ        core+  mlj@dcs.ed.ac.uk         Unix and Windows NT/95
  269.            SML'97                                Alpha, Sparc, x86
  270.                    http://www.dcs.ed.ac.uk/~mlj/    (Compiles to JVM)
  271.  
  272. MLton      yes     MLton@mlton.org                  x86 Linux, FreeBSD, Cygwin
  273.          SML'97    http://www.mlton.org
  274.  
  275. HaMLet     yes     http://www.ps.uni-sb.de/hamlet/  N/A
  276.  
  277. SML.NET    yes     http://www.cl.cam.ac.uk/Research/TSG/SMLNET/
  278.                              (Targets the Common Language Runtime)
  279.  
  280. Details:
  281.  
  282. Standard ML of New Jersey
  283. ------------------------
  284. Standard ML of New Jersey (SML/NJ) was developed jointly at Bell
  285. Laboratories, Princeton University, and recently Yale University.  The
  286. SML/NJ distribution includes CM (a separate compilation manager),
  287. ML-Yacc, ML-Lex, ML-Burg, the SML/NJ Library, Concurrent ML, eXene
  288. (a multithreaded X-windows toolkit), and the SML/NJ-C interface
  289. library.  The software is available with source code under a very
  290. liberal license.
  291.  
  292. Version 110 of SML/NJ (released in February 1998), is largely
  293. compliant with the new SML '97 Definition, including the new Basis
  294. library.
  295.  
  296. Version 110 runs on the following machine/os configurations:
  297.  
  298.     Alpha    OSF/1 3.2, Digital Unix 4.0
  299.     Mips    Irix 4.0.x, Irix 5.x, Irix 6.x
  300.     x86        Linux, Solaris, FreeBSD, NetBSD, Windows95, WindowsNT
  301.     Sparc    SunOS, Solaris
  302.     RS/6000    AIX (also PowerPC)
  303.     HPPA    HPUX 10
  304.  
  305. For the time being, Macintosh users will have to stick with the
  306. previous release, Version 0.93.  New ports to MacOS and Rhapsody on
  307. PowerPC are planned, and there may also be support for BeOS on PowerPC
  308. and Intel.
  309.  
  310. The SML/NJ Version 110 software distribution is available at:
  311.  
  312.     Bell Labs:  ftp://ftp.research.bell-labs.com/dist/smlnj/release/110/
  313.     Stanford:   ftp://rodin.stanford.edu/pub/smlnj/release/110/
  314.     DIKU:       ftp://ftp.diku.dk/pub/smlnj/release/110/
  315.     Cambridge:  ftp://ftp.cl.cam.ac.uk/MIRRORED/smlnj/release/110/
  316.  
  317. or through the SML/NJ web site at:
  318.  
  319.     http://cm.bell-labs.com/cm/cs/what/smlnj
  320.  
  321. This web site also has extensive online documentation and links to
  322. related sites.
  323.  
  324. Another important link is the documentation for the SML '97 Basis, which
  325. can be found at:
  326.  
  327.    http://SML.sourceforge.net/Basis/
  328.  
  329.  
  330. SML2C
  331. -----
  332. sml2c is a Standard ML to C compiler.  It is based on an old
  333. version of SML/NJ from 1992 and shares its front-end and most of the
  334. runtime system. sml2c is a batch compiler and compiles only module-level
  335. declarations.  It does not support SML/NJ style debugging and profiling.
  336.  
  337. sml2c is easily portable and has been ported to IBM RT, 
  338. Decstation 3100, Decstation 5000, Omron Luna 88k, sun-3, sun-4 and a 
  339. 486-based machine (running Mach).  The generated code is highly portable 
  340. and makes very few assumptions about the target machine or the C compilers 
  341. available on the target machine. The runtime system, which it shares with 
  342. the SML/NJ has several machine and operating system dependencies.  sml2c 
  343. has eliminated some of these dependencies by using portable schemes for 
  344. garbage collection and for freezing and restarting programs.
  345.  
  346. sml2c is available by anonymous ftp from ftp.cs.cmu.edu
  347. (128.2.206.173). Log in as anonymous, send username@node as password.
  348. The distribution can be found in /afs/cs/project/mess/research/sml2c/ftp.
  349. The local ftp software will allow you to change directory only
  350. to /afs/cs/project/mess/research/sml2c/ftp.  The README file in this
  351. directory describes the files in the distribution.
  352. The size of the uncompressed distribution is about 12 Meg.
  353.  
  354.  
  355. CAML LIGHT
  356. ----------
  357. Caml Light is a portable, bytecode interpreter for CAML, a dialect of ML.
  358. Some features of Caml Light include separate compilation, streams and
  359. stream parsers, ability to link to C code, and a fairly rich library.
  360. The implementation has low memory requirements, compiles quickly and
  361. generates compact executables. 
  362.  
  363. The Caml Light system comprises a batch compiler, a toplevel-based
  364. interactive compiler, tools for building libraries and toplevel
  365. systems, a replay debugger, and a hypertext-based module browser.
  366.  
  367. Caml Light runs on most modern Unix machines, including Sun
  368. Sparcstations (under SunOS 4.1 and Solaris 2), Decstations 3000
  369. (Alpha) and 5000 (Mips), and PCs under Linux, but many more machines
  370. have been reported to work. It is also available for the Macintosh (as
  371. a "fat binary" that runs native on PowerMacs) and the PC under
  372. MS Windows and MSDOS.
  373.  
  374. The current version is 0.73, released in January 1997. It is available by
  375. anonymous ftp from:
  376.  
  377.     host:           ftp.inria.fr    (192.93.2.54)
  378.     directory:      lang/caml-light
  379.  
  380. Summary of the files:
  381.  
  382.      README.cl            More detailed summary
  383.      cl73unix.tar.gz      Unix version (source code)
  384.      cl73macbin.sea.bin   Binaries for the Macintosh version
  385.      cl73win.exe          Binaries for MS Windows and MSDOS
  386.      cl73refman.*         Reference manual, in various formats
  387.      cl73tutorial.*       Tutorial, in various formats
  388.      cl73macdoc.sea.bin   On-line documentation for the Macintosh version
  389.      cl73macsrc.sea.bin   Source code for the Macintosh version
  390.  
  391. More information on Caml Light is available on the Web at:
  392.   http://pauillac.inria.fr/caml
  393.  
  394. The implementors can be contacted at caml-light@inria.fr.  General
  395. questions and comments of interest to the Caml community should be
  396. sent to caml-list@inria.fr, the Caml mailing list. (see question 2
  397. above for details.)
  398.  
  399.  
  400. OBJECTIVE CAML
  401. --------------
  402. Objective Caml (formerly known as Caml Special Light) is a complete
  403. reimplementation of Caml Light that adds a complete class-based
  404. object-oriented system and a powerful module system in the style of
  405. Standard ML.
  406.  
  407. The object system is statically type-checked (no "message not
  408. understood" run-time errors) and performs ML-style type reconstruction
  409. (no type declarations for function parameters). This is arguably the
  410. first publically available object-oriented language featuring ML-style
  411. type reconstruction.
  412.  
  413. The module system is based on the notion of manifest types /
  414. translucent sums; it supports Modula-style separate compilation, and
  415. fully transparent higher-order functors.
  416.  
  417. Objective Caml comprises two compilers: a bytecode compiler in the
  418. style of Caml Light (but up to twice as fast), and a high-performance
  419. native code compiler for the following platforms:
  420.  
  421.     Alpha processors: DecStation 3000 under OSF1 (a.k.a. Digital Unix)
  422.     Sparc processors: Sun Sparcstation under SunOS 4.1, Solaris 2, NetBSD
  423.     Intel 486 and Pentium processors: PCs under Linux, NextStep,
  424.         FreeBSD, Windows 95 and Windows NT
  425.     Mips processors: DecStation 3100 and 5000 under Ultrix 4
  426.     HP PA-RISC processors: HP 9000/700 under NextStep (no HPUX yet)
  427.     PowerPC processors: IBM RS6000 and PowerPC workstations under AIX 3.2
  428.  
  429. The native-code compiler delivers excellent performance (better than
  430. Standard ML of New Jersey 1.08 on our tests), while retaining the
  431. moderate memory requirements of the bytecode compiler.
  432.  
  433. The source distribution (for Unix machines only) is available by
  434. anonymous FTP on ftp.inria.fr, directory lang/caml-light.
  435.  
  436. More information on Objective Caml is available on the World Wide
  437. Web, at:  http://pauillac.inria.fr/ocaml/
  438.  
  439. Bug reports and technical questions should be directed to
  440. caml-light@inria.fr. For general questions and comments, use the Caml
  441. mailing list caml-list@inria.fr (to subscribe:
  442. caml-list-request@inria.fr).
  443.  
  444.  
  445. BIGLOO
  446. ------
  447. Bigloo is an optimizing Scheme-to-C and Caml-to-C compiler that
  448. produces native machine code from Caml sources. Compatibility with the
  449. bytecoded implementation of Caml Light is almost perfect. Performance
  450. of generated code is on a par with that of New Jersey ML. Bigloo is
  451. also one of the most efficient Scheme compilers available.
  452.  
  453. Bigloo runs on the following Unix platforms: Decstations 3000 and
  454. 5000, Sparcstations, PCs under Linux, HP PA 730 and Sony News R3000.
  455.  
  456. Bigloo is being developed by Manuel Serrano (Manuel.Serrano@inria.fr).
  457.  
  458. Available from:
  459.   ftp://ftp.inria.fr/lang/caml-light/bcl*.tar.gz.
  460.  
  461. CAMLOT
  462. -----
  463. Camlot is the stand alone Caml Light to C compiler. It then uses a standard C
  464. compiler to produce an executable machine code file. The compiler itself is
  465. mostly written in Caml Light and the runtime system is written in standard C,
  466. hence Camlot is easy to port to almost any 32-bit platform. The performance 
  467. of the resulting code is quite good, often ten times faster than the bytecode
  468. original implementation of Caml Light.
  469.  
  470. The distribution has been tested on the following platforms:
  471.  
  472.   Sun Sparcstation
  473.   DecStation 3100
  474.   HP 9000/710
  475.   i386/486 Linux
  476.  
  477. The distribution is avaiable at:
  478.   ftp://ftp.inria.fr/lang/caml-light/camlot0.64a.tar.gz
  479.  
  480. MOSCOW ML
  481. ---------
  482. Moscow ML provides a light-weight implementation of full Standard ML,
  483. including Modules and some extensions.
  484.  
  485. Moscow ML is based on the Caml Light bytecode system, which gives fast
  486. compilation and modest storage consumption.
  487.  
  488. Moscow ML 2.00 properties:
  489.  
  490.   * Supports the full SML'97, including Modules (structures, signatures, 
  491.     and functors), thanks to Claudio Russo
  492.   * Also provides several extensions to the SML Modules language:
  493.      - higher-order functors: functors may be defined within structures 
  494.        and functors
  495.      - first-class modules: structures and functors may be packed and 
  496.        then handled as Core language values, which may then be unpacked 
  497.        as structures or functors again
  498.      - recursive modules: signatures and structures may be recursively 
  499.        defined
  500.   * Implements Standard ML, as revised 1997 (value polymorphism, 
  501.     default overloading resolution, new types)
  502.   * Remains backwards compatible with previous releases of Moscow ML
  503.   * Implements most of the new Standard ML Basis Library, including
  504.     the most common input/output facilities in TextIO and BinIO
  505.   * Built-in help function
  506.   * Interactive top-level as well as separate (batch) compilation
  507.   * Can produce compact stand-alone executables
  508.   * Supports quotations and antiquotations, useful for metaprogramming
  509.   * Dynamic linking of external functions (Linux/x86 and Linux/Alpha, 
  510.     Solaris, Digital Unix, HP-UX, MacOS, Win'95/98/NT/2000)
  511.   * Interface to Boutell's library for making PNG images (structure Gdimage)
  512.   * Interface to the PostgreSQL database server (structure Postgres)
  513.   * Interface to the MySQL database server (structure Mysql)
  514.   * Interface to POSIX 1003.2 regular expressions (structure Regex)
  515.   * Interface to sockets (structure Socket)
  516.   * Interface to GNU gdbm persistent hashtables (structures Gdbm, Polygdbm)
  517.   * Facilities for fast functional generation of HTML code (structure Msp)
  518.   * Facilities for using CGI (structure Mosmlcgi and Mosmlcookie)
  519.   * Registration of ML and C functions for callbacks (structure Callback)
  520.  
  521.  
  522. SUPPORTED PLATFORMS
  523.  
  524. Intel x86-based PCs running Windows'95, '98, 'NT, and '2000, OS/2,
  525. Linux or FreeBSD; DEC Alpha running Linux or Digital Unix; Sun Sparc
  526. running Solaris or SunOS; HP9000 running HP/UX 9 or HP/UX 10; SGI MIPS
  527. running IRIX 5; Macintosh (68k and PPC) running MacOS (thanks to Doug
  528. Currie) or MkLinux, MacOS X.
  529.  
  530.  
  531. AUTHORS
  532.  
  533.   * Sergei Romanenko (roman@keldysh.ru), Moscow, Russia
  534.   * Claudio V. Russo (Claudio.Russo@cl.cam.ac.uk), Cambridge, UK
  535.   * Peter Sestoft (sestoft@dina.kvl.dk), Copenhagen, Denmark
  536.  
  537. AVAILABILITY
  538.  
  539.   * The Moscow ML homepage is
  540.       http://www.dina.kvl.dk/~sestoft/mosml.html
  541.   * Moscow ML library documentation
  542.       http://www.dina.kvl.dk/~sestoft/mosmllib/
  543.   * The Linux executables and documentation are in
  544.       ftp://ftp.dina.kvl.dk/pub/mosml/linux-mos20bin.tar.gz
  545.   * The Unix source files and documentation are in
  546.       ftp://ftp.dina.kvl.dk/pub/mosml/mos20src.tar.gz
  547.   * The MS Windows 95/98/NT executables and documentation are in 
  548.       ftp://ftp.dina.kvl.dk/pub/mosml/win32-mos20bin.zip
  549.   * The MacOS (68k and PPC) executables and docs and source diffs are in
  550.       ftp://ftp.dina.kvl.dk/pub/mosml/MacMoscowML20installer.hqx
  551.   * The MS Windows 95/98/NT/2000 source files are in 
  552.       ftp://ftp.dina.kvl.dk/pub/mosml/win32-mos20src.zip
  553.  
  554. Postscript and PDF versions of the documentation included with the
  555. binaries can be found in ftp://ftp.dina.kvl.dk/pub/mosml/doc/
  556.  
  557. Peter Sestoft (sestoft@dina.kvl.dk) 2000-08-03
  558.  
  559.  
  560. The ML Kit
  561. ----------
  562. Two versions of the ML Kit are available from DIKU: 
  563. (a) The ML Kit (Version 1, 1993)
  564. (b) The ML Kit with Regions (1997)
  565.  
  566. Both are described in more detail at the DIKU ML Kit web site:
  567.  
  568.      http://www.diku.dk/research-groups/topps/activities/mlkit.html
  569.  
  570. ML Kit Version 1
  571. ----------------
  572. Version 1 of the ML Kit is a straight translation of the 1990
  573. Definition of Standard ML into a collection of Standard ML modules.
  574. For example, every inference rule in the Definition is translated into
  575. a small piece of Standard ML code which implements it. The translation
  576. has been done with as little originality as possible - even variable
  577. conventions from the Definition are carried straight over to the Kit.
  578.  
  579. If you are primarily interested in executing Standard ML programs
  580. efficiently, the ML Kit is not the system for you! (It uses a lot of
  581. space and is very slow.) The Kit is intended as a tool box for those
  582. people in the programming language community who may want a
  583. self-contained parser or type checker for full Standard ML but do not
  584. want to understand the clever bits of a high-performance compiler. We
  585. have tried to write simple code and module interfaces; we have not
  586. paid any attention to efficiency.
  587.  
  588. The documentation is around 100 pages long and is provided with the
  589. Kit. It explains how to build, run, read and modify the Kit. It also
  590. describes how typing of flexible records and overloading are handled
  591. in the Kit.
  592.  
  593. The ML Kit is written by Nick Rothwell, David N. Turner, Mads Tofte
  594. and Lars Birkedal at Edinburgh and Copenhagen Universities.
  595.           
  596. The ML Kit with Regions (aka Version 2)
  597. ---------------------------------------
  598. Version 2 builds on Version 1, but is expanded into a real compiler.
  599. Inefficient data structures and algorithms in the system have been
  600. replaced by more efficient ones. The ML Kit with Regions is intended for
  601. the development of stand-alone applications which must be reliable,
  602. fast and space efficient.
  603.  
  604. The main feature of the ML Kit with Regions is that it uses a stack of
  605. regions for memory management rather than traditional garbage
  606. collection techniques; this has several important consequences:
  607.  
  608.    Compile-Time Garbage Collection: 
  609.      All memory allocation directives (both allocation and
  610.      de-allocation) are inferred by the compiler, which uses a number
  611.      of novel program analyses concerning lifetimes and storage
  612.      layout. There is no pointer-tracing garbage collection at
  613.      runtime;
  614.    Memory Safety: 
  615.      Safety of de-allocation of memory is ensured by the compiler; 
  616.    Static detection of space leaks; 
  617.    Region Resetting: 
  618.      It is possible to give explicit directives about resetting of
  619.      regions in cases where the static analyses are too conservative;
  620.      such directives are checked by the compiler;
  621.    Region Profiling: 
  622.      The system includes a graphical region profiler, which helps
  623.      gain detailed control over memory use; 
  624.    Soft Real-Time: 
  625.      Programmers who are interested in real-time programming can
  626.      exploit the absence of garbage collection: there are no
  627.      interruptions of unbounded duration at runtime;
  628.    Interface to the C language: 
  629.      ML Kit applications can call C functions using standard C calling
  630.      conventions; the region scheme can even take care of allocating
  631.      and de-allocating regions used by C functions thus invoked.
  632.  
  633. The overall goal with developing the ML Kit with Regions has been to
  634. combine the advantages of a high-level, type-safe language (Standard
  635. ML, 1997 Definition), with the advantages of low-level languages,
  636. namely detailed control over space and time. Indeed, it turns out that
  637. the regularity provided by the ML type system makes is possible to
  638. infer much more useful information about ML programs than one can
  639. reasonably hope for in languages with more liberal type
  640. systems. Naturally, the hope is that this technology will promote the
  641. use of Standard ML in situations where safety and detailed control of
  642. machine resources are important, as indeed is often the case.
  643.  
  644. Since we are using Standard ML as our source language, one can use the
  645. ML Kit in conjunction with other Standard ML systems; for example, one
  646. can port programs that previously ran on a garbage collection based
  647. Standard ML system to run on the Kit; or one may use the Kit simply to
  648. gain insight into how a program intended for another system uses
  649. memory; or one can develop Standard ML programs directly in the Kit.
  650. We have tried all three with good results.
  651.  
  652. A comprehensive technical report "Programming with Regions in the ML Kit"
  653. is available from the above web site.
  654.  
  655. The ML Kit with Regions was developed by Mads Tofte, Lars Birkedal,
  656. Martin Elsman, Niels Hallenberg, Tommy H{\o}jfeld Olesen (all at DIKU) and
  657. Peter Sestoft and Peter Berthelsen (both at KVL).
  658.  
  659.  
  660. Edinburgh ML 4.0
  661. ----------------
  662. Edinburgh ML 4.0 is an implementation of the core language (without
  663. the module system).  It uses a bytecode interpreter, which is written in C
  664. and runs on any machine with 32 bit words, a continuous address space and
  665. a correct C compiler.  Ports to various 16 bit machines are underway.  The
  666. bytecode interpreter can be compiled with switches to avoid the buggy parts
  667. of the C compilers that we've used it with (as far as I know none of them
  668. worked correctly).  
  669.  
  670. Edinburgh ML 4.0 is available from the LFCS.  See the WWW link:
  671.      http://www.dcs.ed.ac.uk/lfcsinfo/index.html
  672.  
  673. A port to PCs with 386SX processors or better is available by FTP from
  674. ftp.informatik.uni-muenchen.de, in the file
  675. pub/comp/programming/languages/sml/ibmpc/edml3864.exe.
  676. Contact Joern Erbguth (erbguth@juris-sb.de) for more information.
  677.  
  678. Also, there are apparently 8086 and 80386-specific ports of Edinburgh
  679. ML 3.5 in the same location.  The 386 port is in the file
  680. edml3863.exe.
  681.  
  682. There are other Edinburgh (PC-)ports of ML including an OS/2 2.x, an
  683. OS/2 PM and a Dos version. A new version has just been made ready and
  684. is available at forwiss.uni-passau.de (132.231.1.10) in
  685. pub/ibmpc/os2/lang/sml/sml04.zip. It is about 360K long (short?).
  686.  
  687.     All 3 programs have in common (all in one .zip):
  688.        - true 32 Bit applications
  689.        - easy to install, easy to use
  690.        - As far as I know they work stable
  691.          (except the DOS version working as a Windows window
  692.          [you can use it with Windows but it crashes on *exit*])
  693.        - they don't require expensive hardware 
  694.          (and they don't need a co-processor)
  695.  
  696.     To be more specific:
  697.           OS/2 PM               OS/2                DOS    
  698.     OS    >= OS/2 2.0+ServPak   >= OS/2 2.0        >= DOS 5.0
  699.     Edit  PM, GUI,              Standard            command history
  700.           integrated editor
  701.           (cut&paste)
  702.     HW    >= 386/33, 8MB        >= 386/33 4MB       >= 386sx, 2MB
  703.           lots of MB and fast
  704.           graphics ad. recommended
  705.     Help  online                online
  706.           (+ML ref. in german)
  707.  
  708. There's also an amiga port of Edinburgh ML available on all aminet ftp
  709. sites (amiga users should know which these are) in dev/lang, called
  710. "sml4.1.02.lha".  The standard version needs a 68020 or better and an
  711. FPU but there is a 68000-only version as well.
  712.  
  713. MicroML
  714. -------
  715. MicroML is an interpreter for core SML that runs on IBM PCs,
  716. from the Department of Computing Science at the Umea University in
  717. Sweden.  It implements the core language except for records.  A 80286
  718. processor or better is recommended, but it runs even on a 8086. 
  719.  
  720. MicroML is available by anonymous ftp from
  721. ftp.cs.umu.se /pub/uml022.zoo.  For more information contact Olof Johansson
  722. (olof@cs.umu.se).
  723.  
  724.  
  725. Poly/ML
  726. -------
  727. Poly/ML, probably the longest established implementation of Standard ML,
  728. is now available at http://www.polyml.org .
  729.  
  730. Poly/ML was originally written in the mid-eighties at Cambridge
  731. University.  For several years it was marketed by Abstract Hardware
  732. Limited who developed it further.  Recently the rights were reacquired
  733. by Cambridge University Technical Services who have agreed to make
  734. Poly/ML freely available.  Poly/ML now supports full SML 97 and the
  735. Standard Basis Library, along with some non-standard extensions.
  736. According to the web page, the compiler source is available, as well
  737. as binary releases.
  738.  
  739. Poly/ML is currently available for Linux and Windows on Intel
  740. platforms, Sparc/Solaris, and MacOS X. Measurements with several large
  741. ML applications shows Poly/ML to be one of the fastest implementations
  742. of Standard ML around.
  743.  
  744. Poplog ML
  745. ---------
  746. Poplog is a portable system including incremental compilers for Pop-11,
  747. Common Lisp, Prolog and Standard ML, along with a huge amount of system
  748. documentation, teaching materials for AI/Cognitive Science, the
  749. Sim_agent Toolkit, vision libraries, and other things.
  750.  
  751. "Poplog" is a trade mark of the University of Sussex, where most
  752. of Poplog was developed, starting with Pop-11 on a PDP11/40 computer
  753. in the mid 70s, inspired by the Edinburgh AI language Pop2.
  754.  
  755. The full Poplog system (as of version 15.53) is available free of
  756. charge, including source code.
  757.  
  758. For more information, see
  759.  
  760.     ftp://ftp.cs.bham.ac.uk/pub/dist/poplog/poplog.info.html
  761.  
  762. For information about the free versions available, and various teaching
  763. and research support libraries for AI see:
  764.  
  765.     ftp://ftp.cs.bham.ac.uk/pub/dist/poplog/freepoplog.html
  766.  
  767. This includes versions of Poplog V15.53 for
  768.  
  769.     Solaris+Sparc (works on Solaris 7 as well as earlier versions)
  770.     PC Linux (RedHat 5.x, and 6.0) with or without motif
  771.  
  772. There are slightly older versions for
  773.     PC+Solaris86
  774.     Dec Alpha + Digital unix
  775.  
  776. Reduced version (no graphics, nothing that depends on X)
  777.     PC+Windows95/98 (may work on NT also?)
  778.  
  779. Poplog comes with masses of online documentation: this can be browsed at
  780.     ftp://ftp.cs.bham.ac.uk/pub/dist/poplog/doc/
  781.  
  782. Pop-11 documentation can be found at
  783.  
  784.     ftp://ftp.cs.bham.ac.uk/pub/dist/poplog/primer/START.html
  785.     or ftp://ftp.cs.bham.ac.uk/pub/dist/poplog/
  786.  
  787. A slightly zany tutorial file on story grammars can be read in
  788.  
  789.     ftp://ftp.cs.bham.ac.uk/pub/dist/poplog/teach/storygrammar
  790.  
  791. COMP.LANG.POP
  792. Comments and questions about Poplog and Pop-11 may be posted to the
  793. comp.lang.pop newsgroup, which is linked to an email list.
  794. See ftp://ftp.cs.bham.ac.uk/pub/dist/poplog/newsgroup.txt
  795.  
  796. (Please do NOT post general conference announcements, advertisements,
  797. etc.)
  798.  
  799. Adrian John Howard (adrianh@cogs.susx.ac.uk) has a WWW page for Poplog:
  800.  
  801.     http://www.cogs.susx.ac.uk/users/adrianh/poplog.html
  802.  
  803. Harlequin MLWorks
  804. -----------------
  805.  
  806. Harlequin MLWorks is no longer available as a commercial product.
  807.  
  808. http://www.harlequin.com/products/mlworks_message.html
  809.  
  810. MLJ
  811. ---
  812. MLj is a Standard ML compiler which produces Java bytecodes. 
  813.  
  814. MLj 0.2 compiles the functor-free subset of the new SML'97 language plus
  815. some new language extensions for straightforward interlanguage working
  816. with Java. It produces compact standalone compiled code which can be
  817. run on any computer with a Java Virtual Machine. This release includes a 
  818. number of improvements over the original release (0.1), including 
  819. significantly better compilation times, better code generation, more complete 
  820. Basis library support, better error messages and friendlier language 
  821. extensions for interlanguage working.
  822.  
  823. Although there are limitations (most importantly a lack of 
  824. general tail-call optimisation), MLj is quite usable for many 
  825. small-to-medium projects. It can be used to write portable ML
  826. applications and applets which make use of Java's standard libraries
  827. for graphics, database access, networking, etc. and which interwork
  828. with third-party Java code.
  829.  
  830. Visit the new MLj website at http://www.dcs.ed.ac.uk/~mlj/ to find
  831. out more about MLj, see some example ML applets and download the MLj
  832. 0.2 distribution.
  833.  
  834. The compiler is distributed as source+standalone binaries for Sparc/Solaris,
  835. Intel/Linux and Intel/Windows, and in source-only form for compilation under
  836. SML/NJ version 110. It is covered by the GNU Public License version 2. 
  837.  
  838. MLj was written by Nick Benton, Andrew Kennedy and George Russell of
  839. the Cambridge Research Group of Persimmon IT, Inc. Please note that 
  840. Persimmon IT will no longer distribute or support the compiler; 
  841. instead, Ian Stark and Tom Chothia of the University of Edinburgh 
  842. have kindly offered to host the new download site. The original authors 
  843. continue to develop the compiler and it is hoped that further releases will 
  844. take place in the future.
  845.  
  846.  
  847. MLton
  848. -----
  849.  
  850. MLton is a whole-program optimizing compiler for the Standard ML
  851. programming language.  MLton runs on X86 machines with Linux, FreeBSD,
  852. or Cygwin/Windows.  MLton has the following features.
  853.  
  854.    + Generates standalone executables with good runtime performance
  855.    + SML 97 compliant, with a mostly complete basis library
  856.    + Fast IntInf based on the GNU multiprecision library (gmp)
  857.    + Fast C FFI
  858.    + Profiling
  859.    + Supports large amounts of memory and large arrays.
  860.    + Libraries for continuations, interval timers, random numbers,
  861.        resource limits, resource usage, signal handlers, sockets, system
  862.        logging, threads, and heap save and restore
  863.  
  864. For more information, go to the MLton home page. 
  865.  
  866.     http://www.mlton.org/
  867.  
  868. Send comments, questions, and bug reports to MLton@mlton.org.
  869.  
  870.  
  871. HaMLet
  872. ------
  873.  
  874. HaMLet is a faithful implementation of the Standard ML programming
  875. language (SML'97). It aims to be
  876.  
  877. * an accurate reference implementation of the language specification, 
  878. * a platform for experimentation with the language semantics or
  879. extensions to it, 
  880. * a useful tool for educational purposes. 
  881.  
  882. The implementation is intended to be as direct a translation of the
  883. language formalisation found in the Definition of Standard ML as
  884. possible, modulo bug fixes. It tries hard to get all details of the
  885. Definition right. The HaMLet source code
  886.  
  887. * implements complete Standard ML, 
  888. * closely follows the structure of the Definition, with lots of cross
  889. references, 
  890. * conforms to the latest version of the Standard ML Basis Library,
  891. * is written entirely in Standard ML, with the ability to bootstrap, 
  892. * may readily be compiled with SML/NJ, Moscow ML, or MLton. 
  893.  
  894. HaMLet can perform different phases of execution - like parsing,
  895. elaboration (type checking), and evaluation - selectively. In
  896. particular,
  897. it is possible to execute programs in an untyped manner, thus exploring
  898. the universe where even ML programs "can go wrong".
  899.  
  900. SML.NET
  901. -------
  902. SML.NET is a whole program compiler for full Standard ML that compiles
  903. to the .NET Common Language Runtime.  For more information, see
  904.  
  905. http://www.cl.cam.ac.uk/Research/TSG/SMLNET/
  906.  
  907. --------------------------------------------------------------------------
  908.  
  909. 4. Unsupported SML/NJ Ports
  910.  
  911. This section describes various ports of SML/NJ (see section 3) 
  912. that are not directly supported by the NJ folks.  
  913.  
  914. OS/2:
  915. ----
  916.  
  917. An old port of SML/NJ ver. 0.93 to OS/2 exists.  The port is no longer
  918. being maintained, but may be downloaded from:
  919.  
  920.   ftp://ftp.dina.kvl.dk/pub/Staff/Peter.Bertelsen/smlnj/0.93-os2/
  921.  
  922. Another unmaintained and somewhat incomplete port of SML/NJ
  923. ver. 108.10 to OS/2 may be downloaded from:
  924.  
  925.   ftp://ftp.dina.kvl.dk/pub/Staff/Peter.Bertelsen/smlnj/108.10-os2/
  926.  
  927. NEXTSTEP:
  928. ---------
  929. The CSDMteam at the University of Munich proudly presents the port of 
  930. Standard  ML of NJ, version 0.93, to NEXTSTEP for Intel processors.
  931.  
  932. The modified source can be found at ftp.informatik.uni-muenchen.de:
  933. /pub/comp/programming/languages/sml/NJ-0.93/93.src.nsfip.tar.Z (please look 
  934. at the installation instructions in the file README.NeXT.I386).
  935.  
  936. A precompiled binary of the interpreter (gzip'ed) is located at  
  937. ftp.informatik.uni-muenchen.de:/pub/comp/platforms/next/Developer/languages/ml 
  938. /sml.0.93.I.b.gz.
  939.  
  940. SVR4:
  941. -----
  942. An mplementation for SVR4.0.4 is available from Anthony Shipman 
  943. (als@tusc.com.au) that fixes the problems with listDir and getWD 
  944. and includes a full malloc implementation for runtime/malloc.c.  
  945. Contact Anthony for more info.
  946.  
  947.  
  948. --------------------------------------------------------------------------
  949.  
  950. 5. Where can I find documentation on ML?
  951.  
  952. THE DEFINITION
  953. --------------
  954. Robin Milner, Mads Tofte, Robert Harper and Dave MacQueen
  955. The Definition of Standard ML (Revised)
  956. MIT Press, 1997, xiii + 114 pp.
  957. ISBN 0-262-63181-4 (paper)
  958.  
  959. Robin Milner, Mads Tofte and Robert Harper
  960. The Definition of Standard ML
  961. MIT, 1990.
  962. ISBN: 0-262-63132-6
  963.  
  964. Robin Milner and Mads Tofte
  965. Commentary on Standard ML
  966. MIT, 1991
  967. ISBN: 0-262-63137-7
  968.  
  969. TEXTS       (date order)
  970. -----
  971. Ake Wikstrom
  972. Functional Programming Using Standard ML
  973. Prentice Hall 1987
  974. ISBN: 0-13-331661-0
  975.  
  976. Chris Reade
  977. Elements of Functional Programming
  978. Addison-Wesley 1989
  979. ISBN: 0-201-12915-9
  980. (see http://www.kingston.ac.uk/~bs_s075/EofFP.html for information and
  981. updates)
  982.     
  983. Stefan Sokolowski
  984. Applicative High Order Programming: The Standard ML perspective
  985. Chapman & Hall 1991
  986. ISBN: 0-412-39240-2     0-442-30838-8 (USA)
  987.  
  988. Ryan Stansifer
  989. ML Primer
  990. Prentice Hall, 1992
  991. ISBN 0-13-561721-9
  992.  
  993. Colin Myers, Chris Clack, and Ellen Poon
  994. Programming with Standard ML
  995. Prentice Hall, 1993
  996. ISBN 0-13-722075-8 (301pp)
  997.  
  998. Jeffrey D. Ullman
  999. Elements of ML Programming
  1000. Prentice-Hall, 1993 (Oct. 15)
  1001. ISBN: 0-13-184854-2
  1002. (See Comp.Lang.ML archives, message from Ullman dated 22 Sep 1993 for
  1003.  chapter headings.)
  1004.  
  1005. Rachel Harrison
  1006. Abstract Data Types in Standard ML
  1007. John Wiley & Sons, April 1993
  1008. ISBN: 0-471-938440
  1009.  
  1010. Richard Bosworth
  1011. A Practical Course in Functional Programming Using Standard ML,
  1012. McGraw-Hill 1995,
  1013. ISBN: 0-07-707625-7.
  1014.  
  1015. Elementary Standard ML
  1016. Greg Michaelson
  1017. UCL Press 1995
  1018. ISBN: 1-85728-398-8 PB
  1019. (available at <ftp://ftp.macs.hw.ac.uk/pub/funcprog/gjm.book95.ps.Z>)
  1020.  
  1021.  
  1022. Lawrence C Paulson
  1023. ML for the Working Programmer (2nd Edition, ML97)
  1024. Cambridge University Press 1996
  1025. ISBN: 0-521-56543-X (paperback), 0-521-57050-6 (hardback)
  1026. http://www.cl.cam.ac.uk/users/lcp/MLbook/
  1027.  
  1028. Jeffrey D. Ullman
  1029. Elements of ML Programming (2nd Edition, ML97)
  1030. MIT Press 1997
  1031. http://www-db.stanford.edu/~ullman/emlp.html
  1032.  
  1033. G.Cousineau & M.Mauny
  1034. The Functional Approach to Programming
  1035. Cambridge University Press, 1998
  1036. [Uses CAML]
  1037.  
  1038. M.Felleisen & D.P.Friedman
  1039. The Little MLer
  1040. MIT Press, 1998
  1041.  
  1042. Chris Okasaki
  1043. Purely Functional Data Structures
  1044. Cambridge University Press, 1998.
  1045. ISBN: 0-521-63124-6
  1046.  
  1047. Michael R. Hansen, Hans Rischel
  1048. Introduction to Programming using SML
  1049. Addison-Wesley, 1999
  1050. ISBN: 0-201-39820-6 
  1051. http://www.it.dtu.dk/introSML
  1052.  
  1053. John Reppy
  1054. Concurrent Programming in ML
  1055. Cambridge University Press 1999
  1056. ISBN: 0-521-48089-2
  1057.  
  1058. INFORMATION AVAILABLE BY INTERNET
  1059. ---------------------------------
  1060.  
  1061. The Fox project at CMU has a WWW page for information about Standard ML,
  1062. which also includes the first two reports below:
  1063.    http://foxnet.cs.cmu.edu/sml.html
  1064.  
  1065. The following report covers all of Standard ML, and is available at:
  1066.     ftp://ftp.cs.cmu.edu/afs/cs/project/fox/mosaic/intro-notes.ps
  1067. A revised, though still unstable web version of these notes is
  1068. available at:
  1069.     http://www.cs.cmu.edu/People/rwh/introsml
  1070.   Robert Harper
  1071.   Introduction to Standard ML
  1072.   LFCS Report Series  ECS-LFCS-86-14
  1073.   Laboratory for Foundations of Computer Science
  1074.   Department of Computer Science
  1075.   University of Edinburgh
  1076.   Nov. 1986 (revised Jan. 1989 by Nick Rothwell and Kevin Mitchell)
  1077.  
  1078. The following report includes an introduction to Standard ML and 3
  1079. lectures on the modules system.  Available from: 
  1080.     http://foxnet.cs.cmu.edu/sml.html
  1081.   Mads Tofte
  1082.   Four Lectures on Standard ML
  1083.   LFCS Report Series  ECS-LFCS-89-73
  1084.   Laboratory for Foundations of Computer Science
  1085.   Department of Computer Science
  1086.   University of Edinburgh
  1087.   March 1989
  1088.  
  1089. Extended ML (EML) is a framework for specification and formal
  1090. development of SML programs.  EML specifications look just like SML
  1091. programs except that logical axioms are allowed in signatures and in
  1092. place of code in structures and functors.  Some EML specifications are
  1093. executable, making EML a "wide-spectrum" language which can be used to
  1094. express every stage in the development of a SML program from the
  1095. initial high-level specification to the final program itself and
  1096. including intermediate stages in which specification and program are
  1097. intermingled.  Formally developing a program in EML yields an
  1098. interconnected collection of generic SML modules, each with a complete
  1099. and accurate axiomatic specification of its interface with the rest of
  1100. the system.  Information about EML is available from
  1101. http://www.dcs.ed.ac.uk/home/dts/eml/
  1102.  
  1103. Le projet Cristal at INRIA Rocquencourt has set up a WWW server for
  1104. information regarding its activities, especially the Caml and Caml
  1105. Light compilers. The server also offers on-line access to
  1106. documentation, publications and to a database of BibTex references in
  1107. CS.  Welcome to:
  1108.    http://pauillac.inria.fr/
  1109. Please report problems and suggestions to Xavier.Leroy@inria.fr.
  1110.  
  1111. Richard Botting has taken Larry Paulson's SML Syntax and
  1112. translated it into a form that can be read by mosaic, netscape,
  1113. lynx and other WWW browsers.  The URL is:
  1114.   http://www.csci.csusb.edu/dick/samples/ml.syntax.html
  1115.  
  1116. Andrew Cumming has made availible "A Gentle Introduction to ML".  It
  1117. is aimed at students who are reasonably computer literate but who are
  1118. new to functional programming.  It consists largely of questions and
  1119. diversions broken up into roughly one-hour tutorials, most of the
  1120. questions have hints which the student can follow up if required.  The
  1121. material is intended to be used alongside ML - sections of code may be
  1122. copied from the browser window into an ML session.  The URL is
  1123.    http://www.dcs.napier.ac.uk/course-notes/sml/manual.html
  1124.  
  1125. There are some WWW pages based on an info-tree at MIT with a variety
  1126. of useful information on ML.  The URL is:
  1127.    http://www.ai.mit.edu/!info/sml/!!first
  1128.  
  1129. There is an interesting collection of news articles at:
  1130.    http://www.cs.jcu.edu.au/ftp/web/FP/ml.html
  1131.  
  1132. --------------------------------------------------------------------------
  1133.  
  1134. 6. Where can I find library code?
  1135.  
  1136. a. The Standard ML ('97) Basis Library
  1137.  
  1138.  In order to enhance the usefulness of SML as a general-purpose
  1139.  programming language, a group of SML implementers, including
  1140.  representatives of Harlequin's ML Works, Moscow ML and SML/NJ, have
  1141.  put together a proposal for an SML Basis Library, containing a
  1142.  collection of modules to serve as a basic toolkit for the SML
  1143.  programmer. The current draft is available on the web at
  1144.           http://SML.sourceforge.net/Basis/
  1145.  
  1146. b. The Edinburgh SML Library
  1147.  
  1148.  The Edinburgh SML Library provides a consistent set of functions on the
  1149.  built-in types of the language and on vectors and arrays, and a few extras.
  1150.  It includes a "make" system and a consistent set of parsing and unparsing
  1151.  functions.  The library consists of a set of signatures with sample portable
  1152.  implementations, full documentation, and implementations for Poly/ML,
  1153.  Poplog ML and SML/NJ that use some of the non-standard primitives
  1154.  available in those systems.  It is distributed with Poly/ML, Poplog ML and
  1155.  Standard ML of New Jersey.  It is also available from the LFCS.
  1156.  
  1157.  The library documentation is available as a technical report from the LFCS
  1158.  (reports@dcs.ed.ac.uk) and costs 5 pounds or 10 US dollars.  The
  1159.  LaTeX source of the report is included with the library.
  1160.  
  1161.  Dave Berry
  1162.  The Edinburgh SML Library
  1163.  LFCS Report Series  ECS-LFCS-91-148
  1164.  Laboratory for Foundations of Computer Science
  1165.  Department of Computer Science
  1166.  University of Edinburgh
  1167.  April 1991
  1168.  
  1169. c. The SML/NJ Library
  1170.  
  1171.  The SML/NJ Library is distributed with the SML of New Jersey compiler.
  1172.  It provides a variety of utilities such as 2-dimensional arrays, sorting,
  1173.  sets, dictionaries, hash tables, formatted output, Unix path name
  1174.  manipulation, etc.  The library compiles under SML/NJ but should
  1175.  be mostly portable to other implementations.
  1176.  
  1177.  
  1178. d. SML_TK
  1179.  
  1180.  sml_tk is a Standard ML package providing a portable, typed and
  1181.  abstract interface to the user interface description and command
  1182.  language Tcl/Tk. It combines the advantages of the Tk toolkit with
  1183.  the advantages of Standard ML (bypassing the shortcomings of Tcl),
  1184.  allowing the implementation of graphical user interfaces in a
  1185.  structured and reusable way, supported by the powerful module system
  1186.  of Standard ML.
  1187.  
  1188.  For more information, and to obtain sml_tk, please point your web
  1189.  browser to the sml_tk homepage at
  1190.     http://www.informatik.uni-bremen.de/~cxl/sml_tk
  1191.  or contact us at smltk@informatik.uni-bremen.de.
  1192.  
  1193.  
  1194. e. Caml-light libraries 
  1195.    (Included in the Caml Light distribution unless otherwise noted)
  1196.    (Most of these libraries are also available for Objective Caml)
  1197.  
  1198.  CAML-TK
  1199.  TK is a GUI library for the TCL language. Normally, TK is controlled
  1200.  from TCL. The Caml-TK interface provides a Caml Light library to control TK
  1201.  from Caml Light programs. Thus, TK can be used to program graphical
  1202.  user-interfaces in Caml Light without knowledge of the TCL language.
  1203.  
  1204.  LIBGRAPH 
  1205.  The "libgraph" library implements basic graphics primitives (line
  1206.  and text drawing, bitmaps, basic event processing) for the Caml Light system.
  1207.  It is portable across all platforms that run Caml Light: X-Windows,
  1208.  Macintosh, MSDOS.
  1209.  
  1210.  CAMLWIN
  1211.  Camlwin is a GUI library for Caml Light that provide all the classical
  1212.  graphic objects: buttons, string and text editors, list... and a high
  1213.  level object like windowed file selector. It is based on an extension
  1214.  of the "libgraph" library and therefore highly portable. Its main
  1215.  interest is its ability to compile the same code under many systems.
  1216.  At present time, it works under DOS, Windows, and X11 with unix.
  1217.  Camlwin is distributed at:
  1218.    ftp.inria.fr:lang/caml-light/Usercontribs/camlwin
  1219.  The reference manual is also available on the WWW at:
  1220.    http://liasc.enst-bretagne.fr/~saunier
  1221.  
  1222.  LIBNUM 
  1223.  The "libnum" library implements exact-precision rational arithmetic
  1224.  for Caml Light. It is built upon a state-of-the-art
  1225.  arbitrary-precision integer arithmetic package, and therefore
  1226.  achieves very good performance (it's much faster than Maple, for
  1227.  instance).
  1228.  
  1229.  LIBUNIX 
  1230.  The "libunix" library makes many Unix system calls and system-related
  1231.  library functions available to Caml Light programs. It provides Caml
  1232.  programs with full access to Unix capabilities, especially network
  1233.  sockets.
  1234.  
  1235.  LIBSTR
  1236.  The "libstr" library for Caml Light provides high-level string
  1237.  processing functions, including regular expression matching and
  1238.  substitution. It is intended to support the kind of text processing
  1239.  that is usually performed with "sed" or "perl".
  1240.  
  1241. f. The Qwertz Toolbox
  1242.  
  1243.  The qwertz toolbox, a library of Standard ML modules with an emphasis
  1244.  on symbolic Artificial Intelligence programming, may now be obtained
  1245.  by anonymous ftp at:
  1246.     ftp.gmd.de:gmd/ai-research/Software/qwertz.tar.gz
  1247.  
  1248.  The qwertz.tar.gz file is a tar archive compressed using the the GNU
  1249.  gzip program.  Use the gunzip program to decompress it.  The
  1250.  README file explains how the install the library.  
  1251.  
  1252.  The toolbox includes: symbols and symbolic expressions, tables
  1253.  including association lists, sets, queues and priority queues,
  1254.  streams, heuristic search including A* and iterative deepening,
  1255.  and an ATMS reason maintenance system.
  1256.  
  1257.  
  1258. --------------------------------------------------------------------------
  1259.  
  1260. 7. Theorem Provers and ML
  1261.  
  1262. (Collected by Paul Black, pblack@cs.berkeley.edu.  Thanks Paul!)
  1263.  
  1264. - LCF (Edinburgh LCF and Cambridge LCF)
  1265.     * originally written in the Edinburgh dialect of ML from which SML 
  1266.       developed.
  1267.  
  1268.    "Logic and Computation: Interactive Proof with Cambridge LCF"
  1269.     also by Lawrence C. Paulson.  (Describes a Standard ML [core language
  1270.     only] version of LCF.)  The port was done by M. Hedlund, then at
  1271.     Rutherford Appleton Labs, UK.  It is available by anon. ftp from
  1272.     ftp://ftp.cl.cam.ac.uk/ml/lcf.tar.gz.
  1273.  
  1274. - Lego (LFCS, Edinburgh Univ., SML)
  1275.     * originally developed in CAML
  1276.     * latest version (5) now runs under SML/NJ 
  1277.     * only higher-order resolution
  1278.     * available via anon. ftp from ftp.dcs.ed.ac.uk:/pub/lego
  1279.  
  1280. - HOL90 
  1281.    Authors = Konrad Slind, Elsa Gunter
  1282.    kxs@cl.cam.ac.uk, elsa@research.att.com
  1283.    http://www.cl.cam.ac.uk/Research/HVG/HOL/
  1284.  
  1285.    hol90 is a free implementation in SML/NJ of Mike Gordon's HOL logic (a
  1286.    polymorphic version of Church's Simple Type Theory). The system provides
  1287.    a lot of automated support including:
  1288.    
  1289.    - a powerful rewriting package;
  1290.    - pre-installed theories for booleans, products, sums, natural
  1291.      numbers, lists, and trees;
  1292.    - definition facilities for recursive types and recursive functions
  1293.      over those types (mutual recursion is also handled);
  1294.    - extensive libraries for strings, sets, group theory, integers, the
  1295.      real numbers, wellordered sets, automatic solution of goals
  1296.      involving linear arithmetic, tautology checking, inductively
  1297.      defined predicates, Hoare logic, Chandy and Misra's UNITY theory,
  1298.      infinite state automata, and many others.
  1299.  
  1300.    The HOL community has a lively mailing list accessible at
  1301.    info-hol-request@leopard.cs.byu.edu and a yearly user's meeting that
  1302.    alternates between Europe and North America. hol90 is available by
  1303.    anonymous ftp from
  1304.  
  1305.     machine = ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/slind/hol90/
  1306.      or
  1307.     machine = ftp.research.att.com/dist/ml/hol90/
  1308.  
  1309.    Tim Leonard mentions that a description of the variant of ML used in
  1310.    HOL88 is online at the following url:
  1311.  
  1312.    http://lal.cs.byu.edu/lal/holdoc/Description/ML/ML.html
  1313.  
  1314. - NuPrl (from Bob Constable`s group at Cornell)
  1315.  
  1316. - Isabelle (Lawrence C. Paulson, Cambridge and Tobias Nipkow, Munich)
  1317.     * has integrated rewriting and classical reasoning
  1318.     * a generic proof tool supporting the following formalisms among others:
  1319.                 i) FOL - first order logic
  1320.                 ii) HOL - higher order logic
  1321.                 iii) LCF - Logic of computable functions
  1322.                 vi) ZF - Zermelo-Fraenkel set theory
  1323.     * There's a WWW page:
  1324.         http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
  1325.     * There's also a mailing list: isabelle-users@cl.cam.ac.uk
  1326.  
  1327. - MERILL (Brian Matthews, U. of Glasgow & Rutherford Appleton Laboratory)
  1328.     * written in standard ML
  1329.     * a general purpose order-sorted equational reasoning system
  1330.     * Allows the user to declare their own object language, allows
  1331.     AC-rewriting and AC-unification of terms and equations, has
  1332.     several completion algorithms, is built on a hierarchy of
  1333.     types known as Order-Sorting, and allows the user to try
  1334.     different termination methods.
  1335.     * available via anonymous ftp from the University of Glasgow,
  1336.     ftp address: ftp.dcs.glasgow.ac.uk (130.209.240.50)
  1337.     * Brian Matthews, brian@dcs.glasgow.ac.uk or bmm@inf.rl.ac.uk
  1338.  
  1339. - FAUST (Karlsruhe)
  1340.     * a HOL add-on written in ML.
  1341.     * ftp from goethe.ira.uka.de (129.13.18.22)
  1342.  
  1343. - Alf
  1344.     * written in SML
  1345.     * An implementation of Martin-Lofs type theory with dependent types
  1346.     * Proof editor
  1347.     * available by anonymous ftp from cs.chalmers.se
  1348.     * only higher-order resolution
  1349.  
  1350. - Coq
  1351.    * written in Objective CAML 
  1352.      (previous versions were written in CAML and Caml-Light)
  1353.    * implements the Calculus of Inductive Constructions 
  1354.      a logical framework suitable for abstract mathematical formalisation 
  1355.      and functional program manipulation.
  1356.    * available via anon. ftp from ftp.ens-lyon.fr:/pub/LIP/COQ/V6.1
  1357.      ftp.inria.fr:INRIA/Projects/coq/coq/V6.1
  1358.    * possible contact: coq@pauillac.inria.fr
  1359.      more information : http://pauillac.inria.fr/coq/systeme_coq-eng.html
  1360.    * Coq has an interface based on Centaur developed by the CROAP project 
  1361.      at INRIA Sophia-Antipolis :
  1362.     http://www.inria.fr/croap/ctcoq/ctcoq-eng.html
  1363.  
  1364. - ICLHOL/ProofPower (Lemma 1)
  1365.     * a commercial system using a reimplementation of HOL in SML
  1366.     * http://www.lemma-one.com/ProofPower/index/index.html
  1367.  
  1368. - Lamdba/DIALOG (Abstract Hardware Ltd)
  1369.     * a commercial tool written in Poly/ML
  1370.     * contact ahl@ahl.co.uk
  1371.  
  1372. - Twelf (Frank Pfenning & Carsten Schuermann, Carnegie Mellon Univ)
  1373.   * Twelf is a meta-logical framework for deductive systems.
  1374.   * Twelf includes an implementation of LF, including type
  1375.     reconstruction, the Elf constraint logic programming language,
  1376.     and a preliminary inductive meta-theorem prover for LF.
  1377.   * The implementation is written in SML'97 and has been tested
  1378.     under SML/NJ and MLWorks on Unix and Windows platforms.
  1379.     It also includes a complete user's manual, tutorial,
  1380.     example suites, and an Emacs mode.
  1381.   * Further information, including download instructions, information
  1382.     on the mailing list, publications, etc. can be found at
  1383.     http://www.cs.cmu.edu/~twelf
  1384.  
  1385. - Definitional Reasoning (Univerity of Tasmania)
  1386.    * developed with SML/NJ
  1387.    * a study of Boolean Affine Combinations (a highly formal case construct)
  1388.    * includes a rich set of term rewriting combinators
  1389.    * ftp://hilbert.maths.utas.edu.au/pub/DR.tar.gz
  1390.    * mail to piggy@acm.org for more information.
  1391.  
  1392. References
  1393.    "ML for the Working Programmer" by Lawrence C. Paulson contains a
  1394.     small first-order theorem prover.
  1395.  
  1396.     Paulson also has a good chapter on writing theorem provers in ML in
  1397.     "Handbook of logic in computer science",
  1398.     Edited by:  S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum.
  1399.     Oxford : Clarendon Press, 1992-.
  1400.     CALL#: QA76 .H2785 1992 
  1401.    
  1402. Others
  1403.     Edinburgh's Concurrency Workbench and Sussex's Process Algebra
  1404.     Mauipulator are also ML systems of note, though neither are
  1405.     interactive theorem provers.
  1406.  
  1407.  
  1408. --------------------------------------------------------------------------
  1409.  
  1410. 8. Miscellaneous
  1411.  
  1412. Where can I find out about SML'97?  
  1413.  
  1414.  Look at:
  1415.     http://cm.bell-labs.com/cm/cs/what/smlnj/sml97.html
  1416.  
  1417.  
  1418. How do I write the Y combinator in SML without using a recursive
  1419. definition (i.e. "fun" or "let rec")?
  1420.  
  1421.  datatype 'a t = T of 'a t -> 'a
  1422.  
  1423.  val y = fn f => (fn (T x) => (f (fn a => x (T x) a)))
  1424.                    (T (fn (T x) => (f (fn a => x (T x) a))))
  1425.  
  1426.  
  1427. Where can I find an X-Windows interface to SML?
  1428.  
  1429.  Poly/ML, Poplog/ML, MLWorks and SML/NJ all come with X-Windows
  1430.  interfaces.  See the appropriate entries under section 3.  In
  1431.  addition, Poly/ML interfaces to the industry standard OSF/Motif
  1432.  toolkit.
  1433.  
  1434.  
  1435. How do I call a C function from SML/NJ?
  1436.  
  1437.  The new versions of SML/NJ provide much better support for calling
  1438.  out to C than version 93 did.  There is a discussion of how to use
  1439.  the C function interface off of the SML/NJ web page at
  1440.  http://cm.bell-labs.com/cm/cs/what/smlnj/doc/SMLNJ-C/index.html
  1441.  
  1442.  
  1443. Where can I find an emacs mode for SML?
  1444.  
  1445.  Look in the "Contributed Software" section of the SML/NJ distribution
  1446.  page at http://cm.bell-labs.com/cm/cs/what/smlnj/software.html
  1447.  
  1448.  Nowadays sml-mode works well with Emacs 19 and XEmacs 19, as well as
  1449.  a number of different SML compilers.
  1450.  
  1451.  Stefan Monnier has released a new version (3.9.3) with a number of
  1452.  changes, including improvements to the indentation algorithm.  The
  1453.  new version is available at
  1454.  ftp://rum.cs.yale.edu/pub/monnier/sml-mode
  1455.  
  1456. What is the value restriction?
  1457.  
  1458.  The value restriction is a feature of SML '97 which was introduced to
  1459.  address some issues with polymorphism in the presence of effects.
  1460.  The basic idea is that when a variable is bound to a polymorphic
  1461.  expression, it must be the case that the expression is tantamount to
  1462.  a value: that is, that it is guaranteed not to raise an exception or
  1463.  allocate memory.  For the purposes of typechecking, the class of
  1464.  values is conservatively approximated by the syntactic notion of
  1465.  "non-expansiveness".
  1466.  
  1467.  Values (non-expansive expressions) are:
  1468.  
  1469.   - functions
  1470.   - constants
  1471.   - variables
  1472.   - records of values
  1473.   - constructors applied to values
  1474.  
  1475.  So for example, while in the following code f has type 'a -> 'b -> 'b,
  1476.  g cannot be given the type 'b -> 'b because of the value restriction.
  1477.  
  1478.   fun f x y = y
  1479.   val g = f 3
  1480.  
  1481.  The expression (f 3) is polymorphic (at type 'b -> 'b) but is not a
  1482.  value, and so the value restriction forbids g from being bound
  1483.  polymorphically.  Either the code will be rejected, or g will be
  1484.  given a useless "dummy" type.
  1485.  
  1486.  In practice, this is usually easy to get around by eta-expanding:
  1487.  
  1488.   fun f x y = y
  1489.   val g = fn x => f 3 x
  1490.  
  1491.  More information on the value restriction is available from a number
  1492.  of sources, in particular:
  1493.  
  1494.   - Section 4.7 of "The Definition of Standard ML".  (see above)
  1495.  
  1496.   - Pages 321-326 of Paulson's "ML for the working programmer".  (see
  1497.     above)
  1498.  
  1499.   - http://cm.bell-labs.com/cm/cs/what/smlnj/doc/Conversion/types.html#Value
  1500.     This includes discussion of the particulars of SML/NJ's treatment
  1501.     of the value restriction.
  1502.  
  1503.   - Extensive discussion in the comp.lang.ml archives.
  1504.  
  1505.  
  1506. What is the difference between OCaml and Standard ML?
  1507.  
  1508.   Jen Olsson has created a small chart comparing the OCaml and
  1509.   Standard ML syntax: see
  1510.     http://www.csd.uu.se/~jenso/programming/sml_vs_ml.txt .
  1511.  
  1512.   An extended version written by Andreas Rossberg can be found at
  1513.     http://www.ps.uni-sb.de/~rossberg/SMLvsOcaml.html
  1514.   In addition to the original page it covers modules, records, and
  1515.   some more stuff.
  1516.