Latest versions in Post Script and PDF formats:

- 2010-03-28: http://www.CeX3D.net/cexl/download/DefinitionCeXL_0.9.3.ps
- 2010-03-28: http://www.CeX3D.net/cexl/download/DefinitionCeXL_0.9.3.pdf
- 2004-07-27: http://www.CeX3D.net/cexl/download/DefinitionCeXL_0.9.2.ps
- 2004-07-27: http://www.CeX3D.net/cexl/download/DefinitionCeXL_0.9.2.pdf

Version 0.9.0 of CeXL was handed in as Anoq's bachelor's thesis at The Computer Science Department of the University of Copenhagen (DIKU) on the 19th of December 2003. Many mistakes in the semantics have been corrected since then in the latest version. Version 0.9.0 can still be downloaded in Post Script and PDF formats here, but it is outdated and has several mistakes:

- 2003-12-20: http://www.CeX3D.net/cexl/download/DefinitionCeXL_0.9.0.ps
- 2003-12-20: http://www.CeX3D.net/cexl/download/DefinitionCeXL_0.9.0.pdf

Changes since version 0.9.2:

- CeXL Implementation updated. Quite a few bugs have been fixed since the previous release and performance and error reporting have improved considerably. Notice however that certain things, such as error reporting, is even more improved in the supplied binary file than in the given source code. A few checks are still missing in the implementation, most notably pattern exhaustiveness and redundancy. Also, it is missing the check required as of this version 0.9.3 of the specification that, absent record fields are only removed at let-bindings for non-function and non-reference values. Since these checks are not implemented, the current implementation may implement an unsound version of the language. Support for CM project files has been added as well. A small CeXL Basis Library will be added at some point, but is currently not included. More than 8,000 lines of real-life CeXL code has been type-checked with this version!
- Small change of syntax: The meanings of semicolon (;) and comma (,) have been exchanged in named type parameter lists. Now the syntax is like this: '['a; 'b : absent | present, 'c : ~lab]', i.e. with semicolon between type variables which have the same restrictions and comma between type variables normally. The former syntax was taken from parameter lists in RenderMan Shading Language, but it turns out to be awkward and unfamiliar compared to Standard ML. The parameter lists are actually also a bit awkward in RenderMan Shading Language, as compared to C, which it tries to mimic. The motivation for doing it the other way around as now is that, the most common is that one just writes a list of type variables with different restrictions, in which case the familiar syntax with commas is preferred. Allowing multiple type variables to have the same restrictions is actually a new feature that CeXL introduces, compared to Standard ML, so it should also only be here that new syntax is introduced.
- A small change of semantics: Removing absent record fields is now only done for types of non-function and non-reference values, since doing this for reference values or function values may be unsound. This changes a couple of lines in the descriptions in sections 3.13, 5.9 and 15.6.
- A warning on potential future changes: Parts of the syntax and semantics, which makes CeXL incompatible with Standard ML, are subject to change in the future. In particular, the ordered type parameters should ideally behave in a way more similar to Standard ML and the explicit scoping of type variables at val bindings should as well. However, such changes should preserve the current features of CeXL, particularly the features "named type parameters" and "partial type instantiation" (as defined in section 2). Such changes involve some subtle design work, which does not currently have priorty for being done.
- Fixed problems with structure prefix and periods for internal identifier names in the translation from Naked CeXL to xi-Calculus.
- Corrected that the translation function xi_tyargs should be epsilon_tyargs in the translation function xi_ty for the case of type application (section 19.8).
- Improved the layout for the translation functions epsilon_packdec and epsilon_packstrbind, such that they, more or less, fit within the width of the page
- Fixed problem that the environments of type variables bound to restrictions were propagated from one declaration to the next in the translation from Naked CeXL to xi-Calculus.
- Fixed problem in the translation from Naked CeXL to xi-Calculus, where
declaration environments were generated several times in nested structures,
which resulted in datatype names and constructor names being regenerated
multiple times with incompatiple names. This also resulted in the translation
being less efficient to perform, if implemented directly from the semantics.
Implementing the new semantics directly with this problem fixed gave a front-end performance increase of approximately a factor 1.7 in the implementation, when compiling 6,600 lines of particular code, which was used for testing (in the year 2004, when this change was made).

