Ponder(ID:1512/pon001)

Jon Fairbairn, . Polymorphic, non-strict functional language. Has a type system similar to Girard's System F, also known as Lambda-2 or the polymorphic lambda calculus. Ponder adds extra recursive 'mu' types to those of F, allowing more general recursion.

Structures:
References:
  • Fairbairn, J. "Ponder and its Type System", TR 31, Cambridge U Computer Lab, Nov 1982 view details Abstract: Despite the work of Landin and others as long ago as 1966, almost all
    recent programming languages are large and difficult to
    understand. This thesis is a re-examination of the possibility of
    designing and implementing a small but practical language based on
    very few primitive constructs.

    The text records the syntax and informal semantics of a new language
    called Ponder. The most notable features of the work are a powerful
    type-system and an efficient implementation of normal order reduction.

    In contrast to Landin?s ISWIM, Ponder is statically typed, an
    expedient that increases the simplicity of the language by removing
    the requirement that operations must be defined for incorrect
    arguments. The type system is a powerful extension of Milner?s
    polymorphic type system for ML in that it allows local quantification
    of types. This extension has the advantage that types that would
    otherwise need to be primitive may be defined.

    The criteria for the well-typedness of Ponder programmes are presented
    in the form of a natural deduction system in terms of a relation of
    generality between types. A new type checking algorithm derived from
    these rules is proposed.

    Ponder is built on the ë-calculus without the need for additional
    computation rules. In spite of this abstract foundation an efficient
    implementation based on Hughes? super-combinator approach is
    described. Some evidence of the speed of Ponder programmes is
    included.

    The same strictures have been applied to the design of the syntax of
    Ponder, which, rather than having many pre-defined clauses, allows the
    addition of new constructs by the use of a simple extension mechanism.
    Abstract: This note describes the programming language ?Ponder?, which is
    designed according to the principles of referencial transparency and
    ?orthogonality? as in [vWijngaarden 75]. Ponder is designed to be
    simple, being functional with normal order semantics. It is intended
    for writing large programmes, and to be easily tailored to a
    particular application. It has a simple but powerful polymorphic type
    system.

    The main objective of this note is to describe the type system of
    Ponder. As with the whole of the language design, the smallest
    possible number of primitives is built in to the type system. Hence
    for example, unions and pairs are not built in, but can be constructed
    from other primitives.
  • Fairbairn, Jon "A new type-checker for a functional language" Technical Report UCAM-CL-TR-53 view details
  • Paiva, V. "Subtyping in Ponder", TR 203, Aug 1990 view details