![]() |
| Home > Programming > |
| Comp.Lang.ML FAQ [Monthly Posting] |
Section 2 of 2 - Prev - Next
some new language extensions for straightforward interlanguage working
with Java. It produces compact standalone compiled code which can be
run on any computer with a Java Virtual Machine. This release includes a
number of improvements over the original release (0.1), including
significantly better compilation times, better code generation, more complete
Basis library support, better error messages and friendlier language
extensions for interlanguage working.
Although there are limitations (most importantly a lack of
general tail-call optimisation), MLj is quite usable for many
small-to-medium projects. It can be used to write portable ML
applications and applets which make use of Java's standard libraries
for graphics, database access, networking, etc. and which interwork
with third-party Java code.
Visit the new MLj website at http://www.dcs.ed.ac.uk/~mlj/ to find
out more about MLj, see some example ML applets and download the MLj
0.2 distribution.
The compiler is distributed as source+standalone binaries for Sparc/Solaris,
Intel/Linux and Intel/Windows, and in source-only form for compilation under
SML/NJ version 110. It is covered by the GNU Public License version 2.
MLj was written by Nick Benton, Andrew Kennedy and George Russell of
the Cambridge Research Group of Persimmon IT, Inc. Please note that
Persimmon IT will no longer distribute or support the compiler;
instead, Ian Stark and Tom Chothia of the University of Edinburgh
have kindly offered to host the new download site. The original authors
continue to develop the compiler and it is hoped that further releases will
take place in the future.
MLton
-----
MLton is a whole-program optimizing compiler for the Standard ML
programming language. MLton runs on X86 machines with Linux, FreeBSD,
or Cygwin/Windows. MLton has the following features.
+ Generates standalone executables with good runtime performance
+ SML 97 compliant, with a mostly complete basis library
+ Fast IntInf based on the GNU multiprecision library (gmp)
+ Fast C FFI
+ Profiling
+ Supports large amounts of memory and large arrays.
+ Libraries for continuations, interval timers, random numbers,
resource limits, resource usage, signal handlers, sockets, system
logging, threads, and heap save and restore
For more information, go to the MLton home page.
http://www.mlton.org/
Send comments, questions, and bug reports to MLton@mlton.org.
HaMLet
------
HaMLet is a faithful implementation of the Standard ML programming
language (SML'97). It aims to be
* an accurate reference implementation of the language specification,
* a platform for experimentation with the language semantics or
extensions to it,
* a useful tool for educational purposes.
The implementation is intended to be as direct a translation of the
language formalisation found in the Definition of Standard ML as
possible, modulo bug fixes. It tries hard to get all details of the
Definition right. The HaMLet source code
* implements complete Standard ML,
* closely follows the structure of the Definition, with lots of cross
references,
* conforms to the latest version of the Standard ML Basis Library,
* is written entirely in Standard ML, with the ability to bootstrap,
* may readily be compiled with SML/NJ, Moscow ML, or MLton.
HaMLet can perform different phases of execution - like parsing,
elaboration (type checking), and evaluation - selectively. In
particular,
it is possible to execute programs in an untyped manner, thus exploring
the universe where even ML programs "can go wrong".
SML.NET
-------
SML.NET is a whole program compiler for full Standard ML that compiles
to the .NET Common Language Runtime. For more information, see
http://www.cl.cam.ac.uk/Research/TSG/SMLNET/
--------------------------------------------------------------------------
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.
OS/2:
----
An old port of SML/NJ ver. 0.93 to OS/2 exists. The port is no longer
being maintained, but may be downloaded from:
ftp://ftp.dina.kvl.dk/pub/Staff/Peter.Bertelsen/smlnj/0.93-os2/
Another unmaintained and somewhat incomplete port of SML/NJ
ver. 108.10 to OS/2 may be downloaded from:
ftp://ftp.dina.kvl.dk/pub/Staff/Peter.Bertelsen/smlnj/108.10-os2/
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
(see http://www.kingston.ac.uk/~bs_s075/EofFP.html for information and
updates)
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
(available at )
Lawrence C Paulson
ML for the Working Programmer (2nd Edition, ML97)
Cambridge University Press 1996
ISBN: 0-521-56543-X (paperback), 0-521-57050-6 (hardback)
http://www.cl.cam.ac.uk/users/lcp/MLbook/
Jeffrey D. Ullman
Elements of ML Programming (2nd Edition, ML97)
MIT Press 1997
http://www-db.stanford.edu/~ullman/emlp.html
G.Cousineau & M.Mauny
The Functional Approach to Programming
Cambridge University Press, 1998
[Uses CAML]
M.Felleisen & D.P.Friedman
The Little MLer
MIT Press, 1998
Chris Okasaki
Purely Functional Data Structures
Cambridge University Press, 1998.
ISBN: 0-521-63124-6
Michael R. Hansen, Hans Rischel
Introduction to Programming using SML
Addison-Wesley, 1999
ISBN: 0-201-39820-6
http://www.it.dtu.dk/introSML
John Reppy
Concurrent Programming in ML
Cambridge University Press 1999
ISBN: 0-521-48089-2
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
A revised, though still unstable web version of these notes is
available at:
http://www.cs.cmu.edu/People/rwh/introsml
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
Extended ML (EML) is a framework for specification and formal
development of SML programs. EML specifications look just like SML
programs except that logical axioms are allowed in signatures and in
place of code in structures and functors. Some EML specifications are
executable, making EML a "wide-spectrum" language which can be used to
express every stage in the development of a SML program from the
initial high-level specification to the final program itself and
including intermediate stages in which specification and program are
intermingled. Formally developing a program in EML yields an
interconnected collection of generic SML modules, each with a complete
and accurate axiomatic specification of its interface with the rest of
the system. Information about EML is available from
http://www.dcs.ed.ac.uk/home/dts/eml/
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://SML.sourceforge.net/Basis/
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.berkeley.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 and Tobias Nipkow, Munich)
* has integrated rewriting and classical reasoning
* a generic proof tool supporting the following formalisms among others:
i) FOL - first order logic
ii) HOL - higher order logic
iii) LCF - Logic of computable functions
vi) ZF - Zermelo-Fraenkel set theory
* There's a WWW page:
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
* 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 (Lemma 1)
* a commercial system using a reimplementation of HOL in SML
* http://www.lemma-one.com/ProofPower/index/index.html
- Lamdba/DIALOG (Abstract Hardware Ltd)
* a commercial tool written in Poly/ML
* contact ahl@ahl.co.uk
- Twelf (Frank Pfenning & Carsten Schuermann, Carnegie Mellon Univ)
* Twelf is a meta-logical framework for deductive systems.
* Twelf includes an implementation of LF, including type
reconstruction, the Elf constraint logic programming language,
and a preliminary inductive meta-theorem prover for LF.
* The implementation is written in SML'97 and has been tested
under SML/NJ and MLWorks on Unix and Windows platforms.
It also includes a complete user's manual, tutorial,
example suites, and an Emacs mode.
* Further information, including download instructions, information
on the mailing list, publications, etc. can be found at
http://www.cs.cmu.edu/~twelf
- 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?
The new versions of SML/NJ provide much better support for calling
out to C than version 93 did. There is a discussion of how to use
the C function interface off of the SML/NJ web page at
http://cm.bell-labs.com/cm/cs/what/smlnj/doc/SMLNJ-C/index.html
Where can I find an emacs mode for SML?
Look in the "Contributed Software" section of the SML/NJ distribution
page at http://cm.bell-labs.com/cm/cs/what/smlnj/software.html
Nowadays sml-mode works well with Emacs 19 and XEmacs 19, as well as
a number of different SML compilers.
Stefan Monnier has released a new version (3.9.3) with a number of
changes, including improvements to the indentation algorithm. The
new version is available at
ftp://rum.cs.yale.edu/pub/monnier/sml-mode
What is the value restriction?
The value restriction is a feature of SML '97 which was introduced to
address some issues with polymorphism in the presence of effects.
The basic idea is that when a variable is bound to a polymorphic
expression, it must be the case that the expression is tantamount to
a value: that is, that it is guaranteed not to raise an exception or
allocate memory. For the purposes of typechecking, the class of
values is conservatively approximated by the syntactic notion of
"non-expansiveness".
Values (non-expansive expressions) are:
- functions
- constants
- variables
- records of values
- constructors applied to values
So for example, while in the following code f has type 'a -> 'b -> 'b,
g cannot be given the type 'b -> 'b because of the value restriction.
fun f x y = y
val g = f 3
The expression (f 3) is polymorphic (at type 'b -> 'b) but is not a
value, and so the value restriction forbids g from being bound
polymorphically. Either the code will be rejected, or g will be
given a useless "dummy" type.
In practice, this is usually easy to get around by eta-expanding:
fun f x y = y
val g = fn x => f 3 x
More information on the value restriction is available from a number
of sources, in particular:
- Section 4.7 of "The Definition of Standard ML". (see above)
- Pages 321-326 of Paulson's "ML for the working programmer". (see
above)
- http://cm.bell-labs.com/cm/cs/what/smlnj/doc/Conversion/types.html#Value
This includes discussion of the particulars of SML/NJ's treatment
of the value restriction.
- Extensive discussion in the comp.lang.ml archives.
What is the difference between OCaml and Standard ML?
Jen Olsson has created a small chart comparing the OCaml and
Standard ML syntax: see
http://www.csd.uu.se/~jenso/programming/sml_vs_ml.txt .
An extended version written by Andreas Rossberg can be found at
http://www.ps.uni-sb.de/~rossberg/SMLvsOcaml.html
In addition to the original page it covers modules, records, and
some more stuff.
Section 2 of 2 - Prev - Next
| Back to category Programming - Discuss "Comp.Lang.ML FAQ [Monthly Posting]" |
| Home - Search - About the project - Forum - Feedback |
© 2005 allanswers.org | Terms of use