Internet Info 1997 December

home *** CD-ROM | disk | FTP | other *** search

/ Internet Info 1997 December / Internet_Info_CD-ROM_Walnut_Creek_December_1997.iso / faqs / comp / answers / meta-lang-faq < prev next >

Wrap

Internet Message Format | 1997-10-02 | 50.8 KB

Path: senator-bedfellow.mit.edu!bloom-beacon.mit.edu!news-out.internetmci.com!newsfeed.internetmci.com!4.1.16.34!cpk-news-hub1.bbnplanet.com!news.bbnplanet.com!portc02.blue.aol.com!pitt.edu!newsfeed.pitt.edu!bb3.andrew.cmu.edu!honeysuckle.srv.cs.cmu.edu!goldenapple.srv.cs.cmu.edu!rowan From: rowan@cs.cmu.edu (Rowan Davies) Newsgroups: comp.lang.ml,comp.answers,news.answers Subject: Comp.Lang.ML FAQ [Monthly Posting] Followup-To: poster Date: 1 Oct 1997 15:34:43 GMT Organization: Carnegie Mellon Univ. -- Computer Science Dept. Lines: 1306 Sender: rowan@cs.cmu.edu Approved: comp-lang-ml@cs.cmu.edu Expires: Tue, 4 Nov 1997 00:00:00 GMT Message-ID: <60tqij$6k4$1@goldenapple.srv.cs.cmu.edu> Reply-To: comp-lang-ml-request@cs.cmu.edu NNTP-Posting-Host: kurt.tip.cs.cmu.edu Summary: This posting contains a list of Frequently asked questions (and their answers) about the family of ML programming languages, including Standard ML, CAML, Lazy-ML, and CAML-Light. This post should be read before asking a question on the comp.lang.ml newsgroup. Originator: rowan@kurt.tip.cs.cmu.edu Xref: senator-bedfellow.mit.edu comp.lang.ml:2188 comp.answers:28320 news.answers:113580 Archive-name: meta-lang-faq Last-modified: 1997/08/07 COMP.LANG.ML Frequently Asked Questions and Answers (compiled by Dave Berry and Greg Morrisett) (maintained by Rowan Davies) Please send corrections, additions, or comments regarding this list to comp-lang-ml-request@cs.cmu.edu. Changes since last month: - None Contents: --------- 1. What is ML? 2. Where is ML discussed? a. Comp.Lang.ML b. SML-LIST c. CAML-LIST 3. What implementations of ML are available? a. quick summary (by machine/OS) b. Standard ML of New Jersey (SML/NJ) c. sml2c d. Caml Light e. Objective Caml f. Bigloo g. Camlot h. Moscow ML i. ML Kit j. Edinburgh k. MicroML l. Poly/ML m. Poplog ML n. MLWorks 4. Unsupported SML/NJ Ports a. Linux b. OS/2 c. FreeBSD d. NEXTSTEP e. SVR4 5. Where can I find documentation/information on ML? a. The Definition b. Textbooks c. Information on the Internet 6. Where can I find ML library code? a. The Standard ML ('97) Basis Library b. The Edinburgh SML Library c. The SML/NJ Library d. SML_TK e. Caml-light libraries f. The Qwertz Toolbox (for AI) 7. Theorem Provers and ML 8. Miscellaneous Questions a. How do I write the Y combinator in SML? b. Where can I find an X-windows interface to SML? c. How do I call a C function from SML/NJ? d. Where can I find an emacs mode for SML? -------------------------------------------------------------------------- 0. Where can I find the latest copy of this FAQ? This document can be retrieved via anonymous ftp from ftp://pop.cs.cmu.edu/usr/rowan/sml-archive/faq.txt or from rtfm.mit.edu. There is an HTTP version with active links at http://www.cis.ohio-state.edu/hypertext/faq/usenet/meta-lang-faq/faq.html -------------------------------------------------------------------------- 1. What is ML? ML (which stands for Meta-Language) is a family of advanced programming languages with [usually] functional control structures, strict semantics, a strict polymorphic type system, and parametrized modules. It includes Standard ML, Lazy ML, CAML, CAML Light, and various research languages. Implementations are available on many platforms, including PCs, mainframes, most models of workstation, multi-processors and supercomputers. ML has many thousands of users, is taught at many universities (and is the first programming language taught at some). -------------------------------------------------------------------------- 2. Where is ML discussed? COMP.LANG.ML ------------ comp.lang.ml is a moderated usenet newsgroup. The topics for discussion include but are not limited to: * general ML enquiries or discussion * general interpretation of the definition of Standard ML * applications and use of ML * announcements of general interest (e.g. compiler releases) * discussion of semantics including sematics of extensions based on ML * discussion about library structure and content * tool development * comparison/contrast with other languages * implementation issues, techniques and algorithms including extensions based on ML Requests should be sent to: comp-lang-ml@cs.cmu.edu Administrative mail should be sent to: comp-lang-ml-request@cs.cmu.edu Messages sent to the newsgroup are archived at CMU. The archives can be retrieved by anonymous ftp from internet sites. Messages are archived on a year-to-year basis. Previous years' messages are compressed using the Unix "compress" command. The current year's messages are not compressed. ftp pop.cs.cmu.edu username: anonymous password: <username>@<site> binary cd /usr/rowan/sml-archive get sml-archive.<year>.Z quit zcat sml-archive.<year>.Z (Pop's IP address is 128.2.205.205). Individual messages can also be accessed in the directories /usr/rowan/mh-sml-archive/<year>-sml. SML-LIST -------- The SML-LIST is a mailing list that exists for people who cannot (or do not want to) read the Usenet COMP.LANG.ML newsgroup. Messages are crossposted from COMP.LANG.ML to the SML-LIST and vice-versa. You should ask to join the SML-LIST _only if_ you cannot (or do not want to) read the Usenet COMP.LANG.ML newsgroup. To send a message to the SML-LIST distribution, address it to: sml-list@cs.cmu.edu (sites not connected to the Internet may need additional routing.) Administrative mail such as requests to add or remove names from the distribution list should be addressed to sml-list-request@cs.cmu.edu CAML-LIST --------- The Caml language, a dialect of ML, is discussed on the Caml mailing list. To send mail to the Caml mailing list, address it to: caml-list@inria.fr Administrative mail should be addressed to: caml-list-request@inria.fr ALT.LANG.ML ----------- No longer used. -------------------------------------------------------------------------- 3. What implementations of ML are available and where can I find them? Quick Summary: System full SML? contact Platforms ------ --------- ------------ ------------------------------ SML/NJ yes sml-nj@research.bell-labs.com Unix/Sparc,Mips,Vax,680x0, SML'97 ftp.research.att.com I386/486/Pentium,HPPA,RS/6000, MacOS/MacII ftp.cs.sunysb.edu Linux (including binaries) ftp-os2.nmsu.edu OS/2 (including binaries) ftp.informatik.uni-muenchen.de Nextstep sml2c yes dtarditi@cs.cmu.edu 32-bit Unix machines (C code) ftp.cs.cmu.edu Caml Light coreish caml-light@inria.fr Unix, Mac, PC 80386, ftp ftp.inria.fr (bytecode) Objective own caml-light@inria.fr Unix and Windows NT/95 Caml modules ftp ftp.inria.fr (bytecode) Alpha, Sparc, x86, Mips, HPPA, Power (native code) Bigloo coreish Manuel.Serrano@inria.fr. Unix (compiles caml-light ftp ftp.inria.fr to native code) Camlot coreish Regis.Cridlig@ens.fr Any 32-bit (compiles ftp ftp.inria.fr caml-light to C) Moscow ML core+ sestoft@dina.kvl.dk PC 80386, Mac, Unix SML'97 ftp ftp.dina.kvl.dk (bytecode) Kit yes ftp ftp.diku.dk (Requires another SML compiler ftp ftp.dcs.ed.ac.uk to build binaries) Edinburgh core ftp.dcs.ed.ac.uk 32-bit machines (bytecode) ftp.informatik.uni-muenchen.de PC 80386SX+, Amiga MicroML core Olof.Johansson@cs.umu.se PC 8086+ (bytecode) ftp ftp.cs.umu.se Poly/ML yes ahl@ahl.co.uk SPARC/SUNOS, SPARC/Solaris RS6000/AIX PoplogML yes isl@isl.co.uk Sun/Solaris, Sun/SunOS, SG/IRIX, PC/Linux, HP/HP-UX, Alpha/OSF, Alpha/VMS, VAX/VMS MLWorks yes web@harlequin.com SunOS, Solaris, Irix, SML'97 Windows NT/95. http://www.harlequin.com/mlworks Details: Standard ML of New Jersey ------------------------ Standard ML of New Jersey was developed jointly at AT&T Bell Laboratories and Princeton University. It is currently being worked on by researchers at AT&T Labs Research, Lucent Bell Labs, Princeton University, and Yale University. The SML/NJ distribution includes CM (a separate compilation manager), ML-Yacc, ML-Lex, ML-Burg, the SML/NJ Library, Concurrent ML, and eXene (a multithreaded X-windows toolkit). Version 93 of SML/NJ (released in February 1993) works on the Motorola 68k, SPARC, and MIPS (both big and little endian), I386/486/Pentium, HPPA(HP9000/700), and RS/6000 architectures under various versions of the Unix operating system (SunOS, Ultrix, Mach, Irix 4.0.x, Riscos, HPUX, AIX, AUX, etc.), and on the Macintosh OS (Mac II, System 7.x, min 12MB ram or any system of greater or equal power, which includes most Macs produced after about 1987). The SML/NJ team is currently working towards a release of version 110, which will be fuly SML'97 compliant. The latest ``working'' version can be found at: ftp://ftp.research.bell-labs.com/dist/smlnj/working/ Most working versions are quite stable, but check the README file for details. The working versions are currently supported on the following hardware/system combinations: Alpha OSF/1 Mips Irix 4.0.x, Irix 5.x, Irix 6.x x86 Linux, Solaris, FreeBSD, NetBSD, Windows95, WindowsNT Sparc SunOS, Solaris RS/6000 AIX (also PowerPC) HPPA HPUX 9, HPUX 10 In addition, there are ports of the PowerPC version to MacOS and BeOS in progress. There are a number of useful web links relating to SML/NJ. These can all be reached from the SML/NJ home page, which is at: http://cm.bell-labs.com/cm/cs/what/smlnj/index.html Another important link is the documentation for the SML'97 basis, which can be found at: http://cm.bell-labs.com/cm/cs/what/smlnj/basis/index.html http://www.dina.kvl.dk/~sestoft/sml/sml-std-basis.html SML2C ----- sml2c is a Standard ML to C compiler. It is based on an old version of SML/NJ from 1992 and shares its front-end and most of the runtime system. sml2c is a batch compiler and compiles only module-level declarations. It does not support SML/NJ style debugging and profiling. sml2c is easily portable and has been ported to IBM RT, Decstation 3100, Decstation 5000, Omron Luna 88k, sun-3, sun-4 and a 486-based machine (running Mach). The generated code is highly portable and makes very few assumptions about the target machine or the C compilers available on the target machine. The runtime system, which it shares with the SML/NJ has several machine and operating system dependencies. sml2c has eliminated some of these dependencies by using portable schemes for garbage collection and for freezing and restarting programs. sml2c is available by anonymous ftp from ftp.cs.cmu.edu (128.2.206.173). Log in as anonymous, send username@node as password. The distribution can be found in /afs/cs/project/mess/research/sml2c/ftp. The local ftp software will allow you to change directory only to /afs/cs/project/mess/research/sml2c/ftp. The README file in this directory describes the files in the distribution. The size of the uncompressed distribution is about 12 Meg. CAML LIGHT ---------- Caml Light is a portable, bytecode interpreter for CAML, a dialect of ML. Some features of Caml Light include separate compilation, streams and stream parsers, ability to link to C code, and a fairly rich library. The implementation has low memory requirements, compiles quickly and generates compact executables. The Caml Light system comprises a batch compiler, a toplevel-based interactive compiler, tools for building libraries and toplevel systems, a replay debugger, and a hypertext-based module browser. Caml Light runs on most modern Unix machines, including Sun Sparcstations (under SunOS 4.1 and Solaris 2), Decstations 3000 (Alpha) and 5000 (Mips), and PCs under Linux, but many more machines have been reported to work. It is also available for the Macintosh (as a "fat binary" that runs native on PowerMacs) and the PC under MS Windows and MSDOS. The current version is 0.73, released in January 1997. It is available by anonymous ftp from: host: ftp.inria.fr (192.93.2.54) directory: lang/caml-light Summary of the files: README.cl More detailed summary cl73unix.tar.gz Unix version (source code) cl73macbin.sea.bin Binaries for the Macintosh version cl73win.exe Binaries for MS Windows and MSDOS cl73refman.* Reference manual, in various formats cl73tutorial.* Tutorial, in various formats cl73macdoc.sea.bin On-line documentation for the Macintosh version cl73macsrc.sea.bin Source code for the Macintosh version More information on Caml Light is available on the Web at: http://pauillac.inria.fr/caml The implementors can be contacted at caml-light@inria.fr. General questions and comments of interest to the Caml community should be sent to caml-list@inria.fr, the Caml mailing list. (see question 2 above for details.) OBJECTIVE CAML -------------- Objective Caml (formerly known as Caml Special Light) is a complete reimplementation of Caml Light that adds a complete class-based object-oriented system and a powerful module system in the style of Standard ML. The object system is statically type-checked (no "message not understood" run-time errors) and performs ML-style type reconstruction (no type declarations for function parameters). This is arguably the first publically available object-oriented language featuring ML-style type reconstruction. The module system is based on the notion of manifest types / translucent sums; it supports Modula-style separate compilation, and fully transparent higher-order functors. Objective Caml comprises two compilers: a bytecode compiler in the style of Caml Light (but up to twice as fast), and a high-performance native code compiler for the following platforms: Alpha processors: DecStation 3000 under OSF1 (a.k.a. Digital Unix) Sparc processors: Sun Sparcstation under SunOS 4.1, Solaris 2, NetBSD Intel 486 and Pentium processors: PCs under Linux, NextStep, FreeBSD, Windows 95 and Windows NT Mips processors: DecStation 3100 and 5000 under Ultrix 4 HP PA-RISC processors: HP 9000/700 under NextStep (no HPUX yet) PowerPC processors: IBM RS6000 and PowerPC workstations under AIX 3.2 The native-code compiler delivers excellent performance (better than Standard ML of New Jersey 1.08 on our tests), while retaining the moderate memory requirements of the bytecode compiler. The source distribution (for Unix machines only) is available by anonymous FTP on ftp.inria.fr, directory lang/caml-light. More information on Objective Caml is available on the World Wide Web, at: http://pauillac.inria.fr/ocaml/ Bug reports and technical questions should be directed to caml-light@inria.fr. For general questions and comments, use the Caml mailing list caml-list@inria.fr (to subscribe: caml-list-request@inria.fr). BIGLOO ------ Bigloo is an optimizing Scheme-to-C and Caml-to-C compiler that produces native machine code from Caml sources. Compatibility with the bytecoded implementation of Caml Light is almost perfect. Performance of generated code is on a par with that of New Jersey ML. Bigloo is also one of the most efficient Scheme compilers available. Bigloo runs on the following Unix platforms: Decstations 3000 and 5000, Sparcstations, PCs under Linux, HP PA 730 and Sony News R3000. Bigloo is being developed by Manuel Serrano (Manuel.Serrano@inria.fr). Available from: ftp://ftp.inria.fr/lang/caml-light/bcl*.tar.gz. CAMLOT ----- Camlot is the stand alone Caml Light to C compiler. It then uses a standard C compiler to produce an executable machine code file. The compiler itself is mostly written in Caml Light and the runtime system is written in standard C, hence Camlot is easy to port to almost any 32-bit platform. The performance of the resulting code is quite good, often ten times faster than the bytecode original implementation of Caml Light. The distribution has been tested on the following platforms: Sun Sparcstation DecStation 3100 HP 9000/710 i386/486 Linux The distribution is avaiable at: ftp://ftp.inria.fr/lang/caml-light/camlot0.64a.tar.gz MOSCOW ML --------- Moscow ML is a Core Standard ML implementation, based on the Caml Light system. It implements the Core language of Standard ML and separate compilation via a limited version of the SML Modules language, with signatures and non-nested structures but no functors. Version 1.42 of Moscow ML * is somewhat faster * provides support for writing CGI scripts * automatically includes all required libraries when linking Moscow ML implements much of the SML Basis Library, follows the 1997 revision of Standard ML, and can produce compact stand-alone executables (a la Caml Light). Moscow ML works under DOS, many Unixes (including Linux, MkLinux, Solaris, IRIX, HP/UX), and MacOS (68k and PPC). It was written by Sergei Romanenko (roman@keldysh.ru) at the Keldysh Institute of Applied Mathematics, Moscow, Russia, and Peter Sestoft (sestoft@dina.kvl.dk) at the Royal Veterinary and Agricultural University, Denmark. Thanks to Xavier Leroy and Damien Doligez (Caml Light), Doug Currie (MacOS version, new bytecode) and Jonas Barklund (CGI support). * The Moscow ML homepage http://www.dina.kvl.dk/~sestoft/mosml.html * Moscow ML library units documentation http://www.dina.kvl.dk/~sestoft/mosmllib/index.html * The DOS executables (and documentation) are in ftp://ftp.dina.kvl.dk/pub/mosml/mos14bin.zip * The Linux executables (and documentation) are in ftp://ftp.dina.kvl.dk/pub/mosml/linux-mos14bin.tar.gz * The Macintosh/MacOS (68k and PPC) executables are in ftp://ftp.dina.kvl.dk/pub/mosml/mac-mos14bin.sea.hqx * The DOS source files are in ftp://ftp.dina.kvl.dk/pub/mosml/mos14src.zip * The Unix source files are in ftp://ftp.dina.kvl.dk/pub/mosml/mos14src.tar.gz * The MacOS modified source files (relative to Unix) are in ftp://ftp.dina.kvl.dk/pub/mosml/mac-mos14src.sea.hqx These files are mirrored at ftp://ftp.csd.uu.se/pub/mirror/mosml ftp://ftp.dcs.ed.ac.uk/pub/ml/versions/by_origin/Moscow The ML Kit ---------- Two versions of the ML Kit are available from DIKU: (a) The ML Kit (Version 1, 1993) (b) The ML Kit with Regions (1997) Both are described in more detail at the DIKU ML Kit web site: http://www.diku.dk/research-groups/topps/activities/mlkit.html ML Kit Version 1 ---------------- Version 1 of the ML Kit is a straight translation of the 1990 Definition of Standard ML into a collection of Standard ML modules. For example, every inference rule in the Definition is translated into a small piece of Standard ML code which implements it. The translation has been done with as little originality as possible - even variable conventions from the Definition are carried straight over to the Kit. If you are primarily interested in executing Standard ML programs efficiently, the ML Kit is not the system for you! (It uses a lot of space and is very slow.) The Kit is intended as a tool box for those people in the programming language community who may want a self-contained parser or type checker for full Standard ML but do not want to understand the clever bits of a high-performance compiler. We have tried to write simple code and module interfaces; we have not paid any attention to efficiency. The documentation is around 100 pages long and is provided with the Kit. It explains how to build, run, read and modify the Kit. It also describes how typing of flexible records and overloading are handled in the Kit. The ML Kit is written by Nick Rothwell, David N. Turner, Mads Tofte and Lars Birkedal at Edinburgh and Copenhagen Universities. The ML Kit with Regions (aka Version 2) --------------------------------------- Version 2 builds on Version 1, but is expanded into a real compiler. Inefficient data structures and algorithms in the system have been replaced by more efficient ones. The ML Kit with Regions is intended for the development of stand-alone applications which must be reliable, fast and space efficient. The main feature of the ML Kit with Regions is that it uses a stack of regions for memory management rather than traditional garbage collection techniques; this has several important consequences: Compile-Time Garbage Collection: All memory allocation directives (both allocation and de-allocation) are inferred by the compiler, which uses a number of novel program analyses concerning lifetimes and storage layout. There is no pointer-tracing garbage collection at runtime; Memory Safety: Safety of de-allocation of memory is ensured by the compiler; Static detection of space leaks; Region Resetting: It is possible to give explicit directives about resetting of regions in cases where the static analyses are too conservative; such directives are checked by the compiler; Region Profiling: The system includes a graphical region profiler, which helps gain detailed control over memory use; Soft Real-Time: Programmers who are interested in real-time programming can exploit the absence of garbage collection: there are no interruptions of unbounded duration at runtime; Interface to the C language: ML Kit applications can call C functions using standard C calling conventions; the region scheme can even take care of allocating and de-allocating regions used by C functions thus invoked. The overall goal with developing the ML Kit with Regions has been to combine the advantages of a high-level, type-safe language (Standard ML, 1997 Definition), with the advantages of low-level languages, namely detailed control over space and time. Indeed, it turns out that the regularity provided by the ML type system makes is possible to infer much more useful information about ML programs than one can reasonably hope for in languages with more liberal type systems. Naturally, the hope is that this technology will promote the use of Standard ML in situations where safety and detailed control of machine resources are important, as indeed is often the case. Since we are using Standard ML as our source language, one can use the ML Kit in conjunction with other Standard ML systems; for example, one can port programs that previously ran on a garbage collection based Standard ML system to run on the Kit; or one may use the Kit simply to gain insight into how a program intended for another system uses memory; or one can develop Standard ML programs directly in the Kit. We have tried all three with good results. A comprehensive technical report "Programming with Regions in the ML Kit" is available from the above web site. The ML Kit with Regions was developed by Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg, Tommy H{\o}jfeld Olesen (all at DIKU) and Peter Sestoft and Peter Berthelsen (both at KVL). Edinburgh ML 4.0 ---------------- Edinburgh ML 4.0 is an implementation of the core language (without the module system). It uses a bytecode interpreter, which is written in C and runs on any machine with 32 bit words, a continuous address space and a correct C compiler. Ports to various 16 bit machines are underway. The bytecode interpreter can be compiled with switches to avoid the buggy parts of the C compilers that we've used it with (as far as I know none of them worked correctly). Edinburgh ML 4.0 is available from the LFCS. See the WWW link: http://www.dcs.ed.ac.uk/lfcsinfo/index.html A port to PCs with 386SX processors or better is available by FTP from ftp.informatik.uni-muenchen.de, in the file pub/comp/programming/languages/sml/ibmpc/edml3864.exe. Contact Joern Erbguth (erbguth@juris-sb.de) for more information. Also, there are apparently 8086 and 80386-specific ports of Edinburgh ML 3.5 in the same location. The 386 port is in the file edml3863.exe. There are other Edinburgh (PC-)ports of ML including an OS/2 2.x, an OS/2 PM and a Dos version. A new version has just been made ready and is available at forwiss.uni-passau.de (132.231.1.10) in pub/ibmpc/os2/lang/sml/sml04.zip. It is about 360K long (short?). All 3 programs have in common (all in one .zip): - true 32 Bit applications - easy to install, easy to use - As far as I know they work stable (except the DOS version working as a Windows window [you can use it with Windows but it crashes on *exit*]) - they don't require expensive hardware (and they don't need a co-processor) To be more specific: OS/2 PM OS/2 DOS OS >= OS/2 2.0+ServPak >= OS/2 2.0 >= DOS 5.0 Edit PM, GUI, Standard command history integrated editor (cut&paste) HW >= 386/33, 8MB >= 386/33 4MB >= 386sx, 2MB lots of MB and fast graphics ad. recommended Help online online (+ML ref. in german) There's also an amiga port of Edinburgh ML available on all aminet ftp sites (amiga users should know which these are) in dev/lang, called "sml4.1.02.lha". The standard version needs a 68020 or better and an FPU but there is a 68000-only version as well. MicroML ------- MicroML is an interpreter for core SML that runs on IBM PCs, from the Department of Computing Science at the Umea University in Sweden. It implements the core language except for records. A 80286 processor or better is recommended, but it runs even on a 8086. MicroML is available by anonymous ftp from ftp.cs.umu.se /pub/uml022.zoo. For more information contact Olof Johansson (olof@cs.umu.se). Poly/ML ------- Poly/ML is a commercial product from Abstract Hardware Ltd. (email to ahl@ahl.co.uk, or browse http://www.ahl.co.uk). The Poly/ML system has been used to implement a number of high-value tools including ICL's ProofPower, ViewLogic's ViewSchedule and AHL's own LAMBDA toolset. Poly/ML 3.0 (Motif Edition) runs on SPARC systems under either SunOS (4.1) or Solaris (2.3 or later). It also runs on IBM RS/6000 systems under AIX. The Motif Edition of Poly/ML features native code generation, a make system, an X11/Xlib interface, and a OSF/Motif interface. Non-standard extensions include concurrent processes and an associated message-passing scheme. The price of the Motif edition of Poly/ML is 1500 pounds for an academic site licence or 3500 pounds per machine for commercial users. Multiple and site licences are available by negotiation. AHL are currently developing a Windows Edition of Poly/ML. This will run on standard PC hardware under the Windows 95. The release date and pricing policy for this product have not yet been finalised. Poplog ML --------- Standard ML is one of four languages included with the Poplog system, the others being Pop-11, Prolog and Common Lisp. It uses an incremental, native-code compiler which implements the full language described in the Definition; compilation is fast with low memory usage. There is an integrated editor and an X interface; these are both programmable only from Pop-11 but the shared compilation environment makes it easy to link Pop-11 procedures into ML programs. This provides a general route for calling out to external libraries. Poplog is available for various Unix systems -- Sun SPARC with Solaris or SunOS, Silicon Graphics, DEC Alpha, HP RISC and Linux -- but also for VMS, both on Alpha and VAX. It costs money, but there are substantial discounts for academic users. Sales are handled by Integral Solutions Ltd. and enquiries should be directed to them at isl@isl.co.uk. You can get a free demonstration copy of Poplog for Linux/x86 from ftp://ftp.cogs.susx.ac.uk/pub/poplog/poplog15.0 This is entirely compatible with the full-price version, but is unsupported and has certain restrictions: in particular, it has a limited heap size and cannot make saved images. But it is a working system and may be of special interest to students who want SML on their PCs at home. Adrian John Howard (adrianh@cogs.susx.ac.uk) has a WWW page for Poplog: http://www.cogs.susx.ac.uk/users/adrianh/poplog.html Harlequin MLWorks ----------------- Harlequin MLWorks is a commercial product and is a full implementation of SML encapsulated inside a modern programming environment. MLWorks supports both SML90 (TDoSML), and SML97 (revised definition). In addition to Harlequin's compiler technology, MLWorks offers: - Graphical browsing and inspection - Source level debugging and tracing - Graphical profiling (call count, time slice and heap) and profiling of standalone applications without source modification - Integration with source editors - Generational garbage collection - A sophisticated compilation manager - A C Foreign Function Interface Libraries are provided supporting graphics, threads and the Standard ML Basis Library. MLWorks is available on SunOS, Solaris, Irix, Windows NT and Windows 95. An evaluation version may be freely downloaded from Harlequin's web site: http://www.harlequin.com/mlworks -------------------------------------------------------------------------- 4. Unsupported SML/NJ Ports This section describes various ports of SML/NJ (see section 3) that are not directly supported by the NJ folks. Linux: ------ (Thanks to Ralf Reetz, Peter Su, and Mark Leone) This is a port of Standard ML of New Jersey (SML/NJ) to Linux. It is based on the work of Mark Leone (mleone@cs.cmu.edu) who did the port for i386/i486 machines. The current binary was compiled using Linux 0.99.7a. Shared lib 4.3.3. This port was done by Sanford Barr (sbarr@cs.sunysb.edu) based on the original port of 0.91 by Hermano Moura (moura@dcs.glasgow.ac.uk) and Andre Santos (andre@dcs.glasgow.ac.uk). Various ftp sites seem to carry SML/NJ version 0.93 for Linux: tsx-11.mit.edu:/pub/linux/sources/usr.bin/ njsml.93.src.tar.z njsml.93.linux.README njsml.93.linux.README.NEW njsml.93.linux.diffs.z ftp.cs.sunysb.edu:/pub/linux/ njsml.93.bin.z njsml.93.mo.i386.z njsml.93.linux.README njsml.93.linux.diffs.z njsml.93.src.tar.z ftp.dcs.glasgow.ac.uk:/pub/linux/ njsml.93.linux.diffs.z njsml.93.src.tar.z smlnj-0.93-linux.README 16M of ram is suggested if you wish to do anything serious with the system. Also, a 386-40 or better would be helpful. KNOWN BUGS AND DEFICIENCIES: 1 Some minimal precision problems exist when a 387 emulator is used. 2 ML functions System.Directory.listDir and System.Directory.getWD not working at the moment. 3 There have been reported problems with the Div exceptions (real & int). The problems have been corrected. See: ftp.id.dth.dk (Internet 130.225.76.51) file pub/sestoft/sml93-linux99pl12/sml.gz That version also allows profiling; see the README file. OS/2: ----- Standard ML of New Jersey (version 0.93) for OS/2 has been implemented using Mark Leone's i386 code generator and the Unix emulator EMX (copyright of Eberhard Mattes). It is an (almost) complete implementation of SML/NJ 0.93. Only a few System.* functions have been left unimplemented. Features of this 2nd release for OS/2: * Signal handling * Interval timers (real-time, supports CML 0.9.8) * 'Garbage flushing', yields better performance on low-memory machines * Reduced executable size (well, now it equals the other ports ;-) * Exporting supported (also in the binary-only package) * Improved MakeML & BindCore utilities * Generally more robust * Using EMX version 0.8h (the latest release at this moment) Available from ftp.research.att.com (in /dist/ml/) and, in Europe, from ftp.id.dth.dk (in /pub/bertelsen/) as: 93.os2b.exe.zip Binary-only, SML/NJ interactive compiler (executable) 93.os2b.src.zip Sources & documentation 93.os2b.txt Introduction See 93.os2b.txt for system requirements and details on .zip files. Peter Bertelsen (c917023@id.dth.dk) Department of Computer Science, Technical University of Denmark FreeBSD: -------- A patch for the standard distribution is available at: ftp://pop.cs.cmu.edu/usr/rowan/sml-archive/freebsd/ NEXTSTEP: --------- The CSDMteam at the University of Munich proudly presents the port of Standard ML of NJ, version 0.93, to NEXTSTEP for Intel processors. The modified source can be found at ftp.informatik.uni-muenchen.de: /pub/comp/programming/languages/sml/NJ-0.93/93.src.nsfip.tar.Z (please look at the installation instructions in the file README.NeXT.I386). A precompiled binary of the interpreter (gzip'ed) is located at ftp.informatik.uni-muenchen.de:/pub/comp/platforms/next/Developer/languages/ml /sml.0.93.I.b.gz. SVR4: ----- An mplementation for SVR4.0.4 is available from Anthony Shipman (als@tusc.com.au) that fixes the problems with listDir and getWD and includes a full malloc implementation for runtime/malloc.c. Contact Anthony for more info. -------------------------------------------------------------------------- 5. Where can I find documentation on ML? THE DEFINITION -------------- Robin Milner, Mads Tofte, Robert Harper and Dave MacQueen The Definition of Standard ML (Revised) MIT Press, 1997, xiii + 114 pp. ISBN 0-262-63181-4 (paper) Robin Milner, Mads Tofte and Robert Harper The Definition of Standard ML MIT, 1990. ISBN: 0-262-63132-6 Robin Milner and Mads Tofte Commentary on Standard ML MIT, 1991 ISBN: 0-262-63137-7 TEXTS (date order) ----- Ake Wikstrom Functional Programming Using Standard ML Prentice Hall 1987 ISBN: 0-13-331661-0 Chris Reade Elements of Functional Programming Addison-Wesley 1989 ISBN: 0-201-12915-9 Lawrence C Paulson ML for the Working Programmer (2nd Edition) Cambridge University Press 1996 ISBN: 0-521-56543-X (paperback), 0-521-57050-6 (hardback) (Covers SML'97. see: http://www.cl.cam.ac.uk/users/lcp/MLbook/) Stefan Sokolowski Applicative High Order Programming: The Standard ML perspective Chapman & Hall 1991 ISBN: 0-412-39240-2 0-442-30838-8 (USA) Ryan Stansifer ML Primer Prentice Hall, 1992 ISBN 0-13-561721-9 Colin Myers, Chris Clack, and Ellen Poon Programming with Standard ML Prentice Hall, 1993 ISBN 0-13-722075-8 (301pp) Jeffrey D. Ullman Elements of ML Programming Prentice-Hall, 1993 (Oct. 15) ISBN: 0-13-184854-2 (See Comp.Lang.ML archives, message from Ullman dated 22 Sep 1993 for chapter headings.) Rachel Harrison Abstract Data Types in Standard ML John Wiley & Sons, April 1993 ISBN: 0-471-938440 Richard Bosworth, A Practical Course in Functional Programming Using Standard ML, McGraw-Hill 1995, ISBN: 0-07-707625-7. Elementary Standard ML Greg Michaelson UCL Press 1995 ISBN: 1-85728-398-8 PB (see ftp://ftp.cee.hw.ac.uk/pub/funcprog/gjm.book95.ps.Z for contents and prologue). INFORMATION AVAILABLE BY INTERNET --------------------------------- The Fox project at CMU has a WWW page for information about Standard ML, which also includes the first two reports below: http://foxnet.cs.cmu.edu/sml.html The following report covers all of Standard ML, and is available at: ftp://ftp.cs.cmu.edu/afs/cs/project/fox/mosaic/intro-notes.ps Robert Harper Introduction to Standard ML LFCS Report Series ECS-LFCS-86-14 Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh Nov. 1986 (revised Jan. 1989 by Nick Rothwell and Kevin Mitchell) The following report includes an introduction to Standard ML and 3 lectures on the modules system. Available from: http://foxnet.cs.cmu.edu/sml.html Mads Tofte Four Lectures on Standard ML LFCS Report Series ECS-LFCS-89-73 Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh March 1989 The following report introduces Extended ML, a language for writing (non-executable) specifications of Standard ML programs and for formally developing Standard ML programs from such specifications. The report is available at: http://www.dcs.ed.ac.uk/%7Edts/eml/bcs.ps Don Sannella Formal program development in Extended ML for the working programmer. LFCS Report Series ECS-LFCS-89-102 Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh December 1989 Le projet Cristal at INRIA Rocquencourt has set up a WWW server for information regarding its activities, especially the Caml and Caml Light compilers. The server also offers on-line access to documentation, publications and to a database of BibTex references in CS. Welcome to: http://pauillac.inria.fr/ Please report problems and suggestions to Xavier.Leroy@inria.fr. Richard Botting has taken Larry Paulson's SML Syntax and translated it into a form that can be read by mosaic, netscape, lynx and other WWW browsers. The URL is: http://www.csci.csusb.edu/dick/samples/ml.syntax.html Andrew Cumming has made availible "A Gentle Introduction to ML". It is aimed at students who are reasonably computer literate but who are new to functional programming. It consists largely of questions and diversions broken up into roughly one-hour tutorials, most of the questions have hints which the student can follow up if required. The material is intended to be used alongside ML - sections of code may be copied from the browser window into an ML session. The URL is http://www.dcs.napier.ac.uk/course-notes/sml/manual.html There are some WWW pages based on an info-tree at MIT with a variety of useful information on ML. The URL is: http://www.ai.mit.edu/!info/sml/!!first There is an interesting collection of news articles at: http://www.cs.jcu.edu.au/ftp/web/FP/ml.html -------------------------------------------------------------------------- 6. Where can I find library code? a. The Standard ML ('97) Basis Library In order to enhance the usefulness of SML as a general-purpose programming language, a group of SML implementers, including representatives of Harlequin's ML Works, Moscow ML and SML/NJ, have put together a proposal for an SML Basis Library, containing a collection of modules to serve as a basic toolkit for the SML programmer. The current draft is available on the web at http://cm.bell-labs.com/cm/cs/what/smlnj/basis/index.html http://www.dina.kvl.dk/~sestoft/sml/sml-std-basis.html b. The Edinburgh SML Library The Edinburgh SML Library provides a consistent set of functions on the built-in types of the language and on vectors and arrays, and a few extras. It includes a "make" system and a consistent set of parsing and unparsing functions. The library consists of a set of signatures with sample portable implementations, full documentation, and implementations for Poly/ML, Poplog ML and SML/NJ that use some of the non-standard primitives available in those systems. It is distributed with Poly/ML, Poplog ML and Standard ML of New Jersey. It is also available from the LFCS. The library documentation is available as a technical report from the LFCS (reports@dcs.ed.ac.uk) and costs 5 pounds or 10 US dollars. The LaTeX source of the report is included with the library. Dave Berry The Edinburgh SML Library LFCS Report Series ECS-LFCS-91-148 Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh April 1991 c. The SML/NJ Library The SML/NJ Library is distributed with the SML of New Jersey compiler. It provides a variety of utilities such as 2-dimensional arrays, sorting, sets, dictionaries, hash tables, formatted output, Unix path name manipulation, etc. The library compiles under SML/NJ but should be mostly portable to other implementations. d. SML_TK sml_tk is a Standard ML package providing a portable, typed and abstract interface to the user interface description and command language Tcl/Tk. It combines the advantages of the Tk toolkit with the advantages of Standard ML (bypassing the shortcomings of Tcl), allowing the implementation of graphical user interfaces in a structured and reusable way, supported by the powerful module system of Standard ML. For more information, and to obtain sml_tk, please point your web browser to the sml_tk homepage at http://www.informatik.uni-bremen.de/~cxl/sml_tk or contact us at smltk@informatik.uni-bremen.de. e. Caml-light libraries (Included in the Caml Light distribution unless otherwise noted) (Most of these libraries are also available for Objective Caml) CAML-TK TK is a GUI library for the TCL language. Normally, TK is controlled from TCL. The Caml-TK interface provides a Caml Light library to control TK from Caml Light programs. Thus, TK can be used to program graphical user-interfaces in Caml Light without knowledge of the TCL language. LIBGRAPH The "libgraph" library implements basic graphics primitives (line and text drawing, bitmaps, basic event processing) for the Caml Light system. It is portable across all platforms that run Caml Light: X-Windows, Macintosh, MSDOS. CAMLWIN Camlwin is a GUI library for Caml Light that provide all the classical graphic objects: buttons, string and text editors, list... and a high level object like windowed file selector. It is based on an extension of the "libgraph" library and therefore highly portable. Its main interest is its ability to compile the same code under many systems. At present time, it works under DOS, Windows, and X11 with unix. Camlwin is distributed at: ftp.inria.fr:lang/caml-light/Usercontribs/camlwin The reference manual is also available on the WWW at: http://liasc.enst-bretagne.fr/~saunier LIBNUM The "libnum" library implements exact-precision rational arithmetic for Caml Light. It is built upon a state-of-the-art arbitrary-precision integer arithmetic package, and therefore achieves very good performance (it's much faster than Maple, for instance). LIBUNIX The "libunix" library makes many Unix system calls and system-related library functions available to Caml Light programs. It provides Caml programs with full access to Unix capabilities, especially network sockets. LIBSTR The "libstr" library for Caml Light provides high-level string processing functions, including regular expression matching and substitution. It is intended to support the kind of text processing that is usually performed with "sed" or "perl". f. The Qwertz Toolbox The qwertz toolbox, a library of Standard ML modules with an emphasis on symbolic Artificial Intelligence programming, may now be obtained by anonymous ftp at: ftp.gmd.de:gmd/ai-research/Software/qwertz.tar.gz The qwertz.tar.gz file is a tar archive compressed using the the GNU gzip program. Use the gunzip program to decompress it. The README file explains how the install the library. The toolbox includes: symbols and symbolic expressions, tables including association lists, sets, queues and priority queues, streams, heuristic search including A* and iterative deepening, and an ATMS reason maintenance system. -------------------------------------------------------------------------- 7. Theorem Provers and ML (Collected by Paul Black, pblack@cs.berekeley.edu. Thanks Paul!) - LCF (Edinburgh LCF and Cambridge LCF) * originally written in the Edinburgh dialect of ML from which SML developed. "Logic and Computation: Interactive Proof with Cambridge LCF" also by Lawrence C. Paulson. (Describes a Standard ML [core language only] version of LCF.) The port was done by M. Hedlund, then at Rutherford Appleton Labs, UK. It is available by anon. ftp from ftp://ftp.cl.cam.ac.uk/ml/lcf.tar.gz. - Lego (LFCS, Edinburgh Univ., SML) * originally developed in CAML * latest version (5) now runs under SML/NJ * only higher-order resolution * available via anon. ftp from ftp.dcs.ed.ac.uk:/pub/lego - HOL90 Authors = Konrad Slind, Elsa Gunter kxs@cl.cam.ac.uk, elsa@research.att.com http://www.cl.cam.ac.uk/Research/HVG/HOL/ hol90 is a free implementation in SML/NJ of Mike Gordon's HOL logic (a polymorphic version of Church's Simple Type Theory). The system provides a lot of automated support including: - a powerful rewriting package; - pre-installed theories for booleans, products, sums, natural numbers, lists, and trees; - definition facilities for recursive types and recursive functions over those types (mutual recursion is also handled); - extensive libraries for strings, sets, group theory, integers, the real numbers, wellordered sets, automatic solution of goals involving linear arithmetic, tautology checking, inductively defined predicates, Hoare logic, Chandy and Misra's UNITY theory, infinite state automata, and many others. The HOL community has a lively mailing list accessible at info-hol-request@leopard.cs.byu.edu and a yearly user's meeting that alternates between Europe and North America. hol90 is available by anonymous ftp from machine = ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/slind/hol90/ or machine = ftp.research.att.com/dist/ml/hol90/ Tim Leonard mentions that a description of the variant of ML used in HOL88 is online at the following url: http://lal.cs.byu.edu/lal/holdoc/Description/ML/ML.html - NuPrl (from Bob Constable`s group at Cornell) - Isabelle (Lawrence C. Paulson, Cambridge Univ. ) * has rewriting, but not many decision procedures. It does have things like model elimination-based decision procedures. * a generic automatic theorem prover i.e. you can program it to the logic system/proof system you want. Already has the following subsystems already implemented: i) FOL - first order logic ii) HOL - higher order logic iii) LCF - Logic of computable functions iv) LK - Gentzen system LK v) Modal - Modal logic systems T, S4, S43 vi) ZF - Zermelo-Fraenkel set theory * ftp from ftp://ftp.cl.cam.ac.uk/ml/Isabelle94.tar.gz * There's a WWW page: http://www.cl.cam.ac.uk/Research/HVG/isabelle.html * There's also a mailing list: isabelle-users@cl.cam.ac.uk - MERILL (Brian Matthews, U. of Glasgow & Rutherford Appleton Laboratory) * written in standard ML * a general purpose order-sorted equational reasoning system * Allows the user to declare their own object language, allows AC-rewriting and AC-unification of terms and equations, has several completion algorithms, is built on a hierarchy of types known as Order-Sorting, and allows the user to try different termination methods. * available via anonymous ftp from the University of Glasgow, ftp address: ftp.dcs.glasgow.ac.uk (130.209.240.50) * Brian Matthews, brian@dcs.glasgow.ac.uk or bmm@inf.rl.ac.uk - FAUST (Karlsruhe) * a HOL add-on written in ML. * ftp from goethe.ira.uka.de (129.13.18.22) - Alf * written in SML * An implementation of Martin-Lofs type theory with dependent types * Proof editor * available by anonymous ftp from cs.chalmers.se * only higher-order resolution - Coq * written in Objective CAML (previous versions were written in CAML and Caml-Light) * implements the Calculus of Inductive Constructions a logical framework suitable for abstract mathematical formalisation and functional program manipulation. * available via anon. ftp from ftp.ens-lyon.fr:/pub/LIP/COQ/V6.1 ftp.inria.fr:INRIA/Projects/coq/coq/V6.1 * possible contact: coq@pauillac.inria.fr more information : http://pauillac.inria.fr/coq/systeme_coq-eng.html * Coq has an interface based on Centaur developed by the CROAP project at INRIA Sophia-Antipolis : http://www.inria.fr/croap/ctcoq/ctcoq-eng.html - ICLHOL/ProofPower (ICL Secure Systems) * a commercial system using a reimplementation of HOL in SML * contact ProofPower-server@win.icl.co.uk - Lamdba/DIALOG (Abstract Hardware Ltd) * a commercial tool written in Poly/ML * contact ahl@ahl.co.uk - Elf (Frank Pfenning, Carnegie Mellon Univ.) * Elf is a higher-order logic programming language based on the LF Logical Framework. * Elf is not a theorem prover per-se, but is useful for specifying and proving properties of programming languages, logics, and their implementations. A number of examples are provided with the distribution. * The Elf implementation is written in SML/NJ and should be easily portable to other SML implementations. * Elf can be ftp'd from ftp.cs.cmu.edu (128.2.206.173) in the directory user/fp/ * A home page for Elf can be found at http://www.cs.cmu.edu/~fp/elf.html * There is an Elf mailing list. Contact elf-request@cs.cmu.edu to join. * For further information, contact Frank Pfenning (fp@cs.cmu.edu). - Definitional Reasoning (Univerity of Tasmania) * developed with SML/NJ * a study of Boolean Affine Combinations (a highly formal case construct) * includes a rich set of term rewriting combinators * ftp://hilbert.maths.utas.edu.au/pub/DR.tar.gz * mail to piggy@acm.org for more information. References "ML for the Working Programmer" by Lawrence C. Paulson contains a small first-order theorem prover. Paulson also has a good chapter on writing theorem provers in ML in "Handbook of logic in computer science", Edited by: S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum. Oxford : Clarendon Press, 1992-. CALL#: QA76 .H2785 1992 Others Edinburgh's Concurrency Workbench and Sussex's Process Algebra Mauipulator are also ML systems of note, though neither are interactive theorem provers. -------------------------------------------------------------------------- 8. Miscellaneous Where can I find out about SML'97? Look at: http://cm.bell-labs.com/cm/cs/what/smlnj/sml97.html How do I write the Y combinator in SML without using a recursive definition (i.e. "fun" or "let rec")? datatype 'a t = T of 'a t -> 'a val y = fn f => (fn (T x) => (f (fn a => x (T x) a))) (T (fn (T x) => (f (fn a => x (T x) a)))) Where can I find an X-Windows interface to SML? Poly/ML, Poplog/ML, MLWorks and SML/NJ all come with X-Windows interfaces. See the appropriate entries under section 3. In addition, Poly/ML interfaces to the industry standard OSF/Motif toolkit. How do I call a C function from SML/NJ? See the file runtime/cfuns.c for example C functions that are in the runtime and callable from ML. You have to enter the function into a table at the end of the file along with a string. You use the function System.Unsafe.CInterface to look up the function, using the string as the key. Note that you'll need to convert ML values to C representations and back. You'll have to rebuild the compiler using makeml. Where can I find an emacs mode for SML? Version 3.2 of sml-mode is at ftp://set.gmd.de/pub/sks/mjm/sml-mode/ and Version 3.3, which is stable but still at beta, is at http://www.scs.leeds.ac.uk/mjm/sml-mode/ Nowadays sml-mode works well with Emacs 19 and XEmacs 19, as well as a number of different SML compilers.