[Prev][Next][Index][Thread]

Experimental Fmeet typechecker available


A typechecker for the typed lamba-calculus Fmeet [4,5], an extension
of Cardelli and Wegner's system Fsub [1] with intersection types
[2,3], is now available by anonymous FTP.

Intersection types and bounded quantification are complementary
mechanisms for extending the expressive power of statically typed
programming languages.  They begin with a common framework: a simple,
typed language with higher-order functions and a notion of subtyping.
Intersection types extend this framework by giving every pair of types
S and T a greatest lower bound, S/\T, corresponding intuitively to the
intersection of the sets of values described by S and T.  Bounded
quantification extends subtyping along a different axis by adding
polymorphic functions that operate uniformly on all the subtypes of a
given type.  A calculus including both supports the expressive
programming style of ML or Quest based on parametric polymorphism, in
addition to a rich form of ``coherent overloading'' -- so rich,
indeed, that it can be used to provide an simple form of abstract
interpretation during typechecking; for example, the addition function
can be given a type showing that it maps pairs of positive inputs to a
positive result, pairs of zero inputs to a zero result, etc.  A number
of example scripts are included with the distribution.

The typechecker is available in both source and binary form (for sun4
processors).  The sources may be recompiled on any machine running
Standard ML of New Jersey (version 93).

To retrieve the files, proceed as follows.  Remember to set the
connection type to binary; otherwise compressed files will come out as
garbage on the other end!

    ftp ftp.dcs.ed.ac.uk                [or 129.215.160.5]
    login: anonymous
    password: <your mail address>
    cd pub/bcp
    binary			        [don't forget this!]
    get fmeet.sun4.tar.Z               

The sources are in the file checkers.src.tar.Z in the same directory.

Enjoy,

        Benjamin Pierce

[1] Luca Cardelli and Peter Wegner, "On Understanding Types, Data
    Abstraction, and Polymorphism."  Computing Surveys, Volume 17, 
    number 4, December, 1985.

[2] Coppo, M. and Dezani-Ciancaglini, M., "An Extension of the Basic
    Functionality Theory for the lambda-Calculus."  Notre-Dame Journal of
    Formal Logic, 21, 4, pp. 685-693, October, 1980.

[3] John C. Reynolds, "Preliminary Design of the Programming Language
    Forsythe."  Technical report number CMU-CS-88-159, Carnegie Mellon
    University, June, 1988.

[4] Benjamin C. Pierce, "Programming with Intersection Types and
    Bounded Polymorphism."  Ph.D. thesis, Carnegie Mellon University,
    December, 1991.  Available as School of Computer Science technical
    report CMU-CS-91-205.

[5] Benjamin C. Pierce, "Intersection Types and Bounded Polymorphism."
    Conference on Typed Lambda Calculi and Applications, March, 1993.