ML(ID:620/ml:001)

Meta Language 


Meta Language. R. Milner Edinburgh et al, 1973. A strict higher-order functional language with statically-checked polymorphic types, garbage collection and a formal semantics. It began as the metalanguage for the Edinburgh LCF proof assistant. (LCF="Logic for Computable Functions")

LCF ML was implemented in Stanford LISP. Cardelli (1981) implemented ML in Pascal, using the FAM (Functional Abstract Machine).

(Meta-language) is a family of advanced languages with  (usually) functional control structures, strict semantics, a strict polymorphic type system and parameterized modules. The family includes; Standard ML, Lazy ML, Caml, Caml Light, and various research languages.



Places
People:
Structures:
Related languages
Edinburgh LCF => ML   Meta language for
ML => CAML   Dialect of
ML => Elle   Based on
ML => EML   Evolution of
ML => EML   Extension of
ML => FIML   Extension of
ML => Galileo   Based on
ML => HOL-88   Written using
ML => HOL-88   Based on
ML => IFX   Extension of
ML => INFER   Incorporated some features of
ML => LML   Variant
ML => Lucid Synchrone   Evolution of
ML => MCPL   Influence
ML => Mini-ML   Implementation of
ML => Miranda   Strong, Influence
ML => ML-Twig   Written using
ML => Modular Prolog   Influence
ML => NESL   Based on
ML => Ontic   Influence
ML => PFL   Extension of
ML => POPLOG   Implementation
ML => PROP   Incorporated some features of
ML => RUSSELL   Extension of
ML => SML   Evolution of
ML => Sticks&Stones   Adaptation of

