A White Paper on CAMlog Contents 1. Language Characteristics 2. Goals Of The Project 3. Implementation And Interoperability 4. Imperative (Monadic) Elements 5. Logic Style Syntax 6. CAMlog And The History Of Constructive Mathematics Other Papers - A Gentle Introduction To CAMlog - CAMlog Language Description (NOT YET) - CAMlog User Guide (NOT YET) - CAMlog Scripting API documentation (NOT YET) - CAMlog Quick Reference (NOT YET) Abstract CAMlog incorporates an abstract model of computation, a language that syntactically represents this model and a rigorous implementation of both. The language is functional with a logical flavor and some typically imperative (monadic) features built on top of it. The system is essentially Java based and thus has good Java-interoperability. This paper summarizes the goals and ideas behind CAMlog. 1. Language Characteristics These are the principal design concepts - The basis of CAMlog a lambda calculus with pairs, making it a purely declarative functional language with patterns. - On top of that basis there is a layer of the imperative ('monadic') features continuation, alternation and (NOT YET) state. Strict evaluation ensures this layer is efficiently mapped to the underlying operational semantics. - Control structures of CAMlog mimic logic programming (or definite clause grammars) and admit backtracking, but do not refer to refer to resolution calculus; we call this 'logic style'. - CAMlog is statically typed, admits polymorphism and algebraic type definitions. In CAMlog typings are infered. 2. Goals Of The Project a. What CAMlog Is Good For Generally declarative languages show their most strength in so-called 'intelligent' applications: complex structures and algorithms with a high level of abstraction having nontrivial semantics behind it. CAMlog is intended to be used as a scripting engine in modeling applications; however it is still a general purpose language. With the implementation we want to show that there is no contradiction between real life scripting applications and decarative purity. b. The Future Of CAMlog It should be noted that CAMlog is still an experiment, in particular the intended inclusion of states/objects/processes will change the language. The implementation will soon be extended by a blindingly fast C-backend, using C-based interpretation and/or Compilation to C. 3. Implementation And Interoperability The CAMlog implementation is Java-based, which means that Java takes the role of an operating system around CAMlog. Sources are compiled to 'CAMlog operational code', which is then interpreted. The operational code may be serialized to a binary program file; a runtime version of the CAMlog virtual machine then suffices to execute the program. There is a simple, but fairly general concept of separate compilation: A CAMlog program can be written to evaluate to what is called an 'evaluation context', usually containing some definitions. The evaluation context can then be loaded into the system as an environment for separately compiled and interpreted code which may reference definitions from the context. A command line interface is provided interactively interpret a sequence of terms in some precompiled context for exercising, experimenting and rapid prototyping. Interfacing with the Java host language takes place on two levels - Backend (CAMlog calls Java): The computation model can easily be extended by Java implemented new 'builtin' operations. - Frontend (Java calls CAMlog): Java methods may call the CAMlog virtual machine to execute CAMlog code. 4. Imperative (Monadic) Elements a. A Remark On Programming Style The critcism on imperative programming style(!) customary in the software engineering community sometimes obfuscates the view on imperative programming as a model of computation, where it is indispensable for the sake of complexity. As declarative languages are longing for real life applicability, imperative elements have to come back into play. While in earlier days purity has been compromized (Scheme, ML), modern approaches rather preserve referential transparency by building an imperative level on top of the declarative structure, as in Haskell's and O'Haskell's monads, Clean's uniqueness types or Mercury's unique modes. The formal semantics ensures that the safe, but in a-priori interpretation inherently inefficient source code can be translated into an efficient operational code by one-to-one implementation of imperative features. b. The CAMlog Monads All CAMlog computations take place in an environment constituted by the composite of two (soon: three) implied monads (i) continuation (ii) alternation (iii) mutable state (NOT YET) Since the environment is implicit, one may well refer to CAMlog as an imperative language. The way in which the imperative features are combined however is not fully at the application programmers disposal but rather determined by the language concept. c. Monad Abstraction And The Monad Composition Problem Haskell's concept of incorporating imperative elements looks more pure and is more flexible, at the expense of leaving monad composition to the application programmer. This is a high price, since the monad combination problem has no canonical solution and can be rather intricate. The built in monads of CAMlog cover most applications (Note: when state is included, so NOT YET) and are carefully woven into syntax and type system. c. Monadic Bind Notation Monads are not a singular feature in Haskell, in fact the monad typeclass and their implementations are part of the standard library rather than as builtins. What makes monadic programming so smooth in Haskell is the 'do notation', defined by a syntactic transformation. The same effect is achieved in CAMlog by the two fundamental syntactic elements '>' (send to output variables) and ',' (compute sequentially) which together form a monadic bind operation. 5. Logic Style Syntax Syntactically CAMlog programs in some aspects look very much like PROLOG's Horn clause notation, and this is not a coincidence. Practically logic programs rarely ever make use of the full strength of the declarative semantics: Unifications most often have an implicit direction, meaning an assignment or some pattern matching. The variable dependencies moreover imply an order on the members of clauses, so resolution of conjuctions actually becomes sequential computation. CAMlog uses logic program notation exactly on this level: as a convenient way to express the control structure of monadic computations. The concepts of continuation and non-backtracking semantics appear rather natural in this setting, although they resemble the logically problematic concepts of of 'cut' and 'negation as failure'. 6. CAMlog And The History Of Constructive Mathematics Behind the Language is an extension of a computation model known as the 'Categorical Abstract Machine' (CAM) which has been developed mainly by French scientists at INRIA. It all began with Heyting, who formulated an alternative proof theoretic foundation for mathematics, known as intuitionistic logic (abandoning the law of excluded middle). The intention was to capture the notion of construction. There is conceptual relationship between Heyting's logic and an enriched lambda-calculus with pairs (the Curry-Howard corresponcence, as it is known in type theory), which brings us into the realm of functional computation. If we translate typed lambda calculus with pairs into combinatory logic, the result is the theory of a well known mathematical structure: a cartesian closed category (CCC). The equations of that theory already give rise to an interpreter that directly implements a denotational semantics. As was first observed by Cousineu, Curien and Mauny, the CCC combinators have a rather canonical translation into an operational semantics: the CAM. This model comes along so naturally, that I would like to refer to it as being 'discovered', while other abstract machines (like SECD, G-machine) had to be 'invented'.