Modified: 2012-09-13E-mail: Contact
Latest versions in Post Script and PDF formats:
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:
Changes since version 0.9.2:
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).
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.
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:
Changes since version 0.9.0:
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).
Modified: 2012-09-13
E-mail: Contact