home *** CD-ROM | disk | FTP | other *** search
/ Usenet 1994 January / usenetsourcesnewsgroupsinfomagicjanuary1994.iso / answers / meta-lang-faq < prev    next >
Text File  |  1993-11-24  |  35KB  |  887 lines
  1. Newsgroups: comp.lang.ml,comp.answers,news.answers
  2. Path: senator-bedfellow.mit.edu!bloom-beacon.mit.edu!noc.near.net!das-news.harvard.edu!honeydew.srv.cs.cmu.edu!news
  3. From: jgmorris@cs.cmu.edu (Greg Morrisett)
  4. Subject: Comp.Lang.ML FAQ [Monthly Posting]
  5. Message-ID: <CH01Az.Gow.3@cs.cmu.edu>
  6. Followup-To: poster
  7. Summary: This posting contains a list of Frequently asked questions (and their
  8.          answers) about the family of ML programming languages, including 
  9.          Standard ML, CAML, Lazy-ML, and CAML-Light.  This post should be read 
  10.          before asking a question on the comp.lang.ml newsgroup.
  11. Originator: jgmorris@VACHE.VENARI.CS.CMU.EDU
  12. Sender: jgmorris@cs.cmu.edu
  13. Nntp-Posting-Host: vache.venari.cs.cmu.edu
  14. Reply-To: comp-lang-ml-request@cs.cmu.edu
  15. Organization: School of Computer Science, Carnegie Mellon
  16. Date: Wed, 24 Nov 1993 13:54:35 GMT
  17. Approved: comp-lang-ml@cs.cmu.edu
  18. Expires: Fri, 24 Dec 1993 00:00:00 GMT
  19. Lines: 865
  20. Xref: senator-bedfellow.mit.edu comp.lang.ml:251 comp.answers:2793 news.answers:15062
  21.  
  22. Archive-name: meta-lang-faq
  23. Last-modified: 1993/10/29
  24.  
  25.  
  26.          COMP.LANG.ML Frequently Asked Questions and Answers 
  27.        (compiled by Dave Berry and Greg Morrisett)
  28.  
  29. Please send corrections, additions, or comments regarding this list to
  30. comp-lang-ml-request@cs.cmu.edu.  
  31.  
  32. Changes since last month:
  33. ------------------------
  34. - Added SML/NJ FAQ info for MS-DOS/MS-Windows port.
  35. - Added access for individual posts to archives.
  36. - Added Paul Black's summary of theorem provers & ML
  37. - Added SML/NJ Linux info.
  38. - Added SML/NJ OS/2 info.
  39. - Expanded contents.
  40.  
  41. Contents:
  42. ---------
  43.     1. What is ML?
  44.     2. Where is ML discussed?
  45.         a. Comp.Lang.ML
  46.         b. SML-LIST
  47.         c. CAML-LIST
  48.     3. What implementations of ML are available?
  49.         a. quick summary (by machine/OS)
  50.         b. Poly/ML
  51.         c. Standard ML of New Jersey
  52.         d. Poplog ML
  53.         e. ANU ML
  54.         f. MicroML
  55.         g. sml2c
  56.         h. Caml Light
  57.         i. ML Kit Compiler
  58.     4. Unsupported SML/NJ Ports
  59.         a. MS-DOS/Windows
  60.         b. Linux
  61.         c. OS/2
  62.         5. Where can I find documentation on ML?
  63.         a. The Definition
  64.         b. Textbooks
  65.     6. Where can I find ML library code?
  66.     7. Theorem Provers and ML
  67.         8. Miscellaneous Questions
  68.         a. How do I write the Y combinator in SML?
  69.         b. Where can I find an X-windows interface to SML?
  70.         c. How do I call a C function from SML/NJ?
  71.  
  72. --------------------------------------------------------------------------
  73. 1. What is ML?
  74.  
  75.   ML (which stands for Meta-Language) is a family of advanced programming 
  76.   languages with [usually] functional control structures, strict semantics, 
  77.   a strict polymorphic type system, and parametrized modules.  It includes 
  78.   Standard ML, Lazy ML, CAML, CAML Light, and various research languages.  
  79.   Implementations are available on many platforms, including PCs, mainframes,
  80.   most models of workstation, multi-processors and supercomputers.  ML has 
  81.   many thousands of users, is taught at many universities (and is the first
  82.   programming language taught at some).
  83.  
  84. --------------------------------------------------------------------------
  85. 2. Where is ML discussed?
  86.  
  87. COMP.LANG.ML
  88. ------------
  89. comp.lang.ml is a moderated usenet newsgroup.  The topics for discussion
  90. include but are not limited to:
  91.  
  92.    * general ML enquiries or discussion 
  93.    * general interpretation of the definition of Standard ML 
  94.    * applications and use of ML 
  95.    * announcements of general interest (e.g. compiler releases)
  96.    * discussion of semantics including sematics of extensions based on ML
  97.    * discussion about library structure and content
  98.    * tool development
  99.    * comparison/contrast with other languages
  100.    * implementation issues, techniques and algorithms including extensions
  101.        based on ML
  102.  
  103. Requests should be sent to:
  104.  
  105.     comp-lang-ml@cs.cmu.edu
  106.  
  107. Administrative mail should be sent to:
  108.  
  109.     comp-lang-ml-request@cs.cmu.edu
  110.  
  111. Messages sent to the newsgroup are archived at CMU.  The archives can be
  112. retrieved by anonymous ftp from internet sites.  Messages are archived
  113. on a year-to-year basis.  Previous years' messages are compressed using
  114. the Unix "compress" command.  The current year's messages are not
  115. compressed.
  116.  
  117.     ftp pop.cs.cmu.edu
  118.     username: anonymous
  119.     password: <username>@<site>
  120.     binary
  121.     cd /usr/jgmorris/sml-archive
  122.     get sml-archive.<year>.Z
  123.     quit
  124.     zcat sml-archive.<year>.Z
  125.  
  126. (Pop's IP address is 128.2.205.205).
  127.  
  128. Individual messages can also be accessed in the directories
  129. /usr/jgmorris/mh-sml-archive/<year>-sml.
  130.  
  131. SML-LIST
  132. --------
  133. The SML-LIST is a mailing list that exists for people who cannot
  134. (or do not want to) read the Usenet COMP.LANG.ML newsgroup. 
  135. Messages are crossposted from COMP.LANG.ML to the SML-LIST and
  136. vice-versa.  You should ask to join the SML-LIST _only if_ you cannot
  137. (or do not want to) read the Usenet COMP.LANG.ML newsgroup.
  138.  
  139. To send a message to the SML-LIST distribution, address it to:
  140.  
  141.     sml-list@cs.cmu.edu
  142.  
  143. (sites not connected to the Internet may need additional routing.)
  144.  
  145. Administrative mail such as requests to add or remove names from the
  146. distribution list should be addressed to 
  147.  
  148.     sml-list-request@cs.cmu.edu
  149.  
  150.  
  151. CAML-LIST
  152. ---------
  153. The Caml language, a dialect of ML, is discussed on the Caml mailing
  154. list.  To send mail to the Caml mailing list, address it to:
  155.  
  156.     caml-list@margaux.inria.fr
  157.  
  158. Administrative mail should be addressed to:
  159.  
  160.     caml-list-request@margaux.inria.fr
  161.  
  162. ALT.LANG.ML
  163. -----------
  164. Another venue for ML-related discussion is the Netnews group
  165. alt.lang.ml, though this has seen relatively little traffic.  
  166. --------------------------------------------------------------------------
  167. 3. What implementations of ML are available and where can I find them?
  168.    (Note, this information may be out of date.)
  169.  
  170. Quick Summary:
  171.  
  172. System    full SML?  contact                        Platforms
  173. ------    ---------  ------------                 ------------------------------
  174. Poly/ML       yes       ahl@ahl.co.uk                Unix/Sparc,Sun3 (others soon)
  175.  
  176. SML/NJ       yes     dbm@resarch.att.com             Unix/Sparc,Mips,Vax,680x0,
  177.            ftp research.att.com             I386/486,HPPA,RS/6000,
  178.                          MacOS/MacII
  179.            ftp.rz.uni-karlsruhe.de     Linux (including binaries)
  180.            ftp-os2.nmsu.edu         OS/2  (including binearies)
  181.            
  182.  
  183. PoplogML   yes       isl@integ.uucp,             VMS/Vax, Unix/Vax,Suns,Sparcs,
  184.            alim@uk.ac.sussex.cogs,       Solbourne, Sequent Symmetry,
  185.            pop@cs.umass.edu             HP M680?0, Apollo, AUX/MacII
  186.  
  187. Edinburgh  core       ftp ftp.dcs.ed.ac.uk             32-bit machines (bytecode)
  188.            ftp ftp.informatik.uni-muenchen.de PC 80386SX+
  189.  
  190. ANU ML       core    mcn@anucsd.anu.edu.au     Sun-3, Ultrix/Vax, Pyramid,
  191.                          AUX/MacII
  192.  
  193. MicroML       core    olof or mahler @cs.umu.se     PC 80286+ (bytecode)
  194.            ftp ftp.cs.umu.se
  195.  
  196. sml2c       yes       dtarditi@cs.cmu.edu         32-bit Unix machines (C code)
  197.            ftp dravido.soar.cs.cmu.edu
  198.  
  199. Caml Light coreish caml-light@margaux.@inria.fr     32-bit Unix, Mac, PC 8086,
  200.            ftp ftp.inria.fr         PC 80386 (bytecode)
  201.  
  202. Kit       yes       ftp ftp.diku.dk         (Requires another SML compiler
  203.            ftp ftp.dcs.ed.ac.uk          to build binaries)
  204.  
  205. Details:
  206.                
  207. Poly/ML:
  208.     Poly/ML produces native code for SPARC and Sun3
  209. systems.  Poly/ML uses a persistent store and supports arbitrary precision
  210. integer arithmetic.  It comes with a make system, an X11/Xlib interface,
  211. and a OSF/Motif interface.  Non-standard extensions include concurrent 
  212. processes and an associated message-passing scheme.
  213.     Poly/ML is distributed by Abstract Hardware Ltd. (ahl@ahl.co.uk).
  214. The price of the Motif edition is 1250 pounds for an academic site 
  215. licence or 3300 pounds per machine for commercial users.  Multiple
  216. and site licences are available by negotiation.
  217.  
  218. Standard ML of New Jersey:
  219.         Standard ML of New Jersey was developed jointly at AT&T Bell
  220. Laboratories and Princeton University.  It is an open system (source
  221. code is freely available) implemented in Standard ML.  Version 0.93 of
  222. SML/NJ generates native code for 68020, SPARC, and MIPS (big and
  223. little endian), I386/486, HPPA(HP9000/700), and RS/6000 architectures
  224. under various versions of the Unix operating system (SunOS, Ultrix,
  225. Mach, Irix, Riscos, HPUX, AIX, AUX, etc.), and on the MacIntosh OS
  226. (Mac II, System 7.x, min 12MB ram).  Version 0.75 runs on the Vax
  227. under Ultrix, BSD, and Mach.
  228.     SML/NJ comes with a source-level debugger, profiler, gnu emacs
  229. interface, ML implementations of LEX, YACC, and Twig, separate compilation
  230. facilities, Concurrent ML, the eXene X Window library, and the SML/NJ
  231. library.  It runs interactively and can produce stand-alone executable
  232. applications.
  233.     Non-standard extensions include typed first-class continuations,
  234. Unix signal handling, and higher-order functors.
  235.         SML/NJ is copyrighted by AT&T but the system, including source
  236. code, is freely distributable.  It is available by anonymous ftp from
  237. research.att.com (192.20.225.2) and princeton.edu (128.112.128.1).
  238. Login as "anonymous" with your user name as password.  Put ftp in
  239. binary mode and copy the (compressed tar) files you need from the
  240. directory dist/ml (pub/ml on princeton.edu).  You only need the 93.mo.*.tar.Z 
  241. files for your machine in addition to the 93.src.tar.Z.  (You might also 
  242. want the 93.release-notes.[ps|txt], 93.tools.tar.Z, 93.doc.tar.Z, and 
  243. smlnj-lib-0.1.tar.Z files.)  Alternatively mail dbm@research.att.com.  
  244. In the UK, SML/NJ is available from the LFCS.
  245.     There are unsupported ports of SML/NJ to other platforms, including
  246. Linux, OS/2, and Microsoft Windows 3.1.  See the "Unsupported SML/NJ Ports" 
  247. section for details.
  248.  
  249. Poplog ML:
  250.         Standard ML is supported as part of the Poplog system, which also
  251. provides incremental compilers for Pop-11, Common Lisp and Prolog in a
  252. common environment with shared data-structures, so that mixed language
  253. programming is possible. The integrated editor and HELP mechanism
  254. support online teaching aids.  Poplog comes with an X Windows interface.
  255.     Poplog is available for VAX+VMS, VAX+Ultrix, VAX+Bsd 4.2/3,
  256. Sun-2,3,4, Sun386i, SPARCstation, Solbourne, Sequent Symmetry (with Dynix),
  257. HP M680?0+Unix workstations and Apollo+Unix. Versions for MAC-II with A/UX,
  258. DECstation 3100 and MIPS will be available shortly.
  259.         UK educational users should contact the School of Cognitive and
  260. Computing Sciences, University of Sussex (alim@uk.ac.sussex.cogs).  People in
  261. the USA or Canada should contact Computable Functions Inc. (pop@cs.umass.edu).
  262. All others should contact Integral Solutions Ltd. (isl@integ.uucp).  UK
  263. academic prices start at 600 pounds.  Non-UK academic prices start at 1125
  264. pounds.  Commercial prices start around 2,000 pounds for an ML-only version
  265. or 7,500 pounds for the full Poplog system.
  266.  
  267. Edinburgh ML 4.0:
  268.     Edinburgh ML 4.0 is an implementation of the core language (without
  269. the module system).  It uses a bytecode interpreter, which is written in C
  270. and runs on any machine with 32 bit words, a continuous address space and
  271. a correct C compiler.  Ports to various 16 bit machines are underway.  The
  272. bytecode interpreter can be compiled with switches to avoid the buggy parts
  273. of the C compilers that we've used it with (as far as I know none of them
  274. worked correctly).  
  275.     Edinburgh ML 4.0 is available from the LFCS.  
  276.     A port to PCs with 386SX processors or better is available by FTP
  277. from ftp.informatik.uni-muenchen.de, in the file pub/sml/ibmpc/edml3864.exe.
  278. Contact Joern Erbguth (jnerbgut@informatik.uni-erlangen.de) for more 
  279. information. 
  280.  
  281.  
  282. ANU ML
  283.     ANU ML is descended from Cardelli's ML Pose 3.  It implements the
  284. core language of the standard and an old version of modules.  It incrementally
  285. compiles to native code on Sun-3, Vax/Ultrix, Pyramid and MacII/AUX.  (It
  286. is intended to standardize modules and do the port to Sun-4 in the near
  287. future.)
  288.     ANU ML has a program development system with strong support for
  289. debugging (tracing, automatic retesting etc.) and has been extended with
  290. a built-in type complex.  
  291.     ANU ML is still considered to be in beta release since exceptions
  292. have been standardized quite recently.  It is available from Malcolm Newey,
  293. CS Dept., Australian National University (mcn@anucsd.anu.edu.au) by
  294. arrangement; soon to be available by ftp.
  295.  
  296. MicroML
  297.     MicroML is an interpreter for a subset of SML that runs on IBM PCs,
  298. from the Institute of Information Processing at the University of Umea in
  299. Sweden.  It implements the core language except for records.  A 80286
  300. processor or better is recommended.
  301.     MicroML is available as an alpha-release by anonymous ftp from
  302. ftp.cs.umu.se /pub/umlexe01.uue.  There are several known bugs in the current
  303. version.  For more information contact Olof Johansson (olof@cs.umu.se) or
  304. Roger Mahler (mahler@cs.umu.se).
  305.  
  306. sml2c
  307.     sml2c is a Standard ML to C compiler.  It is based on SML/NJ and
  308. shares its front-end and most of the runtime system. sml2c is a batch
  309. compiler and compiles only module-level declarations.  It does not support
  310. SML/NJ style debugging and profiling.
  311.     sml2c is easily portable and has been ported to IBM RT, 
  312. Decstation 3100, Decstation 5000, Omron Luna 88k, sun-3, sun-4 and a 
  313. 486-based machine (running Mach).  The generated code is highly portable 
  314. and makes very few assumptions about the target machine or the C compilers 
  315. available on the target machine. The runtime system, which it shares with 
  316. the SML/NJ has several machine and operating system dependencies.  sml2c 
  317. has eliminated some of these dependencies by using portable schemes for 
  318. garbage collection and for freezing and restarting programs.
  319.     sml2c is available by anonymous ftp from dravido.soar.cs.cmu.edu
  320. (128.2.220.26). Log in as anonymous, send username@node as password.  The
  321. compressed tar file sml2c.tar.Z can be found in /usr/nemo/sml2c.  The local
  322. ftp software will allow you to change directory only to /usr/nemo/sml2c.
  323. The size of the tar file is about 3 Meg. The size of the uncompressed
  324. distribution is about 12 Meg.
  325.  
  326. Caml Light
  327.  
  328. Caml Light is a portable, bytecode interpreter for a subset of CAML, 
  329. a dialect of ML.  Some features of Caml Light include separate compilation,
  330. streams and stream parsers, ability to link to C code, and tools for
  331. building libraries and toplevel systems.  The PC versions provide
  332. line editing and the 80386 port is VCPI-compliant.
  333.  
  334. The Unix version should work on any modern workstation. We have tested
  335. it on Sun 3 and 4, DecStations, HP 9000/700 and 9000/350, IBM RS/6000,
  336. SGI Indigo, Sony News, Next cubes, and some more exotic machines.
  337. The Macintosh version is now a standalone Macintosh application, and
  338. no longer requires the Macintosh Programmer's Workshop. (Well, at
  339. least for the toplevel environment; the batch compilers still run
  340. under MPW.) The application provides some graphics primitives.
  341. The PC version still comes in two flavors, one that run on any PC, but
  342. is severely limited by the 640K barrier, and one that run on 80386 or
  343. 80486 PC's in 32 bit protected mode to circumvent these limitations.
  344. Both versions now provide the same graphics primitives as the
  345. Macintosh version.  Ports to OS/2 and to the Amiga are in progress.
  346.  
  347. The version 0.6 of the Caml Light system has been released, and is
  348. available by anonymous FTP from:
  349.  
  350.         host:      ftp.inria.fr (192.93.2.54)
  351.  
  352.         directory: lang/caml-light
  353.  
  354.     Summary of the files:
  355.  
  356.         README                  More detailed summary
  357.         cl6unix.tar.Z           Unix version
  358.         cl6macbin.sea.hqx       Binaries for the Macintosh version
  359.         cl6macsrc.sea.hqx       Source code for the Macintosh version
  360.         cl6pc386bin.zip         Binaries for the 80386 PC version
  361.         cl6pc386src.zip         Source code for the 80386 PC version
  362.         cl6pc86bin.zip          Binaries for the 8086 PC version
  363.         cl6pc86src.zip          Source code for the 8086 PC version
  364.         cl6refman.*             Reference manual, in various formats
  365.         cl6tutorial.*           Tutorial, in various formats
  366.  
  367. This release is mostly a bug-fix release and should be compatible with
  368. Caml Light 0.5. The main changes are:
  369.  
  370. * Better handling of type abbreviations.
  371.  
  372. * Debugging mode (option -g to camlc and camllight) to get access
  373.   to the internals of module implementations.
  374.  
  375. * New library modules:
  376.     genlex    generic lexical analyser
  377.     set       applicative sets over ordered types
  378.     map       applicative maps over ordered types
  379.     baltree   balanced binary trees over ordered types
  380.  
  381. * "compile" command at toplevel (especially useful in the Macintosh version).
  382.  
  383. * New contributed libraries and tools:
  384.     camlmode    Emacs editing mode for Caml Light
  385.     mletags     Indexing of Caml Light source files for use with Emacs "tags"
  386.     search_isos Search libraries by types (modulo isomorphisms)
  387.     libgraph    X implementation of the portable graphics library
  388.     libnum      Arbitrary-precision arithmetic
  389.     libstr      String operations, regular expressions
  390.  
  391. * The 80386 PC version is now DPMI-compliant, hence it can run under Windows
  392.   (in text mode inside a DOS windows and with no graphics, though).
  393.  
  394. * More examples, including those from the book "Le langage Caml".
  395.  
  396. General questions and comments of interest to the Caml community
  397. should be sent to caml-list@margaux.inria.fr, the Caml mailing list.
  398. (see question 3 above for details.)
  399.  
  400. ML Kit Compiler
  401.  
  402.   The ML Kit is a straight translation of the Definition of Standard
  403. ML into a collection of Standard ML modules.  For example, every
  404. inference rule in the Definition is translated into a small piece of
  405. Standard ML code which implements it. The translation has been done
  406. with as little originality as possible - even variable conventions
  407. from the Definition are carried straight over to the Kit.
  408.  
  409.   If you are primarily interested in executing Standard ML programs
  410. efficiently, the ML Kit is not the system for you! (It uses a lot of
  411. space and is very slow.) The Kit is intended as a tool box for those
  412. people in the programming language community who may want a
  413. self-contained parser or type checker for full Standard ML but do not
  414. want to understand the clever bits of a high-performance compiler. We
  415. have tried to write simple code and module interfaces; we have not
  416. paid any attention to efficiency.
  417.  
  418.   The documentation is around 100 pages long and is provided with the
  419. Kit. It explains how to build, run, read and modify the Kit. It also
  420. describes how typing of flexible records and overloading are handled
  421. in the Kit.
  422.  
  423.   The ML Kit is written by Nick Rothwell, David N. Turner, Mads Tofte
  424. and Lars Birkedal at Edinburgh and Copenhagen Universities.
  425.    
  426.   The ML Kit is available via anonymous ftp. Here is a sample dialog:
  427.  
  428.   ftp ftp.diku.dk              ftp ftp.dcs.ed.ac.uk
  429.   Name: anonymous              Name: anonymous
  430.   Password: <your loginname@host>      Password: <your loginname@host>
  431.   ftp> binary                  ftp> binary
  432.   ftp> cd diku/users/birkedal          ftp> cd export/ml/mlkit
  433.   ftp> get README              ftp> get README
  434.   ftp> get COPYING              ftp> get COPYING
  435.   ftp> get src.tar.Z              ftp> get src.tar.Z
  436.   ftp> get doc.tar.Z              ftp> get doc.tar.Z
  437.   ftp> get tools.tar.Z          ftp> get tools.tar.Z
  438.   ftp> get examples.tar.Z          ftp> get examples.tar.Z
  439.   ftp> bye                  ftp> bye
  440.  
  441. The file README contains installation instructions. Note that no
  442. binaries are distributed and that you must build these using either
  443. Standard ML of New Jersey, or Poly/ML.
  444.  
  445.  
  446. --------------------------------------------------------------------------
  447. 6. Unsupported SML/NJ Ports
  448.  
  449. This section describes various ports of SML/NJ (see section 5) 
  450. that are not directly supported by the NJ folks.  
  451.  
  452. MS-DOS/Windows?
  453. ---------------
  454. (From Dave MacQueen)
  455.  
  456. There is an MS-Windows/MSDOS implementation of Standard ML of New
  457. Jersey available by annonymous ftp on research.att.com, directory
  458. dist/ml/working/sml-386.  This port was done by Yngvi Guttesen at the
  459. Danish Technical University in Copenhagen, and it is based on version
  460. 0.75 of SML/NJ.  The distribution consists of the following four
  461. files.
  462.  
  463. -rw-rw-r--  1  dbm     other    417 Feb 16  1993 README
  464. -rw-rw-r--  1  dbm     other  51375 Feb  7  1992 doc.tar.Z
  465. -rw-rw-r--  1  dbm     other 749105 May  5  1992 mo.386.tar.Z
  466. -rw-rw-r--  1  dbm     other 851445 Feb  7  1992 src.tar.Z
  467.  
  468. This Windows port is rather delicate, and when we got it we had a lot
  469. of trouble getting it working here at Bell labs.  We tried several
  470. different machines and finally found one on which it would run (a
  471. Gateway 2000 with 16 MB of RAM), though even then it was not very
  472. robust or fast.  It seemed to be a problem of finding a machine with
  473. just the right memory management configuration.  I must admit that
  474. memory management under Windows is a black art that I am not familiar
  475. with, so I have no idea how to characterize the required memory
  476. configuration.
  477.  
  478. My conclusion is that the current Windows 3.1/MSDOS environment is so
  479. difficult that it would require a major additional investment to have
  480. a really useful port.  Guttesen did not have a 32 bit C compiler
  481. available, so he rewrote the runtime system in assember, which makes
  482. it difficult to modify his port.  An alternative is to wait for
  483. Windows NT (Win32) or OS/2 ports, which may be done in the coming
  484. months (a couple of people have independently been working on OS/2
  485. ports recently).  Another alternative is to look in directory pub/ml
  486. of ftp.dcs.ed.ac.uk, where there are a couple of (partial)
  487. implementations of SML that run on PCs.  A third alternative is to
  488. look into Xavier Leroy's CAML Light.  (Details of these are in the
  489. comp.lang.ml FAQ message.)
  490.  
  491. However, Guttesen's 386 code generator was used by Mark Leone of CMU
  492. as the basis for a port to Unix on Ix86 machines.  The current release
  493. of SML of New Jersey (0.93) incorporates Intel/Unix support for Mach
  494. (used at Carnegie-Mellon University), BSD386 (a product of BSDI?), and
  495. 386bsd (a free version of Unix for the PC).  There are also versions
  496. that run under Linux (available as part of the free Linux distribution)
  497. and SVR4, although we have not yet integrated the code supporting
  498. Linux and SVR4 into the distributed 0.93 runtime system.  Interest has
  499. been expressed in a port for SCO Unix, but, as far as we know, no one
  500. has done such a port.
  501.  
  502. Very recently Peter Bertelsen of the Technical University of Denmark
  503. has done a port to OS2, which is now available on research.att.com,
  504. directory dist/ml.
  505.  
  506. Linux?
  507. ------
  508. (Thanks to Ralf Reetz, Peter Su, and Mark Leone)
  509.  
  510. Various ftp sites that seem to carry SML/NJ version 0.93 for Linux:
  511.  
  512.     ftp.rz.uni-karlsruhe.de:/linux/mirror.tsx/
  513.  
  514.         binaries/usr.bin/njsml.93.bin.z
  515.         sources/usr.bin/njsml.93.linux.README
  516.         sources/usr.bin/njsml.93.linux.README.NEW
  517.         sources/usr.bin/njsml.93.linux.diffs.z
  518.         sources/usr.bin/njsml.93.src.tar.z
  519.  
  520.     ftp@tsx-11.mit.edu:/pub/linux/
  521.  
  522.            sources/usr.bin/njsml.93.src.tar.z
  523.  
  524.     ftp.dcs.glasgow.ac.uk?
  525.  
  526. From the README file:
  527.  
  528.              Standard ML of New Jersey
  529.     Version 0.93 for the i386/i486 running Linux, April 23, 1993
  530.  
  531.  
  532. __ WHAT
  533.     SML/NJ is a compiler for the functional programming language
  534.     Standard ML (SML). It is a fairly complete and robust
  535.     implementation of ML.
  536.  
  537. __ FILES
  538.     njsml.93.bin.z - gzip'd binary of njsml (no SourceGroup)
  539.     njsml-sg.93.bin.z - gzip'd binary of njsml with SourceGroup
  540.     njsml.93.src.tar.z - minimal sources for NJSML on Linux
  541.     njsml.93.mo.i386.z - you'll need these also to compile on Linux
  542.  
  543.     You can pick up additional tools and goodies from:
  544.  
  545.     research.att.com
  546.  
  547.     under the "ml" directory.
  548.  
  549. __ HISTORY
  550.  
  551.     This is a port of Standard ML of New Jersey (SML/NJ) to Linux. It
  552.     is based on the work of Mark Leone (mleone@cs.cmu.edu) who did
  553.     the port for i386/i486 machines. The current binary was compiled
  554.     using Linux 0.99.7a.  Shared lib 4.3.3.
  555.  
  556.     This port was done by Sanford Barr (sbarr@cs.sunysb.edu) based on
  557.         the original port of 0.91 by Hermano Moura (moura@dcs.glasgow.ac.uk)
  558.     and Andre Santos (andre@dcs.glasgow.ac.uk).
  559.  
  560. __ RECOMMENDED ENV
  561.  
  562.     16M of ram is suggested if you wish to do anything serious with
  563.     the system.  Also, a 386-40 or better would be helpful.
  564.  
  565.  
  566. __ KNOWN BUGS AND DEFICIENCIES
  567.  
  568.     1 Some minimal precision problems exist when a 387 emulator is
  569.       used.
  570.  
  571.     2 ML functions System.Directory.listDir and System.Directory.getWD
  572.       not working at the moment.
  573.  
  574. __ WHERE
  575.  
  576.     NJ-SML 0.93 should be available at most major Linux sites.  It
  577.     should also be available in:
  578.         sbcs.sunysb.edu:/pub/linux
  579.     by the time you are reading this.
  580.  
  581. OS/2:
  582. -----
  583. Standard ML of New Jersey (version 0.93) has been ported to PC's running OS/2.
  584. Signal handling is not implemented. This port has been implemented using Mark
  585. Leone's code generator for Intel 80386 and the Unix emulator emx, copyright of
  586. Eberhard Mattes. SML/NJ is copyright of AT&T Bell Laboratories.
  587. There is no warranty of any kind!
  588.  
  589. Requirements:
  590.  - IBM OS/2 version 2.x
  591.  - HPFS file system (long file names required)
  592.  - emx version 0.8g or later
  593.  - '.mo' files for i386
  594.  
  595. The port is available for anonymous ftp from research.att.com (in /dist/ml)
  596. and, in Europe, from ftp.id.dth.dk (in /pub/bertelsen):
  597.  
  598.    93.os2port.zip     Archived with Info-ZIP's Zip utility
  599.    93.os2port.tar.Z   Archived with GNU's tape archive utility
  600.    93.os2port.txt     Port announcement & installation guide
  601.  
  602. Please note that the .tar.Z and .zip version of the SML/NJ port are exactly
  603. alike and both contain a full source set (but no '.mo' files) for compiling 
  604. to OS/2 with emx/gcc (not included).
  605.  
  606. The i386 '.mo' archive (93.mo.i386.tar.Z) is available from research.att.com
  607. (in /dist/ml) and princeton.edu (in /pub/ml). The emx environment is available
  608. from various OS/2 related ftp sites, e.g. ftp-os2.cdrom.com.
  609.  
  610. A binary-only release of this SML/NJ port (no source, interactive system
  611. executable only) is also available for anonymous ftp from ftp-os2.cdrom.com.
  612.  
  613. If you have questions concerning this port, please send email to:
  614.  
  615. Peter Bertelsen  (c917023@id.dth.dk)
  616. Department of Computer Science, Technical University of Denmark
  617. --------------------------------------------------------------------------
  618. 5. Where can I find documentation on SML?
  619.  
  620. THE DEFINITION.
  621.  
  622. Robin Milner, Mads Tofte and Robert Harper
  623. The Definition of Standard ML
  624. MIT, 1990.
  625. ISBN: 0-262-63132-6
  626.  
  627. Robin Milner and Mads Tofte
  628. Commentary on Standard ML
  629. MIT, 1991
  630. ISBN: 0-262-63137-7
  631.  
  632. TEXTS.
  633.  
  634. Jeffrey D. Ullman
  635. Elements of ML Programming
  636. Prentice-Hall, 1993 (Oct. 15)
  637. ISBN: 0-13-184854-2
  638. (See Comp.Lang.ML archives, message from Ullman dated 22 Sep 1993 for
  639.  chapter headings.)
  640.  
  641. Rachel Harrison
  642. Abstract Data Types in Standard ML
  643. John Wiley & Sons, April 1993
  644. ISBN: 0-471-938440
  645.  
  646. Ake Wikstrom
  647. Functional Programming Using Standard ML
  648. Prentice Hall 1987
  649. ISBN: 0-13-331661-0
  650.  
  651. Chris Reade
  652. Elements of Functional Programming
  653. Addison-Wesley 1989
  654. ISBN: 0-201-12915-9
  655.  
  656. Lawrence C Paulson
  657. ML for the Working Programmer
  658. Cambridge University Press 1991
  659. ISBN: 0-521-39022-2
  660.  
  661. Stefan Sokolowski
  662. Applicative High Order Programming: The Standard ML perspective
  663. Chapman & Hall 1991
  664. ISBN: 0-412-39240-2     0-442-30838-8 (USA)
  665.  
  666. Ryan Stansifer
  667. ML Primer
  668. Prentice Hall, 1992
  669. ISBN 0-13-561721-9
  670.  
  671. Colin Myers, Chris Clack, and Ellen Poon
  672. Programming with Standard ML
  673. Prentice Hall, 1993
  674. ISBN 0-13-722075-8 (301pp)
  675.  
  676. The following report is available from the LFCS (Lorraine Edgar,
  677. lme@dcs.ed.ac.uk) and costs 5 pounds or 10 US dollars.  It covers all of
  678. Standard ML.
  679.  
  680. Robert Harper
  681. Introduction to Standard ML
  682. LFCS Report Series  ECS-LFCS-86-14
  683. Laboratory for Foundations of Computer Science
  684. Department of Computer Science
  685. University of Edinburgh
  686. Nov. 1986 (revised Jan. 1989 by Nick Rothwell and Kevin Mitchell)
  687.  
  688. The following report is available from the LFCS (Lorraine Edgar,
  689. lme@dcs.ed.ac.uk) and costs 2.50 pounds or 5 US dollars for single
  690. copies and 1.50 pounds or 3 dollars when bought in bulk.  It includes
  691. an introduction to Standard ML and 3 lectures on the modules system.
  692.  
  693. Mads Tofte
  694. Four Lectures on Standard ML
  695. LFCS Report Series  ECS-LFCS-89-73
  696. Laboratory for Foundations of Computer Science
  697. Department of Computer Science
  698. University of Edinburgh
  699. March 1989
  700.  
  701. The following report is available from the LFCS (Lorraine Edgar,
  702. lme@dcs.ed.ac.uk) and is free.  It introduces Extended ML, a language
  703. for writing (non-executable) specifications of Standard ML programs and
  704. for formally developing Standard ML programs from such specifications.
  705.  
  706. Don Sannella
  707. Formal program development in Extended ML for the working programmer.
  708. LFCS Report Series  ECS-LFCS-89-102
  709. Laboratory for Foundations of Computer Science
  710. Department of Computer Science
  711. University of Edinburgh
  712. December 1989
  713. --------------------------------------------------------------------------
  714. 6. Where can I find library code?
  715.  
  716. The Edinburgh SML Library provides a consistent set of functions on the
  717. built-in types of the language and on vectors and arrays, and a few extras.
  718. It includes a "make" system and a consistent set of parsing and unparsing
  719. functions.  The library consists of a set of signatures with sample portable
  720. implementations, full documentation, and implementations for Poly/ML,
  721. Poplog ML and SML/NJ that use some of the non-standard primitives
  722. available in those systems.  It is distributed with Poly/ML, Poplog ML and
  723. Standard ML of New Jersey.  It is also available from the LFCS.
  724.  
  725. The library documentation is available as a technical report from the LFCS
  726. (Lorraine Edgar, lme@dcs.ed.ac.uk) and costs 5 pounds or 10 US dollars.
  727. The LaTeX source of the report is included with the library.
  728.  
  729. Dave Berry
  730. The Edinburgh SML Library
  731. LFCS Report Series  ECS-LFCS-91-148
  732. Laboratory for Foundations of Computer Science
  733. Department of Computer Science
  734. University of Edinburgh
  735. April 1991
  736.  
  737.  
  738. The SML/NJ Library is distributed with the SML of New Jersey compiler.
  739. It provides a variety of utilities such as 2-dimensional arrays, sorting,
  740. sets, dictionaries, hash tables, formatted output, Unix path name
  741. manipulation, etc.  The library compiles under SML/NJ but should
  742. be mostly portable to other implementations.
  743.  
  744. --------------------------------------------------------------------------
  745. 7. Theorem Provers and ML
  746.  
  747. (Collected by Paul Black, pblack@cs.berekeley.edu.  Thanks Paul!)
  748.  
  749. - LCF (Edinburgh LCF and Cambridge LCF)
  750.     * written in the original Edinburgh dialect of ML from which SML developed.
  751.  
  752.    "Logic and Computation: Interactive Proof with Cambridge LCF"
  753.     also by Lawrence C. Paulson.
  754.  
  755.  
  756. - Lego (LFCS, Edinburgh Univ., SML)
  757.     * written in the original Edinburgh dialect of ML from which SML
  758.     developed.
  759.     * only higher-order resolution
  760.  
  761. - HOL90 (Konrad Slind, TU Munich)
  762.     * reimplementation of HOL in SML
  763.  
  764.     * freely available; ftp from Munich
  765.  
  766.     * HOL90 has lots of decision procedures, and lots of rewriting.
  767.     In general, HOL90 has LOTS of automated support.  But it
  768.     doesn't have dependent types (if one cares about those things).
  769.  
  770. - NuPrl (from Bob Constable`s group at Cornell)
  771.  
  772. - Isabelle (Lawrence C. Paulson, Cambridge Univ. )
  773.     * has rewriting, but not many decision procedures.  It does has
  774.     things like model elimination-based decision procedures.
  775.     * a generic automatic theorem prover i.e. you can program it to
  776.     the logic system/proof system you want.  Already has the
  777.     following subsystems already implemented:
  778.         i) FOL - first order logic
  779.         ii) HOL - higher order logic
  780.         iii) LCF - Logic of computable functions
  781.         iv) LK - Gentzen system LK
  782.         v) Modal - Modal logic systems T, S4, S43
  783.         vi) ZF - Zermelo-Fraenkel set theory
  784.     * ftp from <gannet.cl.cam.ac.uk>
  785.  
  786. - MERILL (Brian Matthews, U. of Glasgow & Rutherford Appleton Laboratory)
  787.     * written in standard ML
  788.     * a general purpose order-sorted equational reasoning system
  789.     * Allows the user to declare their own object language, allows
  790.     AC-rewriting and AC-unification of terms and equations, has
  791.     several completion algorithms, is built on a hierarchy of
  792.     types known as Order-Sorting, and allows the user to try
  793.     different termination methods.
  794.     * available via anonymous ftp from the University of Glasgow,
  795.     ftp address: ftp.dcs.glasgow.ac.uk (130.209.240.50)
  796.     * Brian Matthews, brian@dcs.glasgow.ac.uk or bmm@inf.rl.ac.uk
  797.  
  798. - FAUST (Karlsruhe)
  799.     * a HOL add-on written in ML.
  800.     * ftp from goethe.ira.uka.de (129.13.18.22)
  801.  
  802. - Alf
  803.     * written in SML
  804.     * only higher-order resolution
  805.  
  806. - Coq
  807.     * written in Caml-Light (but Caml-Light and SML are VERY similar)
  808.     * no serious automated reasoning subsystems (other than
  809.     higher-order resolution), but has a VERY nice package for
  810.     program verification.
  811.     * possible contact: Chet Murthy <murthy@cs.cornell.edu>
  812.  
  813. - ICLHOL/ProofPower (ICL Secure Systems)
  814.     * a commercial system using a reimplementation of HOL in SML
  815.     * contact ProofPower-server@win.icl.co.uk
  816.  
  817. - Lamdba/DIALOG (Abstract Hardware Ltd)
  818.     * a commercial tool written in Poly/ML, neither of which is free.
  819.  
  820. - Elf (Frank Pfenning, Carnegie Mellon Univ.)
  821.    * Elf is a higher-order logic programming language based on the LF
  822.     Logical Framework.
  823.    * Elf is not a theorem prover per-se, but is useful for specifying
  824.     and proving properties of programming languages, logics, and their
  825.     implementations.  A number of examples are provided with the
  826.     distribution.
  827.    * The Elf implementation is written in SML/NJ and should be easily
  828.         portable to other SML implementations.
  829.    * Elf can be ftp'd from alonzo.tip.cs.cmu.edu (128.2.209.194)
  830.     in the directory /afs/cs/user/fp/public.
  831.    * A bibliography and a collection of papers regarding LF and Elf
  832.         can be found in the directory /afs/cs/user/fp/public/elf-papers.
  833.    * There is an Elf mailing list.  Contact elf-request@cs.cmu.edu to join.
  834.    * For further information, contact Frank Pfenning (fp@cs.cmu.edu).
  835.  
  836. References
  837.    "ML for the Working Programmer" by Lawrence C. Paulson contains a
  838.     small first-order theorem prover.
  839.  
  840.     Paulson also has a good chapter on writing theorem provers in ML in
  841.     "Handbook of logic in computer science",
  842.     Edited by:  S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum.
  843.     Oxford : Clarendon Press, 1992-.
  844.     CALL#: QA76 .H2785 1992 
  845.  
  846.    
  847. Others
  848.     We have an automated theorm proving system here at the University
  849.     of Tasmania, but it is still under development, currently
  850.     riddled with bugs and has an obscure "input language"; aside
  851.     from those minor problems, it'd be perfect...
  852.     La Monte H. Yarroll <piggy@hilbert.maths.utas.edu.au>
  853.  
  854.     Edinburgh's Concurrency Workbench and Sussex's Process Algebra
  855.     Mauipulator are also ML systems of note, though neither are
  856.     interactive theorem provers.
  857.  
  858.  
  859. --------------------------------------------------------------------------
  860. 8. Miscellaneous
  861.  
  862. How do I write the Y combinator in SML without using a recursive
  863. definition (i.e. "fun" or "let rec")?
  864.  
  865.     datatype 'a t = T of 'a t -> 'a
  866.  
  867.     val y = fn f => (fn (T x) => (f (fn a => x (T x) a)))
  868.                          (T (fn (T x) => (f (fn a => x (T x) a))))
  869.  
  870. Where can I find an X-Windows interface to SML?
  871.  
  872.     Poly/ML, Poplog/ML, and SML/NJ all come with X-Windows interfaces.
  873.     See the appropriate entries under section 3.  In addition, Poly/ML
  874.     interfaces to the industry standard OSF/Motif toolkit.
  875.  
  876. How do I call a C function from SML/NJ?
  877.  
  878. See the file runtime/cfuns.c for example C functions that are in
  879. the runtime and callable from ML.  You have to enter the function
  880. into a table at the end of the file along with a string.  You use
  881. the function System.Unsafe.CInterace to look up the function, using
  882. the string as the key.  Note that you'll need to convert ML values
  883. to C representations and back.  You'll have to rebuild the compiler
  884. using makeml.
  885.  
  886.     
  887.