HAL
HAL is a strongly typed, weakly moded, constraint logic/functional language designed to support the construction and extension and use of new constraint solvers being developed jointly at the University of Melbourne and Monash University.

Introduction to HAL

Constraint logic programming (CLP) languages are evolving to support more flexible experimentation with constraint solvers. First generation CLP languages, such as CLP(R) [Jaffar et al 92], provided almost no support. They had a fixed underlying solver for each constraint domain which was viewed as a closed ``black box.'' Second generation CLP languages, such as clp(fd) [Diaz and Codognet 93], provided more support by viewing the solver as a ``glass box'' which the programmer could extend to provide problem-specific complex constraints. However, CLP programmers want more than this: they want to be able to develop new problem-specific constraint solvers, for example by using ``hybrid'' methods that combine different constraint solving techniques (see e.g. [Wallace 98]). For this reason, recent versions of the CLP languages ECLiPSe and SICStus support the addition and specification of new constraint solvers by providing features such as dynamic scheduling, constraint handling rules [Fruhwirth 98] and attributed variables [Holzbaur92]. Unfortunately, support for developing solvers in these languages is still less than satisfactory for the reasons detailed below. HAL is a new CLP language, explicitly designed to support experimentation with different constraint solvers and development of new solvers. Our specific design objectives were four-fold: HAL has four interesting features which allow it to meet these objectives. The first is semi-optional type, mode and determinism declarations for predicates and functions. Information from the declarations allows the generation of efficient target code, improves robustness by using compile-time tests to check that solvers and other procedures are being used in the correct way, and facilitates efficient integration with foreign language procedures. Type information also means that predicate and function overloading can be resolved at compile-time, allowing a natural syntax for constraints even for user-defined constraint solvers. The second feature is a well-defined interface for solvers. Solvers are modules which provide various fixed predicates and functions for initializing variables and adding constraints. Obviously, such an interface supports ``plug and play'' experimentation with different solvers. The third feature is support for ``propagators'' by means of a specialized delay construct. HAL allows the programmer to annotate goals with a delay condition which tells the system that execution of that goal should be delayed until the condition is satisfied. By default, the delayed goal remains active and is reexecuted whenever the delay condition becomes true again. Such dynamic scheduling of goals is useful for writing simple constraint solvers, extending a solver and combining different solvers. The fourth feature is a provision for ``global variables.'' These behave a little like C's static variables and are only visible within a module. They are not intended for general use; rather they allow the constraint solver writer to efficiently implement a persistent constraint store. A well-defined solver interface and global variables are, to the best of our knowledge, novel in the context of CLP. While declarations and dynamic scheduling are not new, incorporating them into a CLP language which also allows user-defined constraint solvers has proven challenging. In isolation, each feature is relatively well understood; it is their combination that is not. Major difficulties have been to provide (limited) automatic coercion between types, compile-time reordering of literals during mode-checking with appropriate automatic initialization of solver variables, and efficient, yet accurate mode and determinism checking in the presence of dynamic scheduling. Dynamic scheduling has also complicated the design of the solver interface since the choice and implementation of delay conditions is necessarily solver dependent. One interesting feature has been the need to provide an external and internal view of the type and mode of a solver variable.

An example of a HAL program

As a simple example, the following program is a HAL version of the now classic CLP program mortgage for modelling the relationship between P the principal or amount owed, T the number of periods in the mortgage, I the interest rate of the mortgage, R the repayment due each period of the mortgage and B the balance owing at the end. 
:- module mortgage.						 (L1)
:- import simplex.						 (L2)
:- export pred mortgage(cfloat,cfloat,cfloat,cfloat,cfloat).	 (L3)
:-        mode mortgage(in,in,in,in,out) is semidet.		 (L4)
:-        mode mortgage(oo,oo,oo,oo,oo) is nondet.		 (L5)
mortgage(P,0.0,I,R,P).						 (R1)
mortgage(P,T,I,R,B) :-                                           (R2)
        T >= 1.0,
        NP = P + P * I - R,
        mortgage(NP,T-1.0,I,R,B).