- Made a time-complexity optimization in the semantics,
by changing the translation of value bindings from Naked CeXL to xi-Calculus.
This required adding a flag variable 'rec' to the epsilon
translation functions for patterns.
The operation of removing all exceptions and constructors from the environment, as was done earlier, took O(n) time in the number of declared variables. The same O(n) time-complexity was present for the operation of appending two value environments, as was also done earlier. Since both of these operations were done for each fun binding and recursive val binding in the program, this gave roughly O(n^2) time-complexity in the total number of variables in the program being translated, which is very bad.

Implementing this change to the semantics directly gave a front-end performance increase of approximately a factor 5.6 in the implementation, when compiling the 6,600 lines of code tested at that moment (in the year 2004). If the append operation was not removed, the performance increase was only about a factor 1.7, which most likely means that the time-complexity has actually dropped by this optimization. This should of course mean much higher factors of performance increase for larger programs.

- All of the optimizations described above have given a
performance increase
of a factor of 1.7 * 5.6 = 9.52 in total for
reading and type-checking
a particular program of 6,600 lines of CeXL code.
This performance increase was for the total time used
to parse, do Naked CeXL To xi-Calculus translation and type-inference -
so the performance increase in the translation from Naked CeXL to xi-Calculus
(where most optimizations were done) must have been bigger.
After all these optimizations had been implemented, it was possible to read, type-check the 6,600 line program in around 4 seconds on a 733 Mhz Pentium III running Linux. This time actually includes execution of the program, but the program only contained declarations, so only the top-level variable environment declarations were "executed". This "execution" is the slowest part, i.e. slower than parsing and type-checking.

Changes since version 0.9.1:

- CeXL Implementation updated.
- Fixed mistake in the Full CeXL grammar for the let construct and in the traslation from the Full grammar to the Naked CeXL grammar for the let and while constructs. The let and while constructs must always have an optional sequence of declarations in their bodies.
- The vid was missing and has been added to the Full CeXL Grammar of fvalbind and in the reduction of fvalbind from the Full CeXL Grammar to Naked CeXL.
- The syntax for restrictions of the form '{{lab1, lab}}' has been changed to '~{lab1, lab}'. Having '}}' as a keyword gives conflicts in the lexical part of the language.
- The syntax for optional fields in record patterns and record expressions has been changed to 'lab ?= v' instead of 'lab = .. v'.
- The notation for the "rest of the fields" in record patterns and record expressions has been changed to '... = v' instead of '... v'.
- The notation for the "rest of the fields" in record types has been changed to "... : 'a" instead of "... 'a".
- while has been renamed to fwhile, but while is still a reserved word. This is to avoid compatibility conflicts with SML'97.
- Use of declared restrictions have been changed to support long identifier names in the grammar, as they should.
- strdecs inside the strbind grammar production has been made optional, to allow for empty structures.
- Fixed mistake in the grammar of restriction declarations. The correct syntax is 'res r = ~{lab}' rather than 'res r of ~{lab}'. The example programs were correct in this respect.
- The optional keywords try and end for the handle and case expressions have been removed. They introduce a lot of ambiguity to the grammar, so that was a serious mistake :) This also eliminates try as a reserved word.
- Added syntactic limitations preventing any occurences of records with extensions without any labels. This goes for record types, record patterns and record expressions.
- Added syntactic limitation preventing the infix identifier = from occurring in patterns. Without this limitation, the syntax is ambiguous.
- The infix operator <> was missing in the lexical description.
- The description of how to form tokens for the lexical analysis has been changed.
- structure and struct were missing from the list of reserved words.
- Refactored type parameters into a separate non-terminal in the BNF-grammar. This affects the Naked CeXL Grammar, the Full CeXL Grammar, the reduction from Full CeXL Grammar to Naked CeXL Grammar and the translation from Naked CeXL to xi-Calculus. It doesn't change the language, but it simplifies the language specification a little :-)
- Refactored translation of type variables from Naked CeXL to xi-Calculus a little. This doesn't change the language.
- Added missing rules for record patterns ending in '...' in the translation from Naked CeXL to xi-Calculus.
- Added rules for checking that a type pattern respects a restriction. These rules are placed with the unification rules for xi-Calculus and are used in the translation of restrictions from Naked CeXL to xi-Calculus.
- Moved check for well-formed restrictions in translation from Naked CeXL to xi-Calculus from declaration of restrictions to where a sequence of restrictions are combined - i.e. to the translation of the syntactical class crestr.
- Corrected mistake in translation of the type variable in the fieldcase expression in translation from Naked CeXL to xi-Calculus.
- Corrected mistake for fn expression in translation from Naked CeXL to xi-Calculus.
- Corrected mistake in translation of typarams from Naked CeXL to xi-Calculus. The environment Delta was not added to the resulting environment as they should.
- Clarified how the quantification of datatype constructors is done in declarations of datatypes in the translation from Naked CeXL to xi-Calculus.
- Corrected mistake in translation of datatype bindings from Naked CeXL to xi-Calculus. The environment VE was not added to the environment produced by constructor bindings.
- Added missing rules for declarations of restrictions, types and datatypes in the translation from Naked CeXL to xi-Calculus. This is in the translation function xi-dec and no xi-Calculus code is inserted for these rules, but the rules must be there.
- Added missing rules for packing exceptions in structures in the translation from Naked CeXL to xi-Calculus.
- Fixed mistakes in all rules related to packing into structures in the translation from Naked CeXL to xi-Calculus: The function inn has been defined and all environment lookups are now done with the prefix inn(longVid).
- Fixed mistake in rule epsilon_packstrbind in the translation from Naked CeXL to xi-Calculus: The suffix .strId is now appended in the argument for epsilon_packstruct.
- Changed the semantics of xi-Calculus to allow well-formed restrictions to have only one type pattern in a sequence of mutually disjoint type patterns (instead of requiring at least 2 as before) . This is the only necessary requirement in the rest of the semantics.
- Fixed mistake in the semantics of the unification relation of xi-Calculus. The former rule (8) for unifying a meta variable with an extensible record is now split into 2 rules, for properly handling the case when the meta variable has no restrictions.
- Fixed mistakes in 3 of the rules in the semantics for the unification of two order independent records: 1) The rule for unifying two records both ending in the empty record has been extended to allow both sides to contain arbitraryly many absent fields as it should. 2) The same has been done for the rule for unifying two records both ending in a type variable (the same type variable on both sides, not meta variable). 3) The rule for unifying two records where one ends in a meta variable and the other ends in a type variable has also been changed, to allow one side of the record to contain arbitraryly many absent fields while unifying the other side with the record with the meta variable.
- Fixed another mistakes in 3 of the rules in the semantics for the unification of two order independent records: We now properly avoid binding a meta variable to an extensible record without any fields.
- Fixed mistake in the semantics of the rules for implicitly scoped type variables of xi-Calculus. The former rule for meta variables has been split into 2 rules, such that bound meta variables are tracked, as they should be.
- Fixed mistakes in the way that the closure operation was done for xi-Calculus type inference. This involves taking the sorrounding environment into consideration when forming the most general unifier in let and letrec. The premise about type variables in the rules for let and letrec has been removed as a consequence of this.
- Added requirement that the right-hand side of a datatype replication is in fact a datatype (but the basic types like int, real, string etc. are also currently allowed).
- Added the syntactical group program to the Full CeXL grammar and the Naked CeXL grammar. Also added a translation function for this in the translation from Naked CeXL to xi-Calculus. A small mistake has been fixed relating to this, namely that resulting translated program is now truly a sequence of let, letrec and letex expressions, as claimed in the comments.
- Added support for doing structure replication, e.g.: structure ST = SymbolTable. This concerns the grammar and the reduction from Naked CeXL to xi-Calculus, and adding this feature was very simple.
- What was called a theorem about exactly typed polymorphicly extensible records with optional fields and typecase, is now just called a claim with justification, since it is not precise enough to be called a theorem with proof.
- Some bugs in some regression tests may have been fixed. In particular, one invalid test program has been removed - it was supposed to be an illegal program but it was in fact legal.

