E-mail:
(for spam-mail protection you cannot copy this e-mail address - you must spell it, and please don't mention this e-mail address on your own website)
Latest version in Post Script and PDF formats:
Version 0.9.0 of CeXL was handed in as my bachelor's thesis at The Computer Science Department (DIKU) of the University of Copenhagen on the 19th of December 2003. Some 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 mistakes:
Changes:
Changes:
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).
This history is only be relevant for those who read the early versions of the document. These early versions were called "PreV1.0" versions - even though the first complete version (my bachelor's thesis) got the version label 0.9.0 in the end :-) This history will be removed quite soon.
This version mostly have small corrections related to spelling and formulation. It is the first version of this specification which is considered "complete". A few changes and fixes might still be published in the future, which is why it is not yet labelled version 1.0.0.
Fixed problem in the Naked CeXL to xi-Calculus translation. It is now properly checked that translated types in declarations for types, datatypes and exceptions do not contain any free types. It is also verified that declared types and datatypes are well-formed according to the xi-Calculus syntax.
Fixed the problem in the static semantics that meta variables must be allowed. The implications of this and relation to the feature Partial Type Instantiation is also described now.
Completed description of initial environments and how to put it all together.
Added more description about subtle details of the static semantics and the Naked CeXL to xi-Calculus.
Properly described and examplified the requirement that the type variable of a fieldcase which is "cased out" must be explicitly mentioned whereever it occurs in the result type of the fieldcase.
Updated the example demonstrating the need for dynamically allocated exception names.
Enhanced the description of static and strong typing slightly and replaced the use of the term "dynamic typing" with "weak typing".
Many small general fixes and modifications to the descriptions.
The feature Optional Type Argument has been renamed to Partial Instantiation.
Identified (but not fixed) a small problem in the static semantics: Meta variables / free types must be allowed.
This document has also been heavily restructured since it is way too big for a bachelor's project. All the semantics are now just appendices. The introduction and examples part has got several impovements to the examples. A new walk-through of all the semantics has been added.
Fixed the following mistake in the semantics for the unification relation in the subsubsection "Unifying meta variables": Bindings to meta variables now include restrictions.
Fixed the following 2 mistakes in the semantics for the unification relation in the subsubsection "Making Record Fields Independent of Order": 1) Changed binding to meta variables so that it includes restriction. 2) Added rule for unifying with a meta variable without any restrictions.
Fixed the following 2 mistakes in the semantics for the unification relation in the subsubsection "Type Respects Restriction": 1) Added the rule for when a type does not have any restictions. 2) Removed the tags c1, ..., ck in the TyPat in the rule for TyCon respects TyPat (i.e. formerly rule (38) now rule (40)).
Added comment to the semantics for the unification relation in the subsubsection "Unifying Order Independent Records".
Completed the section with the lexical part of the syntax.
Added subsection considering record concatenation in the section "Results of Other Language Features Which Have Been Considered".
Fixed some spelling mistakes.
Fixed the following problems in the dynamic semantics: The pattern judgement now takes an environment as input for supporting dynamically allocated exception names. ExVal renamed to ex instead of k. Pack is now an ExVal rather than a ConsVal as it should be. Added inference rule for creating an ExVal. Added inference rule for handling primitive functions.
Fixed the following problems in the translation from Naked CeXL to xi-Calculus: Added rule for translating the type constructor ? when 'a and 'b are written in reverse order.
Fixed some spelling mistakes and added a few more comments to the introductory examples.
Added new section: "Initial Environments".
Added Appendix B with an implementation.
This is the first version of this definition which can be considered complete with all intended features of CeXL - including references, exceptions, simple nested structures, polymorphic extensible records, optional fields with a fieldcase construct etc. A few parts of the description are still missing - in particular the lexical part of the syntax and how to put it all together to form a program.
I believe I even managed to prove the following theorem:
"Exactly typed records supporting optional fields in a way usable by a fieldcase construct in a language with ML's polymorphism implies that record extension must be strict at the type level."