The first line of the file (L1) states that this is the definition of the module mortgage. Line (L2) imports a previously defined module called simplex. This provides a simplex-based linear arithmetic constraint solver for constrained floats, called cfloats. Line (L3) declares that this module exports the predicate mortgage which takes five {\tt cfloat}s as arguments. This is the \emph{type} declaration for {\tt mortgage}. Lines (L4) and (L5) are examples of \emph{mode of usage} declarations. Since there are two declarations, mortgage has two possible modes of usage. In the first, the first four arguments have an in mode meaning their values are fixed when the predicate is called, and the last has a mode out which means it is uninitialized when called, and fixed on the return from the call to mortgage. Line (L5) gives another mode for the mortgage where each argument has mode {\tt oo} meaning that each argument takes a ``constrained'' variable and returns a ``constrained'' variable. This more flexible mode allows arbitrary uses of the mortgage predicate, but will be less efficient to execute. Line (L4) also states that for this mode mortgage is semidet, meaning that it either fails. For example mortgage(0.0,-1.0,0.0,0.0,B) fails or succeeds with exactly one answer. For the second mode (L5) the determinism is nondet meaning that the query may return 0 or more answers. The rest of the file contains the standard two rules defining {\tt mortgage}. The first states that when the number of repayments is 0, then the balance is simply the principal. The second states that if the number of repayments is greater than one, then we make one repayment, compute the new principle NP and take out a mortgage with this new principle for one less time period. As an example of the advantages of overloading, imagine that we wish to write a module for handling complex numbers. We can do this by leveraging from the simplex solver. 
:- module complex.
:- import simplex.
:- export_abstract typedef complex -> c(cfloat,cfloat).
:- export pred cx(cfloat,cfloat,complex).       % access/creation 
:-        mode cx(in,in,out) is det.
:-        mode cx(out,out,in) is det.
:-        mode cx(oo,oo,oo) is semidet.
cx(X,Y,c(X,Y)).
:- export func complex + complex --> complex.   % addition 
:-        mode in + in --> out is det.
:-        mode oo + oo --> oo is semidet.
c(X1,Y1) + c(X2,Y2) --> c(X1+X2,Y1+Y2).
Note that the type definition for complex is exported abstractly, which means that the internal representation of a complex number is hidden within the module. This ensures that code cannot create or modify complex numbers outside of the complex module. Thus, this module also needs to export a predicate, cx, for accessing and creating a complex number. As this example demonstrates, the programmer can use functions. The symbol ``-->'' should be read as ``returns.'' Using this module the programmer can now use complex arithmetic as if it were built into the language itself. If both simplex and {\tt complex} are imported, type inference will determine the type of the arguments of each call to + and appropriately qualify the call with the correct module. As an example of solver implementation, consider implementing a simple integer bounds propagation solver. The following declarations can be used: 
:- module bounds. 
:- export_abstract typedef cint = ...  %% internal cint representation
:- export pred init(cint).
:-        mode init(no) is det.
:- export_only pred cint = cint.
:-             mode oo = oo is semidet.
:- coerce coerce_int_cint(int) --> cint.
:- export func coerce_int_cint(int) --> cint.  
:-        mode coerce_int_cint(in) --> out is det.
The type cint is the type of bounds variables. It might be defined, for example, as an integer indexing into a HAL global variable tableau, as an integer representing a CPLEX variable number, or as a C pointer for a solver implemented in C. Usually, a constraint solver type is exported abstractly. This ensures other modules cannot modify cint variables without calling module bounds. The init predicate is used to initialize a variable, its mode is no or new -> old. The compiler will automatically add appropriate calls to the initialization predicate in user code that makes use of the bounds solver. The equality predicate is required for all constraint solvers. In the above code for cints it is annotated as export_only. This indicates that it should be visible to importing modules but not within this module. This is useful because inside the module bounds we manipulate the internal (rather than the external) representation of cints using equality. We can, however, access the equality predicate by using explicit module qualification. A complete bounds module would also export declarations for (primitive constraint) predicates such as >=, <=, \==, as well as functions such as +, - and *. Automatic coercion is important because it allows constraints and expressions to be written in a natural fashion. Currently, the type system for HAL only supports simple coercion, namely, a type can be involved in at most one coercion relationship. Even handling this restricted kind of coercion is difficult and is one of the most complex parts of the type checking and inference mechanism. Automatic solver-dependent type coercion allows constraints and expressions to be written in a natural fashion. In this case, we would like to be able to write integer constants as cint arguments of predicates and functions, for example as in X + 3*Y >= Z + 2. Thus, we need to instruct the compiler to perform automatic coercion between an int and a cint. The coerce declaration does this, indicating that the coercion function is coerce_int_cint.