Changes since version 0.9.0:

- CeXL Implementation updated.
- Mistakes in the inference rules of the static semantics
has been fixed. The changes makes the static semantics correct, and is
actually a slight simplification at some points. All the changes
are described in the following.
The two rules (62) and (76) in version 0.9.0 would not be able to handle any interesting programs if you think about it! It has been fixed by removing the old rules (61), (62), (75) and (76) - which also means removing 2 judgement forms entirely. The functionality of the old rule (62) was moved to rule (52) (which is called (51) in version 0.9.1) and similarly the functionality of (76) was moved to (73) (which is called (70) in version 0.9.1).

To make the above changes work, the rules for the unification relation had to be changed. The old rule (8) has been split into 2 rules, since extensible records has to be handled specially here.

The old rules (33) and (37) from version 0.9.0 have been removed, since the old (33) is not needed anymore. The old rule (37) is handled by the added special casing of records in the old rule (8), as just described above. Because of these changes, the relation "type respects restriction" may not be used on its own outside of the unification relation anymore. This means, that the descriptions of application of type functions in the CeXL to xi-Calculus translation now refers to unification of types, rather than types respecting a restriction. This actually makes the description more general and less dependent on the inner workings of the unification relation.

Proper occurs checks have been added to the rules of the relation "unifying order independent records".

One extra rule in the unification relation is necessary. This rule is called (8) in version 0.9.1.

Type patterns in restrictions with constructors now consistently (I hope) include constructor tags everywhere. These were missing some places and included other places before.

The rules for checking that type patterns are disjoint has been changed. The premises q, z >= 1, ensuring that there must be at least one constructor tag have been replaced by premises d, d' <> exn saying, that the constructor tag exn is disallowed, which is the true intention of those premises. Now it is only required that q, z >= 0.

Changed the rules for let and letrec, such that the "local" expression does not have the implicitly scoped type variables included for it's inference. Some issues relating to binding type variables in the closure operation has also been changed for let and letrec.

The way that binding of type variables was done for the closure operation was not quite good enough as it was in version 0.9.0. The description of the closure operation has now been updated to be adequate and (hopefully) correct.

In the rule for exception handling, the patterns must be exhaustive on exn (not on tau, as it was before).

Added the rule for fields in type specifications (I had forgotten to add it).

Added the rule for extensible records in record end type specifications. This rule is not necessary if the inference rules involving type specifications check the type specification before any other unification. However, the rule is added to make the semantics bullet-proof, no matter in which order the unification is done in a unification algorithm implementation.

The rule for extensible records in type specifications now explicitly mentions that record labels must be distinct.

For the rules for extensible record expressions and extensible record patterns, the omega is now defined (I had forgotten to define this).

Corrected the rule for implicitly scoped type variables in the fieldcase expression. The type variable alpha is not implicitly scoped, when it is already present in the given environment Delta.

Added rule for meta variables in the rules for implicitly scoped type variables in type specifications (I had forgotten to add this rule).

- Some of the initial environments had mistakes, which are now fixed. In particular, the constructor nil and the assignment operator := were incorrectly typed. The constructors ref, nil, ::, true, false and the exceptions Match and Bind have been removed from the static basis of xi-Calculus, since they will never occur as variables here - only as constructors. A few of the internal names in the environment for the Naked CeXL to xi-Calculus translation where incorrect and the operator <> was missing.
- Changed the grammar of the functional while loop in the full CeXL grammar. It now always includes end keyword end. The mistake that the body was an expression in the grammar but a sequence of declarations in the translation to Naked CeXL has also been fixed: The while loop now has a sequence of declarations in the body both places, as it should.
- Added some regression tests for extensible records.
- The source code for the implementation is no longer included in the report, since it is available separately. Including the code was only for the purpose of the submission of the bachelor's thesis.
- The descriptive parts of the document has been updated to reflect the most recent facts about what has been implemented etc.
- The preface no longer describes this document as my bachelor's thesis.
- The duplication of the comments for the Naked CeXL grammar has been removed from the appendices.
- Many spelling mistakes and formulation mistakes have been fixed.

Modified: 2012-09-13

E-mail: Contact