HHM archive - HQL - HHM's Quantified Lambda

HQL - HHM's Quantified Lambda

Dated: miércoles, julio 13, 2005

HQL stands for HHM's Quantified Lambda (or Hernan's Quantified Lambda), and is a small functional language, whose expressions can involve the use of quantifier operators (for all, exists, etc).

It surely isn't a brilliant masterpiece, but it was a fun thing to do back then (july 2004), and even now it's surely interesting to see.

Downloads:

HQL interpreter: Haskell source
Full language specification, in Latex, PDF and HTML (below)
Original hand-written language specification (very unreadable): type inference and semantics

Full paper in HTML:
(see above for pdf and latex version)

HQL's language specification

by H. Hernán Moraldo

http://www.hhm.com.ar/ June 2005

About HQL

HQL stands for "HHM's Quantified Lambda" and it's a small programming language I created in 2004, for an Advanced Functional Programming class I had with professor Pablo E. Martinez Lopez. It's a very simple functional language, whose expressions can involve the use of quantifier operators (for all, exists, etc).

The following document presents the language formal specification, that is, the type inference for the language, and its semantics. It's the copy of the original hand-written specification, so it might be incomplete.

Visit http://www.hhm.com.ar/ to download the interpreter (with no parser) source code, and for any questions and comments, send mail to mg@moraldo.com.ar

A sample program

We want to have an example of the use of HQL, that shows what kind of language it is, and what kind of programs can be written with it.

Next code, shows a program written in HQL's abstract syntax (as there is no parser yet, you might have to convert it to Haskell data before executing it with the interpreter).

To make this program a real HQL program, all have to be converted to form, and binary operators like , and have to be converted either to BBBOp form, or to applications of functions as defined in the library (library is a non empty initial environment, as the one used by the interpreter). The full converted program would be:

Where code like is applying the function contained in variable to the expression .

The same program is presented in Haskell syntax as follows:

 xTerm6=(tForAllB "x"
  (tForAllB "y"
  (tIif 
  (tOr (tNot (TVar "x")) (TVar "y"))
  (tLogicIf (TVar "x") (TVar "y"))
  )
  )
  )

Where functions like and have been previously defined to make programming much faster.

It's interesting to ask what type has this program. According to the type inference algorithm, it's a . The program semantics is in this case , as the program is describing a truth that does not depend on any external variables (excepting those of the library).

HQL's language specification

Type inference

Definitions:

Base:

Integers:

Booleans:

Application:

Lambda:

Let .. in:

Explicit let .. in

If .. then .. else:

Exists:

would require some extra detail to be thrown in this specification. For now, let's just say that the

is a special type, that can be bool or a restricted integer, so

is a function that converts these special types into the ones accepted by the system.

Not:

IIIOp (others operators are similar):

Semantics

Environments:

Environments are sets of triples like this: , with being a variable name, the expression associated to (its value), and the environment where is defined.