People involved with HAL

HAL Publications

Status

Currently, the HAL compiler, system and libraries consists of some 24,000 lines (comments and blank lines excluded) of HAL code (which is also legitimate SICStus Prolog code). HAL programs are compiled to Mercury (particular subsets of HAL can also be compiled to SICStus Prolog) which, in turn, compiles to C and makes use of the information in declarations to produce efficient code.

Current features:

Currently under development:

Related work

Broadly speaking, HAL unifies two recent directions in constraint programming language research. The first direction is that of earlier CLP languages, including CLP(R), clp(fd), ECLiPSe and SICStus. The second direction is that of logic programming languages with declarations as exemplified by Mercury [Somogyi et al 96]. Earlier CLP languages provided constraints and constraint solvers for pre-defined constraint domains and many provided dynamic scheduling. However, they did not allow type, mode and determinism declarations. Providing such declarations has influenced the entire design of HAL, from the module system to delay constructs. Another important difference is explicit language support for extending or writing constraint solvers. Like HAL, the Mercury language also provides type, mode and determinism declarations. It is probably the most similar language to HAL, and we have leveraged greatly from its sophisticated compilation support by using it as an intermediate target language. The key difference is that Mercury is logic programming based and does not support constraints and constraint solvers. Indeed, it does not even fully support Herbrand constraints since it provides only a limited form of unification. We know of only one other language that integrates declarations into a CLP language: CIAO [Hermenegildo et al 99]. The design of CIAO has proceeded concurrently with that of HAL. HAL has been concerned with providing a language for experimentation with constraint solvers. In contrast, CIAO has focused on exploring the design and use of more flexible declarations for program analysis, debugging, validation, and optimization, and on supporting parallelism and concurrency. Constraint solving in CIAO is inherited from the underlying \&-Prolog/SICStus Prolog implementation: solvers are written using attributed variables. Thus, CIAO does not provide an explicit solver interface, does not provide a dual view of constraint variables, requires the programmer to explicitly insert initialization and coercion predicate calls, and, if more than one (non-Herbrand) constraint solver is used, the programmer must explicitly call the appropriate solver.
  1. [Demoen et al 99a] B. Demoen, M. Garcia de la Banda, and P.J. Stuckey. Type constraint solving for parametric and ad-hoc polymorphism. In Procs. of the 22nd Australian Comp. Sci. Conf. , pages 217--228, 1999.
  2. [Diaz and Codognet 93] D. Diaz and P. Codognet. A minimal extension of the WAM for clp(fd). In Procs. of ICLP93, pages 774--790, 1993.
  3. [Fruhwirth 98] T. Fruhwirth. Theory and practice of constraint handling rules. Journal of Logic Programming, 37:95--138, 1998.
  4. [Harvey and Stuckey 98] W. Harvey and P.J. Stuckey. Constraint representation for propagation. In Procs. of PPCP98, pages 235--249, 1998.
  5. [Hermenegildo et al 99] M. Hermenegildo, F. Bueno, D. Cabeza, M. Garcia de la Banda, P. Lopez, and G. Puebla. The CIAO multi-dialect compiler and system. In Parallelism and Implementation of Logic and Constraint Logic Programming. Nova Science, 1999.
  6. [Holzbaur92] C. Holzbaur. Metastructures vs. attributed variables in the context of extensible unification. In Procs. of the PLILP92, pages 260--268, 1992.
  7. [Jaffar et al 92] J. Jaffar, S. Michaylov, P. Stuckey, and R. Yap. The CLP(\cal R) language and system. ACM Transactions on Programming Languages and Systems, 4(3):339--395, 1992.
  8. [Somogyi et al 96] Z. Somogyi, F. Henderson, and T. Conway. The execution algorithm of Mercury: an efficient purely declarative logic programming language. Journal of Logic Programming, 29:17--64, 1996.
  9. [Wallace 98] M. Wallace, editor. CP98 Workshop on Large Scale Combinatorial Optimiza tion and Constraints, 1998. http://www.icparc.ic.ac.uk/~mgw/chic2_workshop.html.

Disclaimer