informis
/
textfiles
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
textfiles/internet/FAQ/metalng.faq

962 lines
39 KiB
Plaintext
Raw Blame History

Newsgroups: comp.lang.ml,comp.answers,news.answers
Path: bloom-beacon.mit.edu!hookup!europa.eng.gtefsd.com!fs7.ece.cmu.edu!honeydew.srv.cs.cmu.edu!jgmorris
From: jgmorris@cs.cmu.edu (Greg Morrisett)
Subject: Comp.Lang.ML FAQ [Monthly Posting]
Message-ID: <CoM6vH.MDw.3@cs.cmu.edu>
Followup-To: poster
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: jgmorris@VACHE.VENARI.CS.CMU.EDU
Sender: jgmorris@cs.cmu.edu
Nntp-Posting-Host: vache.venari.cs.cmu.edu
Reply-To: comp-lang-ml-request@cs.cmu.edu
Organization: School of Computer Science, Carnegie Mellon
Date: Thu, 21 Apr 1994 14:57:16 GMT
Approved: comp-lang-ml@cs.cmu.edu
Expires: Sat, 21 May 1994 00:00:00 GMT
Lines: 940
Xref: bloom-beacon.mit.edu comp.lang.ml:444 comp.answers:5006 news.answers:18361
Archive-name: meta-lang-faq
Last-modified: 1994/03/18
COMP.LANG.ML Frequently Asked Questions and Answers
(compiled by Dave Berry and Greg Morrisett)
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. Poly/ML
c. Standard ML of New Jersey
d. Poplog ML
e. ANU ML
f. MicroML
g. sml2c
h. Caml Light
i. ML Kit Compiler
4. Unsupported SML/NJ Ports
a. MS-DOS/Windows
b. Linux
c. OS/2
5. Where can I find documentation on ML?
a. The Definition
b. Textbooks
6. Where can I find ML library code?
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. How do I fix the emacs mode to work with
emacs 19?
--------------------------------------------------------------------------
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/jgmorris/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/jgmorris/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@margaux.inria.fr
Administrative mail should be addressed to:
caml-list-request@margaux.inria.fr
ALT.LANG.ML
-----------
Another venue for ML-related discussion is the Netnews group
alt.lang.ml, though this has seen relatively little traffic.
--------------------------------------------------------------------------
3. What implementations of ML are available and where can I find them?
(Note, this information may be out of date.)
Quick Summary:
System full SML? contact Platforms
------ --------- ------------ ------------------------------
Poly/ML yes ahl@ahl.co.uk SPARC/SUNOS, SPARC/Solaris
SML/NJ yes dbm@resarch.att.com Unix/Sparc,Mips,Vax,680x0,
ftp research.att.com I386/486,HPPA,RS/6000,
MacOS/MacII
ftp.rz.uni-karlsruhe.de Linux (including binaries)
ftp-os2.nmsu.edu OS/2 (including binearies)
PoplogML yes isl@integ.uucp, VMS/Vax, Unix/Vax,Suns,Sparcs,
alim@uk.ac.sussex.cogs, Solbourne, Sequent Symmetry,
pop@cs.umass.edu HP M680?0, Apollo, AUX/MacII
Edinburgh core ftp ftp.dcs.ed.ac.uk 32-bit machines (bytecode)
ftp ftp.informatik.uni-muenchen.de PC 80386SX+
ANU ML core mcn@anucsd.anu.edu.au Sun-3, Ultrix/Vax, Pyramid,
AUX/MacII
MicroML core olof or mahler @cs.umu.se PC 80286+ (bytecode)
ftp ftp.cs.umu.se
sml2c yes dtarditi@cs.cmu.edu 32-bit Unix machines (C code)
ftp dravido.soar.cs.cmu.edu
Caml Light coreish caml-light@margaux.inria.fr 32-bit Unix, Mac, PC 8086,
ftp ftp.inria.fr PC 80386 (bytecode)
Kit yes ftp ftp.diku.dk (Requires another SML compiler
ftp ftp.dcs.ed.ac.uk to build binaries)
Details:
Poly/ML:
Poly/ML produces native code for SPARC systems under either
SUNOS (4.1) or Solaris (2.3). A PC version is currently under
development. Poly/ML uses a persistent store and supports arbitrary
precision integer arithmetic. The Motif Edition of Poly/ML comes
with a make system, an X11/Xlib interface, and a OSF/Motif
interface. Non-standard extensions include concurrent processes and
an associated message-passing scheme.
Poly/ML is a commercial product from Abstract Hardware Ltd.
(ahl@ahl.co.uk). The price of the Motif edition is 1250 pounds for an
academic site licence or 3500 pounds per machine for commercial users.
Multiple and site licences are available by negotiation.
Standard ML of New Jersey:
Standard ML of New Jersey was developed jointly at AT&T Bell
Laboratories and Princeton University. It is an open system (source
code is freely available) implemented in Standard ML. Version 0.93 of
SML/NJ generates native code for 68020, SPARC, and MIPS (big and
little endian), I386/486, HPPA(HP9000/700), and RS/6000 architectures
under various versions of the Unix operating system (SunOS, Ultrix,
Mach, Irix, Riscos, HPUX, AIX, AUX, etc.), and on the MacIntosh OS
(Mac II, System 7.x, min 12MB ram). Version 0.75 runs on the Vax
under Ultrix, BSD, and Mach.
SML/NJ comes with a source-level debugger, profiler, gnu emacs
interface, ML implementations of LEX, YACC, and Twig, separate compilation
facilities, Concurrent ML, the eXene X Window library, and the SML/NJ
library. It runs interactively and can produce stand-alone executable
applications.
Non-standard extensions include typed first-class continuations,
Unix signal handling, and higher-order functors.
SML/NJ is copyrighted by AT&T but the system, including source
code, is freely distributable. It is available by anonymous ftp from
research.att.com (192.20.225.2) and princeton.edu (128.112.128.1).
Login as "anonymous" with your user name as password. Put ftp in
binary mode and copy the (compressed tar) files you need from the
directory dist/ml (pub/ml on princeton.edu). You only need the 93.mo.*.tar.Z
files for your machine in addition to the 93.src.tar.Z. (You might also
want the 93.release-notes.[ps|txt], 93.tools.tar.Z, 93.doc.tar.Z, and
smlnj-lib-0.2.tar.Z files.) Alternatively mail dbm@research.att.com.
In the UK, SML/NJ is available from the LFCS.
There are unsupported ports of SML/NJ to other platforms, including
Linux, FreeBSD, OS/2, and Microsoft Windows 3.1. See the "Unsupported SML/NJ
Ports" section for details.
Poplog ML:
Standard ML is supported as part of the Poplog system, which also
provides incremental compilers for Pop-11, Common Lisp and Prolog in a
common environment with shared data-structures, so that mixed language
programming is possible. The integrated editor and HELP mechanism
support online teaching aids. Poplog comes with an X Windows interface.
Poplog is available for VAX+VMS, VAX+Ultrix, VAX+Bsd 4.2/3,
Sun-2,3,4, Sun386i, SPARCstation, Solbourne, Sequent Symmetry (with Dynix),
HP M680?0+Unix workstations and Apollo+Unix. Versions for MAC-II with A/UX,
DECstation 3100 and MIPS will be available shortly.
UK educational users should contact the School of Cognitive and
Computing Sciences, University of Sussex (alim@uk.ac.sussex.cogs). People in
the USA or Canada should contact Computable Functions Inc. (pop@cs.umass.edu).
All others should contact Integral Solutions Ltd. (isl@integ.uucp). UK
academic prices start at 600 pounds. Non-UK academic prices start at 1125
pounds. Commercial prices start around 2,000 pounds for an ML-only version
or 7,500 pounds for the full Poplog system.
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.
A port to PCs with 386SX processors or better is available by FTP
from ftp.informatik.uni-muenchen.de, in the file pub/sml/ibmpc/edml3864.exe.
Contact Joern Erbguth (jnerbgut@cip.informatik.uni-erlangen.de) for more
information.
Some information from Felix von Normann follows:
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. recommened
Help online online
(+ML ref. in german)
ANU ML
ANU ML is descended from Cardelli's ML Pose 3. It implements the
core language of the standard and an old version of modules. It incrementally
compiles to native code on Sun-3, Vax/Ultrix, Pyramid and MacII/AUX. (It
is intended to standardize modules and do the port to Sun-4 in the near
future.)
ANU ML has a program development system with strong support for
debugging (tracing, automatic retesting etc.) and has been extended with
a built-in type complex.
ANU ML is still considered to be in beta release since exceptions
have been standardized quite recently. It is available from Malcolm Newey,
CS Dept., Australian National University (mcn@anucsd.anu.edu.au) by
arrangement; soon to be available by ftp.
MicroML
MicroML is an interpreter for a subset of SML that runs on IBM PCs,
from the Institute of Information Processing at the University of Umea in
Sweden. It implements the core language except for records. A 80286
processor or better is recommended.
MicroML is available as an alpha-release by anonymous ftp from
ftp.cs.umu.se /pub/umlexe01.uue. There are several known bugs in the current
version. For more information contact Olof Johansson (olof@cs.umu.se) or
Roger Mahler (mahler@cs.umu.se).
sml2c
sml2c is a Standard ML to C compiler. It is based on SML/NJ 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 dravido.soar.cs.cmu.edu
(128.2.220.26). Log in as anonymous, send username@node as password. The
compressed tar file sml2c.tar.Z can be found in /usr/nemo/sml2c. The local
ftp software will allow you to change directory only to /usr/nemo/sml2c.
The size of the tar file is about 3 Meg. The size of the uncompressed
distribution is about 12 Meg.
Caml Light
Caml Light is a portable, bytecode interpreter for a subset of CAML,
a dialect of ML. Some features of Caml Light include separate compilation,
streams and stream parsers, ability to link to C code, and tools for
building libraries and toplevel systems. The PC versions provide
line editing and the 80386 port is VCPI-compliant.
The Unix version should work on any modern workstation. We have tested
it on Sun 3 and 4, DecStations, HP 9000/700 and 9000/350, IBM RS/6000,
SGI Indigo, Sony News, Next cubes, and some more exotic machines.
The Macintosh version is now a standalone Macintosh application, and
no longer requires the Macintosh Programmer's Workshop. (Well, at
least for the toplevel environment; the batch compilers still run
under MPW.) The application provides some graphics primitives.
The PC version still comes in two flavors, one that run on any PC, but
is severely limited by the 640K barrier, and one that run on 80386 or
80486 PC's in 32 bit protected mode to circumvent these limitations.
Both versions now provide the same graphics primitives as the
Macintosh version. Ports to OS/2 and to the Amiga are in progress.
The version 0.6 of the Caml Light system has been released, and is
available by anonymous FTP from:
host: ftp.inria.fr (192.93.2.54)
directory: lang/caml-light
Summary of the files:
README More detailed summary
cl6unix.tar.Z Unix version
cl6macbin.sea.hqx Binaries for the Macintosh version
cl6macsrc.sea.hqx Source code for the Macintosh version
cl6pc386bin.zip Binaries for the 80386 PC version
cl6pc386src.zip Source code for the 80386 PC version
cl6pc86bin.zip Binaries for the 8086 PC version
cl6pc86src.zip Source code for the 8086 PC version
cl6refman.* Reference manual, in various formats
cl6tutorial.* Tutorial, in various formats
This release is mostly a bug-fix release and should be compatible with
Caml Light 0.5. The main changes are:
* Better handling of type abbreviations.
* Debugging mode (option -g to camlc and camllight) to get access
to the internals of module implementations.
* New library modules:
genlex generic lexical analyser
set applicative sets over ordered types
map applicative maps over ordered types
baltree balanced binary trees over ordered types
* "compile" command at toplevel (especially useful in the Macintosh version).
* New contributed libraries and tools:
camlmode Emacs editing mode for Caml Light
mletags Indexing of Caml Light source files for use with Emacs "tags"
search_isos Search libraries by types (modulo isomorphisms)
libgraph X implementation of the portable graphics library
libnum Arbitrary-precision arithmetic
libstr String operations, regular expressions
* The 80386 PC version is now DPMI-compliant, hence it can run under Windows
(in text mode inside a DOS windows and with no graphics, though).
* More examples, including those from the book "Le langage Caml".
General questions and comments of interest to the Caml community
should be sent to caml-list@margaux.inria.fr, the Caml mailing list.
(see question 3 above for details.)
ML Kit Compiler
The ML Kit is a straight translation of the 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 is available via anonymous ftp. Here is a sample dialog:
ftp ftp.diku.dk ftp ftp.dcs.ed.ac.uk
Name: anonymous Name: anonymous
Password: <your loginname@host> Password: <your loginname@host>
ftp> binary ftp> binary
ftp> cd diku/users/birkedal ftp> cd export/ml/mlkit
ftp> get README ftp> get README
ftp> get COPYING ftp> get COPYING
ftp> get src.tar.Z ftp> get src.tar.Z
ftp> get doc.tar.Z ftp> get doc.tar.Z
ftp> get tools.tar.Z ftp> get tools.tar.Z
ftp> get examples.tar.Z ftp> get examples.tar.Z
ftp> bye ftp> bye
The file README contains installation instructions. Note that no
binaries are distributed and that you must build these using either
Standard ML of New Jersey, or Poly/ML.
--------------------------------------------------------------------------
6. Unsupported SML/NJ Ports
This section describes various ports of SML/NJ (see section 5)
that are not directly supported by the NJ folks.
MS-DOS/Windows?
---------------
(From Dave MacQueen)
There is an MS-Windows/MSDOS implementation of Standard ML of New
Jersey available by annonymous ftp on research.att.com, directory
dist/ml/working/sml-386. This port was done by Yngvi Guttesen at the
Danish Technical University in Copenhagen, and it is based on version
0.75 of SML/NJ. The distribution consists of the following four
files.
-rw-rw-r-- 1 dbm other 417 Feb 16 1993 README
-rw-rw-r-- 1 dbm other 51375 Feb 7 1992 doc.tar.Z
-rw-rw-r-- 1 dbm other 749105 May 5 1992 mo.386.tar.Z
-rw-rw-r-- 1 dbm other 851445 Feb 7 1992 src.tar.Z
This Windows port is rather delicate, and when we got it we had a lot
of trouble getting it working here at Bell labs. We tried several
different machines and finally found one on which it would run (a
Gateway 2000 with 16 MB of RAM), though even then it was not very
robust or fast. It seemed to be a problem of finding a machine with
just the right memory management configuration. I must admit that
memory management under Windows is a black art that I am not familiar
with, so I have no idea how to characterize the required memory
configuration.
My conclusion is that the current Windows 3.1/MSDOS environment is so
difficult that it would require a major additional investment to have
a really useful port. Guttesen did not have a 32 bit C compiler
available, so he rewrote the runtime system in assember, which makes
it difficult to modify his port. An alternative is to wait for
Windows NT (Win32) or OS/2 ports, which may be done in the coming
months (a couple of people have independently been working on OS/2
ports recently). Another alternative is to look in directory pub/ml
of ftp.dcs.ed.ac.uk, where there are a couple of (partial)
implementations of SML that run on PCs. A third alternative is to
look into Xavier Leroy's CAML Light. (Details of these are in the
comp.lang.ml FAQ message.)
However, Guttesen's 386 code generator was used by Mark Leone of CMU
as the basis for a port to Unix on Ix86 machines. The current release
of SML of New Jersey (0.93) incorporates Intel/Unix support for Mach
(used at Carnegie-Mellon University), BSD386 (a product of BSDI?), and
386bsd (a free version of Unix for the PC). There are also versions
that run under Linux (available as part of the free Linux distribution)
and SVR4, although we have not yet integrated the code supporting
Linux and SVR4 into the distributed 0.93 runtime system. Interest has
been expressed in a port for SCO Unix, but, as far as we know, no one
has done such a port.
Very recently Peter Bertelsen of the Technical University of Denmark
has done a port to OS2, which is now available on research.att.com,
directory dist/ml.
Linux?
------
(Thanks to Ralf Reetz, Peter Su, and Mark Leone)
Various ftp sites that seem to carry SML/NJ version 0.93 for Linux:
ftp.rz.uni-karlsruhe.de:/linux/mirror.tsx/
binaries/usr.bin/njsml.93.bin.z
sources/usr.bin/njsml.93.linux.README
sources/usr.bin/njsml.93.linux.README.NEW
sources/usr.bin/njsml.93.linux.diffs.z
sources/usr.bin/njsml.93.src.tar.z
ftp@tsx-11.mit.edu:/pub/linux/
sources/usr.bin/njsml.93.src.tar.z
ftp.dcs.glasgow.ac.uk?
From the README file:
Standard ML of New Jersey
Version 0.93 for the i386/i486 running Linux, April 23, 1993
__ WHAT
SML/NJ is a compiler for the functional programming language
Standard ML (SML). It is a fairly complete and robust
implementation of ML.
__ FILES
njsml.93.bin.z - gzip'd binary of njsml (no SourceGroup)
njsml-sg.93.bin.z - gzip'd binary of njsml with SourceGroup
njsml.93.src.tar.z - minimal sources for NJSML on Linux
njsml.93.mo.i386.z - you'll need these also to compile on Linux
You can pick up additional tools and goodies from:
research.att.com
under the "ml" directory.
__ HISTORY
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).
__ RECOMMENDED ENV
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.
__ WHERE
NJ-SML 0.93 should be available at most major Linux sites. It
should also be available in:
sbcs.sunysb.edu:/pub/linux
by the time you are reading this.
OS/2:
-----
Standard ML of New Jersey (version 0.93) has been ported to PC's running OS/2.
Signal handling is not implemented. This port has been implemented using Mark
Leone's code generator for Intel 80386 and the Unix emulator emx, copyright of
Eberhard Mattes. SML/NJ is copyright of AT&T Bell Laboratories.
There is no warranty of any kind!
Requirements:
- IBM OS/2 version 2.x
- HPFS file system (long file names required)
- emx version 0.8g or later
- '.mo' files for i386
The port is available for anonymous ftp from research.att.com (in /dist/ml)
and, in Europe, from ftp.id.dth.dk (in /pub/bertelsen):
93.os2port.zip Archived with Info-ZIP's Zip utility
93.os2port.tar.Z Archived with GNU's tape archive utility
93.os2port.txt Port announcement & installation guide
Please note that the .tar.Z and .zip version of the SML/NJ port are exactly
alike and both contain a full source set (but no '.mo' files) for compiling
to OS/2 with emx/gcc (not included).
The i386 '.mo' archive (93.mo.i386.tar.Z) is available from research.att.com
(in /dist/ml) and princeton.edu (in /pub/ml). The emx environment is available
from various OS/2 related ftp sites, e.g. ftp-os2.cdrom.com.
A binary-only release of this SML/NJ port (no source, interactive system
executable only) is also available for anonymous ftp from ftp-os2.cdrom.com.
If you have questions concerning this port, please send email to:
Peter Bertelsen (c917023@id.dth.dk)
Department of Computer Science, Technical University of Denmark
FreeBSD:
--------
SML/NJ is also available in source and binary format for FreeBSD from
freebsd.cdrom.com:/pub/FreeBSD/packages/sml_src.tgz and sml_bin.tgz.
The binary package includes EXene and CML as well.
--------------------------------------------------------------------------
5. Where can I find documentation on SML?
THE DEFINITION.
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.
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
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
Cambridge University Press 1991
ISBN: 0-521-39022-2
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)
The following report is available from the LFCS (Lorraine Edgar,
lme@dcs.ed.ac.uk) and costs 5 pounds or 10 US dollars. It covers all of
Standard ML. The report is also available via the World Wide Web off of
http://www.cs.cmu.edu:8001/afs/cs.cmu.edu/project/fox/mosaic/HomePage.html.
Alternatively, the report can be ftp'd from ftp.cs.cmu.edu as the file
/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 is available from the LFCS (Lorraine Edgar,
lme@dcs.ed.ac.uk) and costs 2.50 pounds or 5 US dollars for single
copies and 1.50 pounds or 3 dollars when bought in bulk. It includes
an introduction to Standard ML and 3 lectures on the modules system.
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 is available from the LFCS (Lorraine Edgar,
lme@dcs.ed.ac.uk) and is free. It introduces Extended ML, a language
for writing (non-executable) specifications of Standard ML programs and
for formally developing Standard ML programs from such specifications.
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
--------------------------------------------------------------------------
6. Where can I find library code?
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
(Lorraine Edgar, lme@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
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.
--------------------------------------------------------------------------
7. Theorem Provers and ML
(Collected by Paul Black, pblack@cs.berekeley.edu. Thanks Paul!)
- LCF (Edinburgh LCF and Cambridge LCF)
* written in the original Edinburgh dialect of ML from which SML developed.
"Logic and Computation: Interactive Proof with Cambridge LCF"
also by Lawrence C. Paulson.
- 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
elsa@research.att.com, slind@informatik.tu-muenchen.de
http://lal.cs.byu.edu/lal/hol-documentation.html
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
directory = local/lehrstuhl/nipkow/hol90/hol90.6.tar.Z
or
machine = research.att.com
directory = dist/ml/hol90/hol90.6.tar.Z
- NuPrl (from Bob Constable`s group at Cornell)
- Isabelle (Lawrence C. Paulson, Cambridge Univ. )
* has rewriting, but not many decision procedures. It does has
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 <gannet.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 Caml-Light (but Caml-Light and SML are VERY similar)
* no serious automated reasoning subsystems (other than
higher-order resolution), but has a VERY nice package for
program verification.
* available via anon. ftp from ftp.inria.fr:/INRIA/coq/V5.8
* possible contact: Chet Murthy <murthy@cs.cornell.edu>
- 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, neither of which is free.
- 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 alonzo.tip.cs.cmu.edu (128.2.209.194)
in the directory /afs/cs/user/fp/public.
* A bibliography and a collection of papers regarding LF and Elf
can be found in the directory /afs/cs/user/fp/public/elf-papers.
* There is an Elf mailing list. Contact elf-request@cs.cmu.edu to join.
* For further information, contact Frank Pfenning (fp@cs.cmu.edu).
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
We have an automated theorm proving system here at the University
of Tasmania, but it is still under development, currently
riddled with bugs and has an obscure "input language"; aside
from those minor problems, it'd be perfect...
La Monte H. Yarroll <piggy@hilbert.maths.utas.edu.au>
Edinburgh's Concurrency Workbench and Sussex's Process Algebra
Mauipulator are also ML systems of note, though neither are
interactive theorem provers.
--------------------------------------------------------------------------
8. Miscellaneous
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, 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.CInterace 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.
How do I get the emacs mode to work with Emacs version 19?
Add these three lines at the top of your `sml-init.el' file:
- ----- BEGIN addition
; emacs 19 doesn't have `make-shell', which sml-shell needs, so get it
; when necessary. 12 Oct 1993 M-J. Dominus (mjd@saul.cis.upenn.edu)
(autoload 'make-shell "make-shell" "Make and initialize shell buffer for SML." nil)
- ----- END addition
They tell emacs to load the file `make-shell.el' when it needs to use
the `make-shell' function.
Then install this file as `make-shell.el' somewhere on your load path,
probably in your emacs `site-lisp' directory:
Reference in New Issue View Git Blame Copy Permalink