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'.