References:
  • Gordon , M.J.C. et al "A Metalanguage for Interactive Proof in LCF" view details
          in [ACM SIGACT-SIGPLAN] Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages 1978 , Tucson, Arizona view details
  • Harland, David M. "Polymorphic Programming Languages", Ellis Horwood 1984. view details
          in [ACM SIGACT-SIGPLAN] Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages 1978 , Tucson, Arizona view details
  • Albano, Antonio; Cardelli, Luca and Orsini, Renzo "Galileo: A Strongly Typed Interactive Conceptual Language" view details Abstract: Galileo, a programming language for database applications, is presented. Galileo is a strongly-typed, interactive programming language designed specifically to support semantic data model features (classification, aggregation, and specialization), as well as the abstraction mechanisms of modern programming languages (types, abstract types, and modularization). The main contributions of Galileo are (a) a flexible type system to model database structure and semantic integrity constraints; (b) the inclusion of type hierarchies to support the specialization abstraction mechanisms of semantic data models; (c) a modularization mechanism to structure data and operations into interrelated units (d) the integration of abstraction mechanisms into an expression-based language that allows interactive use of the database without resorting to a new stand-alone query language. Galileo will be used in the immediate future as a tool for database design and, in the long term, as a high-level interface for DBMSs. Extract: Galileo: relation to previous work
    The design of Galileo has been influenced by two areas of research: conceptual modeling and programming languages. Although these areas have a number of overlapping issues, there are problems to be solved if the results from both areas are to be successfully integrated. Galileo applies results from the conceptual modeling sector for features related to object-oriented databases, declarative definitions of constraints, multiple descriptions of objects, and view modeling.
    Galileo borrows features such as data types, abstract types, and modularization from the programming language area. Although the utility of such features is recognized both pragmatically and theoretically, they have mainly been studied for applications to temporary data (i.e., not involving databases).
    The database proposals that have most influenced the design of Galileo are TAXIS, DIAL, and ADAPLEX. TAXIS is notable for introducing the basic knowledge representation mechanisms of semantic networks on data, transactions, and exceptions and for its approach to user dialogue modeling. DIAL, which has evolved from SDM, uses data types, classes, derived classes, the ?port? mechanism to deal with user interaction, and features to control concurrency at the conceptual level. Finally, ADAPLEX uses semantic data model features in a strongly-typed programming language, namely, Ada.
    The main contributions of Galileo are
    (1) the integration of features to support semantic data model abstraction mechanisms within an expression-based, strongly-typed programming language;
    (2) a systematic use of both concrete and abstract types to model structural and behavioral aspects of a database;
    (3) the inclusion of type hierarchies to support the specialization abstraction mechanism of semantic data models as well as a software development methodology by data specialization
    (4) the proposal of another abstraction mechanism, modularization, to organize a conceptual scheme in meaningful and manageable units, so as to deal with data persistence without resorting to specific data types such as files of programming languages, and to deal with application-oriented views of data in a similar way to the view mechanism of DBMSs;
    (5) a small number of independent primitive features that can be applied orthogonally, that is, in any combination.
    The basic ideas of Galileo have been investigated in ELLE, a programming language designed to deal uniformly with temporary and persistent complex data, that is, without resorting to special data type constructors to deal with permanent data. Both ELLE and Galileo borrow many of their features from the functional programming language ML. Extract: Galileo TYPE HIERARCHIES
    TYPE HIERARCHIES
    An important property of the Galileo type system is the notion of subtype: if a type u is a subtype of a type v (u C v), then a value of type u can be used in any context where a value of type v is expected, but not vice versa. The subtype relation is a partial order. For instance, if a function f has a formal parameter of type v, then an application of f to a value of type u is correctly typechecked because no run-time errors can occur. It is important to stress the point that since Galileo has a secure type system, the notion of type hierarchies is related to that of well-typed expressions [24, 281: expressions that are syntactically well typed are always semantically well typed (i.e., such expressions do not cause runtime type errors, and give a value of the correct type). In Milner?s words, ?welltyped expressions do not go wrong? also [36] apply to hierarchies among types.
    This notion of type hierarchies is different from the subtype concept of Ada, but is similar to the subclass mechanisms of Simula 67 and Smalltalk. In Galileo, this notion is extended to all the types, in the sense explained in the sequel to this paper, while preserving two important properties: the language is still strongly-typed and the functions need not be recompiled in order to be used on parameters of any subtype.
    With this mechanism Galileo supports the notion of programming by data specialization, originally introduced in Simula 67 and generalized in TAXIS to all the constituents of a database application: data, transactions, assertions, and scripts. Complex software applications, especially those related to databases, can be designed and implemented incrementally. Once a set of functions has been designed and tested for the most general data, it can be used with data of any subtype introduced later on in the software development process. Moreover, new functions on the subtypes can be defined in terms of the old functions.
          in ACM Trans Database Sys 10(2) June 1985 view details
  • Gries, D. and J. Prins (1985). "A new notion of encapsulation." view details Abstract: Generally speaking, a `module' is used as an `encapsulation mechanism' to tie together a set of declarations of variables and operations upon them. Although there is no standard way to instantiate or use a module, the general idea is that a module describes the implementation of all the values of a given type. We believe that this is too inflexible to provide enough control: one should be able to use different implementations (given by different modules) for variables (and values) of the same type. When incorporated properly into the notation, this finer grain of control allows one to program at a high level of abstraction and then to indicate how various pieces of the program should be implemented. It provides simple, effective access to earlier-written modules, so that they are usable in a more flexible manner than is possible in current notations. Existing languages such as SETL, Smalltalk, ML, CLU, and Ada already provide some of the capabilities listed above, but our new notion may provide more flexibility and ease of use. The paper is organized as follows. Section 2 gives some basic ground rules for our programming notation and outlines our idea for encapsulation. Section 3 discusses some of the issues involved. Section 4 outlines proofs of correctness. Section 5 discusses a `real' example in detail. This is a report of ongoing work, and not a finished product.     
          in SIGPLAN Notices 20(07) July 1985 (Proceedings of the ACM SIGPLAN 85 symposium on Language issues in programming environments) view details
  • Paulson, LC "Lessons learned from LCF: a survey of natural deduction proofs" pp474-479 view details
          in The Computer Journal 28(5) 1985 view details
  • Mitchell, J. C.; and Harper, R. "The essence of ML" pp28-46 view details Abstract: Standard ML is a useful programming language with polymorphic expressions and a flexible module facility. One notable feature of the expression language is an algorithm which allows type information to be omitted. We study the implicitly-typed expression language by giving a ?syntactically isomorphic? explicitly-typed, polymorphic function calculus. Unlike the Girard-Reynolds polymorphic calculus, for example, the types of our ML calculus may be built-up by induction on type levels (universes). For this reason, the pure ML calculus has straightforward set-theoretic, recursion-theoretic and domain-theoretic semantics, and operational properties such as the termination of all recursion-free programs may be proved relatively simply. The signatures, structures, and functors of the module language are easily incorporated into the typed ML calculus, providing a unified framework for studying the major features of the language (including the novel ?sharing constraints? on functor parameters). We show that, in a precise sense, the language becomes inconsistent if restrictions imposed by type levels are relaxed. More specifically, we prove that the important programming features of ML cannot be added to any impredicative language, such as the Girard-Reynolds calculus, without implicitly assuming a type of all types. DOI
          in [ACM SIGACT-SIGPLAN] Proceedings of the Fifteenth Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, San Diego, California (January 1988) view details
  • Spinellis, Diomidis D., "Programming Paradigms as Object Classes: A Structuring Mechanism for Multiparadigm Programming", PhD Thesis 1994 University of London view details
          in [ACM SIGACT-SIGPLAN] Proceedings of the Fifteenth Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, San Diego, California (January 1988) view details
  • Library of Congress Subject Headings M6 view details
          in [ACM SIGACT-SIGPLAN] Proceedings of the Fifteenth Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, San Diego, California (January 1988) view details