On Axiom Type-Checking and Trace Collection in Extended ML an old english draft

Mikołaj Konarski ^{∗}

               mikon@mimuw.edu.pl

22 Jun 1997

Contents

I Introduction 3

1 Overview of the field 3 1.1 Standard ML . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Extended ML . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.3 Natural Semantics . . . . . . . . . . . . . . . . . . . . . . . . 5 1.4 The EML Kit . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.5 Conclusions and Dependencies Diagram . . . . . . . . . . . . . 6

2 The Concept of Static Analisis 7

2.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

2.2 Basic Definitions . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2.1 Semantic Objects . . . . . . . . . . . . . . . . . . . . . 7 2.2.2 Judgments . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2.3 Principal Signatures . . . . . . . . . . . . . . . . . . . 8

2.3 The Extended ML Case . . . . . . . . . . . . . . . . . . . . . 8 2.3.1 Indeterminism . . . . . . . . . . . . . . . . . . . . . . . 8 2.3.2 Imposing . . . . . . . . . . . . . . . . . . . . . . . . . . 8

2.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

∗Institute of Informatics, Warsaw University, Warsaw, Poland.

II Theory 10

3 Axiom Type-Checking 10 3.1 Axioms in Signatures . . . . . . . . . . . . . . . . . . . . . . . 10 3.2 Modules Elaboration in QUASI-EML . . . . . . . . . . . . . . 11 3.3 A Naive Approach to the EML Rule 65 . . . . . . . . . . . . . 12 3.4 Comforting Lemma . . . . . . . . . . . . . . . . . . . . . . . . 12 3.5 The Mature Approach to the EML Rule 65 . . . . . . . . . . . 13 3.6 Validating Axioms . . . . . . . . . . . . . . . . . . . . . . . . 13

4 Interlude 14 4.1 Static Semantics of Signatures . . . . . . . . . . . . . . . . . . 15 4.2 Elaborating Signatures . . . . . . . . . . . . . . . . . . . . . . 15

5 In the Search for the Basis B_{e} 16 5.1 The Modest Basis . . . . . . . . . . . . . . . . . . . . . . . . . 16 5.2 The Ignorant Basis . . . . . . . . . . . . . . . . . . . . . . . . 16 5.3 The Omniscient Basis . . . . . . . . . . . . . . . . . . . . . . . 17 5.4 The Observation . . . . . . . . . . . . . . . . . . . . . . . . . 17

6 Trace Collection 18 6.1 Traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 6.2 Substitutions and trace collection . . . . . . . . . . . . . . . . 19 6.3 Trace Schemes . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

III Implementation 20

7 The Actual Implementation 20 7.1 Basic Conventions . . . . . . . . . . . . . . . . . . . . . . . . . 20 7.2 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 7.3 Traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

8 An Anegdote 21

References 23

Part I

Introduction

1 Overview of the field

1.1 Standard ML

The EML Kit can be used for type-checking and testing EML programs at all stages of their development.

The EML Kit can help in teaching EML or SML programming or in developing SML software with the EML formalism.

The EML Kit lets the EML authors and all the people involved in the EML-related work fiddle with a straightforward implementation of the EML language.

Current research concerning EML is centered on the Verification Semantics of EML and on issues which one may call “implementation” of the Verification Semantics. These include designing a proof theory for EML and building prototype provers. The Verification Semantics heavily uses the Static Semantics, e.g. for expressing the property of having a type. Moreover the Static Semantics of the EML is burdened with the responsibility of gathering various information for the Verification Semantics. The EML Kit contains an implementation of the Static Semantics of EML, including the “gathering” mechanisms.

The EML Kit can be thought of (with some amount of good will) as a fully deterministic, algorithmic and detailed description of the EML static and dynamic semantics.

The EML definition describes the EML language using a kind of BNF notation for its grammar, and an extension of the formalism called Natural Semantics for the Static and Dynamic Semantics. This form of presentation makes it possible to describe such a large system as EML in a relatively compact and clean way. There is a price to pay, however. Some small mistakes long remain unnoticed. Some mechanisms seem simple and unambiguous, but the first attempt to implement them shows that they are not. Some global relations between parts of the Definition are obscure until the modules hierarchy is described in a serious module-handling formalism, like the one of the SML programming language.

We hope that this report will describe results of the analysis of EML from the perspective of the EML Kit, as well as give an overview of the EML Kit seen as an EML “denotational definition”. We reckon, that a knowledge of at least the Definition of Extended ML [10] is essential for the understanding of our paper.

Now, there is a great need for an “implementation” of the EML Verification Semantics. We hope the EML Kit will help in as well as benefit from the current work on the EML proof theory, proof obligation generators, prototype provers, etc. Yet, as for now only the syntax and type correctness of axioms is checked by the EML Kit - there is no extra aid in proving them correct, sufficient or whatever.

In this paper I will describe two problems, that arose during the work on the implementation of the EML type-checking. The first problem is elaboration of EML signatures in the presence of axioms, and the second is collection of traces during the elaboration process. I will try to indicate the sources of dangerous errors, that can be made if no special care is taken of these problems. On this background I will sketch the correct solutions, mentioning some of their variants. At the end I will comment on the actual implementation of the correct algorithms, as they were incorporated into the EML Kit.

Standard ML (SML) [16] is a functional programming language, equipped with powerful modularization tools. Signatures are one of the components of the SML module system:

signature TOTAL_PREORDER =
sig
    type elem
    val leq : elem * elem -> bool
    (* leq should be a total preorder *)
end

structure OddRational : TOTAL_PREORDER =
struct
    type elem = int * int
    fun leq ((m, n), (k, l)) =
        if n = 0 andalso l = 0
            then m < 0 orelse (m > 0 andalso k > 0)
        else if (n < 0 andalso l >= 0) orelse (n >= 0 andalso l < 0)
                 then k * n <= m * l
             else m * l <= k * n
end

1.2 Extended ML

Extended ML (EML) [10] is a framework for the formal development of programs in Standard ML. High-level specifications and SML code, as well as a mixture of both can be expressed in the Extended ML language. As a language EML is an extension of (a large subset of) SML. In particular, EML signatures may contain axioms:

signature TOTAL_PREORDER =
sig
    type elem
    val leq : elem * elem -> bool
    axiom forall (a, b) => leq (a, b) orelse leq (b, a)
    and forall (c, d, e) =>
        (leq (c, d) andalso leq (d, e)) implies leq (c, e)
end

1.3 Natural Semantics

Similarly the Definition of Extended ML [10] extends in a sense the Definition of Standard ML [16]. Although many things are added, some errors and infelicities corrected and a few presentation conventions changed, the general structure is kept mostly intact and as much of the original text as possible is preserved.

The Definition of Extended ML uses a formalism called Natural Semantics (a kind of operational semantics) to describe the static semantics of EML. There is a collection of semantic objects, defined using mathematical notation, and a set of rules to be used in derivation of judgments of the form

C ⊢ phrase ⇒ A

which can be read “phrase elaborates to A in context C” (C, A are semantic objects, phrase is an EML phrase).

1.4 The EML Kit

The EML Kit [4] aims to be (the basis and test-bed for) a comfortable framework for the formal development of programs, using the Extended ML language, formalism and methodology.

Version 1.0, developed by Marcin Jurdziński, Mikołaj Konarski, Sławomir Leszczyński and Aleksy Schubert, is a complete implementation of the Extended ML programming language. It allows for parsing, type-checking and evaluation of arbitrary EML code, be it pure Standard ML or full-blown EML with its axioms and other specification constructs. All of this is done in a strict adherence to the formally defined EML Syntax, Static Semantics and Dynamic Semantics.

Now, there is a great need for an “implementation” of the EML Verification Semantics. We hope the EML Kit will help in as well as benefit from the current work on the EML proof theory, proof obligation generators, prototype provers, etc. Yet, as for now only the syntax and type correctness of axioms is checked by the EML Kit - there is no extra aid in proving them correct or sufficient.

The EML Kit is based on the ML Kit [2]; a flexible, clean and modularized interpreter of the Standard ML, written in Standard ML. The ML Kit is a faithful and as straightforward as possible implementation of the language described in the SML definition. The overall structure of the ML Kit resembles the structure of the SML definition, abstract syntax tree is almost literally the same and the design of many details, such as naming conventions, is inspired by the Definition.

1.5 Conclusions and Dependencies Diagram

The two facts — that the EML definition is an extension of the SML definition and that the ML Kit is so close to the latter — helped us in our efforts to make the EML Kit a faithful and clean implementation of Extended ML. We were able to extend the ML Kit analogously as the EML definition extends the SML definition, while retaining the style of the ML Kit programming. Thus we have formed a basis for the development of the future EML Programming Environment tools, such as the proof-obligations generator and provers. See the familiar looking diagram below.

”Srodowisko Programistyczne EML

EML Kit

ML Kit

[figure]

Definicja EML

[figure]

Definicja SML

[figure]

[figure]

2 The Concept of Static Analysis

2.1

2.2 Basic Definitions

2.2.1 Semantic Objects

2.2.2 Judgments

Judgments are sentences of the form

C ⊢ phrase ⇒ A

which can be read “phrase elaborates to A in context C” (C, A are semantic objects, phrase is an EML phrase).

The rules of the Static Semantics of EML serve to derive judgments, for example of the form :

B ⊢ sigexp ⇒ S, γ

Here B is a basis, sigexp is a signature expression and S is a semantic structure. The γ is a trace — for a time being we can think of it as a derivation tree; i.e. a tree labeled by the instances of the rules, representing a correct derivation of a judgment found in its root. The whole derivation can be read “in the basis B sigexp elaborates to S and γ”.

2.2.3 Principal Signatures

We say that (N)S with γ is principal for sigexp in B when (in simplification):

• B ⊢ sigexp ⇒ S, γ,

• whenever B ⊢ sigexp ⇒ S′, γ′, then (N)S≥S′ and γ ≻ γ′.

The “≥” relation is signature instantiation and the “≻” relation is trace generalization. Both have intuitively understandable meaning.

2.3 The Extended ML Case

2.3.1 Indeterminism

Fundamental concepts of the Static Semantics are defined using quantification over derivations. For example phrase is said to possess a type τ in a context C, if there exists a derivation of the sentence

C ⊢ phrase ⇒ τ

Let’s take a closer look at the simplest one:

\frac{C ⊢ exp^{•} ⇒ τ, U, γ}{C ⊢ exp^{•} terminates ⇒ bool, U, ϵ}  (11.4)

This can be read: ”if exp^{•} can elaborate in the context C to the type τ, set U and trace γ then exp^{•} terminates can elaborate in the context C to the type bool, set U and empty trace”. For the purpose of implementation we can read it ”if exp^{•} elaborates in the context C to its most general type τ, set U and its most general trace γ then exp^{•} terminates elaborates in the context C to the type bool, set U and empty trace”. This reformulation can be justified by an easy proof that Milner’s algorithms extended to cover this rule remains correct.

2.3.2 Imposing

Axioms can impose type sharing

functor F (Arg : sig
                     type t

                     val f : t -> int
                     type u
                     val a : u
                     axiom f a = 0
                 end) :
sig
    val b : int
end =
struct
    val b = Arg.f Arg.a
end

2.4

Static Semantics in indeterministic. In addition some of the conditions in the rules express properties of the form “for all derivations such that ϕ holds, ψ must hold” — good examples are the principality requirements appearing in the Static Semantics for Modules.

Because of the quantification over infinite sets, it is impossible to implement Static Semantics of EML literally. One has to translate it into a more “denotational” form (some prefer to call it a “deterministic” form) before it can be straightforwardly (at last) implemented in a programming language like SML. Such a reformulation is a non-trivial task.

Fortunately the similar problem concerning SML has been solved quite a while ago. Milner’s algorithm [3] is a well known skeleton for an SML Core language type-checker, and the proof of the Principality Theorem from Section A.2 of the Commentary on Standard ML [15] is a good guideline for dealing with SML Modules language. Last but not least, the ML Kit is a very clean and modest reformulation/implementation of the SML Static Semantics, based on the above-mentioned ideas.

Our work on reformulating the EML-specific fragments of the Static Semantics sometimes amounted to trivial extensions of e.g. Milner’s algorithm, the only work being a struggle with the ML Kit machinery. Sometimes however the extension required a proof of correctness, or a very good knowledge of the ML Kit design. And still sometimes a new approach had to be found, proven correct and implemented within the ML Kit frames.

Part II

Theory

3 Axiom Type-Checking

In SML there are no axioms. In EML axioms can appear as components of structures and signatures. Elaborating EML structures containing axioms is not very difficult, apart from the problem with trace collection described in detail in Section 6. Elaborating EML signatures with axioms is much more complicated.

3.1 Axioms in Signatures

Rule 65 (we consider here a slightly simplified version), describes the static meaning of syntactic signature as an element of a semantic domain Sig. The rule is a bit more complex in the Definition of EML than in the Definition of SML. The additional second and third premises serve to assure, that axioms do not impose any type sharing or setting of equality attributes. This restriction is expressed using the notion of strip — an operation that strips signature of its axioms. The EML rule 65 follows:

\frac{(N)S with γ principal for sigexp in B strip(sigexp, γ) = (sigexp′, γ′) (N)S with γ′ principal for sigexp′ in B}{B ⊢ sigexp ⇒ (N)S, (N)γ}

The main reason for this restriction is that EML programs at the end of their development process (when there are no specification constructs in place of executable code), should become correct SML programs as soon as all the axioms in their bodies are commented out. Consider the following example:

functor F (Arg : sig
                     type t
                     val f : t -> int
                     type u
                     val a : u
                     axiom f a = 0
                 end) :
sig

    val b : int
end =
struct
    val b = Arg.f Arg.a
end

This is not correct, because the axiom imposes that type t is equal to u. If not for the restriction in rule 65 the program would be correct, but then its stripped version would be an incorrect SML program, because of the application of Arg.f to Arg.a.

3.2 Modules Elaboration in QUASI-EML

Let QUASI-EML be a dialect of EML, with second and third premises removed from rule 65. In QUASI-EML rule 65 looks as follows:

\frac{(N)S with γ principal for sigexp in B}{B ⊢ sigexp ⇒ (N)S, (N)γ}

Lemma 3.1. In QUASI-EML type abbreviations can be defined as derived forms.

Instead of a rigorous proof let’s consider the example of type abbreviation taken from [15], p.66:

sig
    type 'a t
    type u = int t (* a type abbreviation *)
    sharing type u = int
end

and it’s translation into QUASI-EML:

sig
    type 'a t
    type u
    axiom true orelse (forall (c : u, d : int t) => c == d)
    sharing type u = int
end

Corollary 3.2. In QUASI-EML reconstruction of principal signatures is undecidable.

The clue is, that type abbreviations in conjunction with sharing specifications make reconstruction of principal signatures as hard as second order unification. (In case of the above example, second order unification would be required to decide whether Λ'a.int or Λ'a.'a is the most general type function which can be assigned to t.) As second order unification is undecidable, we get the undecidability of principal signature reconstruction in QUASI-EML.

3.3 A Naive Approach to the EML Rule 65

Now, let’s come back to the problem of elaboration of the Extended ML signatures. Looking at rule 65 we can conceive an idea, that the most natural solution is the following (for simplicity we disregard traces here):

1. elaborate the original sigexp and obtain its principal signature (N)S,

2. strip sigexp of its axioms getting sigexp′,

3. elaborate sigexp′ and obtain principal signature (N′)S′,

4. if (N)S and (N′)S′ are identical then (N)S is the result, otherwise the signature is incorrect.

Unfortunately, the implementation of the first step is impossible, because it would also be a solution to the (undecidable) problem of principal signature reconstruction in QUASI-EML.

3.4 Comforting Lemma

Fortunately the following lemma holds.

Lemma 3.3 (Comforting Lemma). Axioms do not contribute to the signature internal environment. Moreover the presence and identity of the trace produced as a result of an axiom elaboration doesn’t influence the elaboration of any of the remaining signature components.

Proof. Rule 74.1:

\frac{B ⊢ axdesc ⇒ γ}{B ⊢ axiom axdesc ⇒ \{\} in Env, γ}

and induction over rules 63–90.

Corollary 3.4. Axioms can affect the signature elaboration only by imposing things and not by non-trivially contributing things.

3.5 The Mature Approach to the EML Rule 65

Basing on these facts we can now formulate a sketch of the algorithm for the implementation of rule 65:

1. strip sigexp of its axioms getting sigexp′,

2. elaborate sigexp′ and obtain principal (N′)S′ and γ′,

3. check that the axioms do not impose anything,

4. elaborate axioms according to rule 74.1, getting traces γ_{1}, ···, γ_{n},

5. if everything was all right, return (N′)S′ and additionally γ′ with γ_{1}, ···, γ_{n} inserted into proper places.

(A hint towards a similar solution was formulated by Stefan Kahrs in [6].)

Theorem 3.5. The above procedure is correct.

Proof. When the check performed in step 4 assures us that the axioms do not impose anything, we know by the Comforting Lemma, that the semantic signature resulting from the elaboration of sigexp is the same as from the elaboration of it’s stripped version. On the other hand, as the traces resulting from the elaboration of the signature components are put together in a “free” way (see rule 81 cited in Section 4.2), simple inserting of γ_{1}, ···, γ_{n} into γ′ is enough to correctly reconstruct the trace for sigexp.

Let us analyze the steps sketched above. The first step, stripping axioms, is a simple syntactic operation. As sigexp′ is bereft of axioms the second step, its elaboration, is as easy as elaboration of any SML signature (apart from trace collection involved, see Section 6). Inserting the traces γ_{1}, ···, γ_{n} into γ′ in the fifth step is a technicality. The problem that remains, is how to implement the third and the fourth steps.

3.6 Validating Axioms

Suppose, we are given a sigexp with an axiom inside. Let sigexp′ be sigexp with an empty specification in place of the axiom. If there is a derivation Der′ of a principal signature for sigexp′, let Der_{e} be its sub-derivation, corresponding to the empty specification. Then let B_{e} be the basis found in Der_{e}.

Theorem 3.6. The axiom do not impose any type sharing or setting of equality attributes in sigexp iff there is a derivation Der_{ax} of the principal trace for the axiom in basis B_{e}.

Proof (⇐). Suppose, there exists Der_{ax}. Then Der′ with Der_{ax} in place o Der_{e} is a perfect skeleton of a principal derivation Der for sigexp. To make a formally correct derivation tree out of this skeleton it’s enough to additionally perform two operations on every ancestor node of Der_{e}. First operation is a proper insertion of the trace resulting from Der_{ax} into the traces of the node. Second is substituting the empty specification sub-phrase of the node by the axiom.

After this, Der is a correct derivation for sigexp and moreover it is the principal one, because Der′ and Der_{ax} are principal. Now notice, that Der has the same resulting semantic signature as Der′ and its trace is a simple extension of the Der′ trace. This means that the axiom do not impose any type sharing or setting of equality attributes in sigexp.

Proof (⇒). If sigexp′ has a principal derivation and the axiom do not impose anything, then surely there is a principal derivation for sigexp. Obviously its sub-derivation corresponding to the axiom is also principal. What remains to be proved is, that the derivation for the axiom starts in the basis B_{e}. By the Comforting Lemma the axiom (which as we know, do not impose things) cannot influence any bases occurring in the principal derivation for sigexp. So the principal derivation for the axiom is performed in the same basis as the derivation Der_{e} — in the basis B_{e}.

The checks that there are principal derivations for axioms in given bases is not much more complicated than the elaboration of axioms in structures. Additionally, as can be seen from the proof, the traces produced in the result are the ones required in the step four from Section 3.5. Now the only remaining difficulty in implementing step three, and so the whole algorithm, is the computation of bases B_{e} for given axioms.

4 Interlude

In fact we already know where to get B_{e} from. It’s one of the components of the trace γ′ resulting from the elaboration of sigexp′ (in the second step, Section 3.5). There are two problems however. First, for simplicity we assumed in Section 2.2.2, that traces are full-blown derivation trees. The truth is, that although one can reconstruct a derivation tree for a phrase using its resulting trace, the task is not much simpler than building the derivation tree from scratch. Second, traces are necessary only for the EML Verification Semantics. If we can find a suitable way for computing B_{e} without traces, there is no need to introduce them for the sake of the Static Semantics, as their implementation is somewhat complicated and troublesome (Section 6).

To see how to compute bases B_{e} without the use of traces we should first go into the details of the signature elaboration in SML (or axiom-less signature elaboration in EML).

4.1 Static Semantics of Signatures

Both the EML and the SML Static Semantics for Modules relies on nondeterminism. While elaborating signatures the identity of their type or structure components is nondeterministically guessed. For example in rule 83 (slightly simplified):

\frac{tyvarseq = α^{(k)}  arity θ = k}{C ⊢ tyvarseq tycon ⇒ \{tycon ↦ (θ, \{\})\}}  (83)

where θ may be chosen to achieve the desired sharing or equation attribute properties. Or in rule 63:

\frac{B ⊢ spec ⇒ E, γ}{B ⊢ sig spec end ⇒ (m, E), m · γ}  (63)

where m may be chosen to satisfy the sharing or enrichment requirements.

4.2 Elaborating Signatures

To get rid of the nondeterminism inherent in the Static Semantics, an algorithm for computing principal signatures is used, resembling the algorithm for inferring principal types by Damas and Milner.

Instead of being correctly guessed at once, the type and structure components of a signature are considered to be fresh, most general. Then in the process of elaborating the signature, a realisation is collected and applied to these components. This “improves” the first cautious approximations, makes them more specific, more precise.

To get a bit of intuition about the algorithm let’s look at rule 81, describing the elaboration of sequential specifications:

\frac{B ⊢ spec_{1} ⇒ E_{1}, γ_{1} B + E_{1} ⊢ spec_{2} ⇒ E_{2}, γ_{2}}{B ⊢ spec_{1} ⟨;⟩ spec_{2} ⇒ E_{1} + E_{2}, γ_{1} · γ_{2}}  (81)

and now look at the corresponding code (simplified) in the EML Kit. The things to note are the realisations (rea1, rea2), their composition (oo) and application to the semantic objects (onB, onE):

fun elab_spec (B: Env.Basis, spec: IG.spec) :
    (Stat.Realisation * Env.Env * OG.spec) =

    case spec of
    ...
    (* Sequential specification *)
    | IG.SEQspec(i, spec1, spec2) =>
        let
            val (rea1, E1, out_spec1) = elab_spec(B, spec1)
            val B' = (rea1 onB B) B_plus_E E1
            val (rea2, E2, out_spec2) = elab_spec(B', spec2)
        in
            (rea2 oo rea1, (rea2 onE E1) E_plus_E E2,
             OG.SEQspec(okConv i, out_spec1, out_spec2))
        end

5 In the Search for the Basis B_{e}

Knowing the basics of the algorithm for elaborating axiom-less signatures, let’s try to guess how to get the basis B_{e} for a given sigexp with an axiom.

5.1 The Modest Basis

Should it be the basis used by the algorithm, when it starts to elaborate the whole sigexp? No, and the following example shows why:

signature S1 =
sig
    type t
    axiom forall (a : t) => true
end

In this basis there is no type t, and so the axiom would be wrongly considered ill-formed.

5.2 The Ignorant Basis

Maybe then we should use the basis, which is collected in the place just before the axiom? Let’s look at the following example:

signature S2 =
sig
    type t
    type u
    axiom forall ( a : t, f : u -> bool) => f a

    sharing type t = u
end

The axiom here doesn’t impose any sharing, because in the principal signature for the sigexp with the axiom removed types t and u are identified. Nevertheless the axiom here won’t elaborate in the basis obtained when the algorithm finishes elaborating first two specifications, because fresh types are assigned to t and u, and no knowledge about the upcoming sharing specification is taken into account.

5.3 The Omniscient Basis

It seems so, that the basis collected at the and of the elaboration of the stripped sigexp would be a good candidate for B_{e}. Indeed the axiom from the last example would elaborate correctly in this basis, because types assigned to t and u are finally identified. Unfortunately, in the following example the axiom which is clearly ill-formed, does elaborate in the basis obtained in the final step of signature elaboration:

signature S3 =
sig
    axiom forall (a : t) => true
    type t
end

5.4 The Observation

A we see, in the basis B_{e} there should be exactly those components collected in the basis from just before the axiom, but their identity should be influenced by the information gathered throughout the whole signature.

Observation 5.1. It turns out that to get basis B_{e} it’s enough to obtain the final realisation rea, by using the standard signature type-checking algorithm on sigexp′, and then apply rea to the basis, taken when the algorithm finished processing the specification just before the axiom.

Corollary 5.2. It is possible to obtain the basis B_{e} without the use of traces.

6 Trace Collection

6.1 Traces

Traces serve to record semantic objects produced during elaboration. The gathered information is then heavily used in the EML Verification Semantics. Traces also play some role in the Static Semantics, although with enough care EML type-checking can be performed without the use of traces (see Section 4).

The Clos operator is used in several places of the Static Semantics (rules 11.1, 11.2, 11.3 and 17) to bound type variables in traces with respect to the given context:

Clos_{C}γ = ∀α^{(k)}.γ, where α^{(k)} = tyvars(γ) \ tyvars C

It is not obvious, that a trace collected at one of the intermediate stages of a phrase elaboration can be closed with respect to context of this stage, because the context nor the trace needn’t be principal yet.

In the Definition of Extended ML [10] Core Trace is defined in the following way:

The presentation of Modules Trace found in [10] is not fully satisfactory, mainly from the implementation point of view (see [4]). In the next versions of EML Definition, Modules Trace will be defined as below, and I’m going to use this presentation for our discussion:

Trace = Tree(Trace_{COR} ⊎ SimTrace ⊎ BoundTrace) BoundTrace = NameSet × Trace SimTrace = StrName ⊎ Rea ⊎ VarEnv ⊎ TyEnv ⊎ Env

[11]:

Trace = Tree(SimTrace ⊎ TraceScheme)

SimTrace = Type ⊎ Env ⊎ (Context × Type) ⊎ (Context × Env) ⊎

(Context × TyName) ⊎ TyEnv ⊎ (VarEnv × TyRea) TraceScheme = ⊎_{k≥0}TraceScheme^{(k)} TraceScheme^{(k)} = TyVar^{k} × Trace

[4]:

Trace = Tree(Trace_{COR} ⊎ SimTrace ⊎ BoundTrace) BoundTrace = NameSet × Trace SimTrace = StrName ⊎ Rea ⊎ VarEnv ⊎ TyEnv ⊎ Env

6.2 Substitutions and trace collection

Looking at the Definition of EML one could expect, that collection of traces is a simple thing; just elaborate the sub-phrases of a given phrase getting some semantic objects and traces, and join the traces adding some of the semantic objects in between, if necessary. The problem is that the elaboration is performed using the algorithm which assigns too general semantic objects to the phrases and then “improves” the first cautious guesses, by applying substitutions. In the result the traces resulting from the sub-phrases elaboration are too general, and cannot be immediately used to obtain correct trace for a given phrase.

It’s clear, that somewhere substitutions should be applied to traces. Where? A natural choice is to apply a substitution to a trace every time the substitution is applied to the semantic object being the result of the elaboration of the sub-phrase. The soundness of this procedure follows from it’s conformance to the principles of the Milner’s algorithm.

6.3 Trace Schemes

Part III

Implementation

7 The Actual Implementation

In this section I’ll try to describe how I actually implemented the algorithm sketched in the Theorem, on the basis of the ML Kit algorithm for the SML signature elaboration.

7.1 Basic Conventions

7.2 Axioms

First I would like to obtain (N′)S′ and the realisation. My implementation elaborates the original sigexp instead of its stripped version taking advantage of the fact, that errors found while elaborating axioms are recorded in the abstract syntax tree and in other ways ignored. The result of this elaboration is some strange trace γ′′, the principal signature (N′′)S′′ for sigexp′, and the corresponding realisation. Now I make the signature equality-principal, and accordingly extend the realisation, getting at last (N′)S′. This is the end of the first pass. The code follows:

fun elab_psigexp (B: Env.Basis, psigexp: IG.psigexp)
    : (Stat.Sig * OG.psigexp) =
  let
    val IG.PRINCIPpsigexp(i, sigexp) = psigexp
    val A = Env.mkAssembly B
(* mikon#1.45 *)
    val NofB = Env.N_of_B B
    val (rea, _, S_first, _) =
        (StrId.backup_state();
        elab_sigexp'(B, sigexp, A, FIRST_PASS))
    val (_, rea1) = Stat.equality_principal(NofB, S_first)
    val (_, _, S, out_sigexp) =
        (StrId.restore_state();
        elab_sigexp'(B, sigexp, A, SECOND_PASS(rea1 oo rea)))
(* end mikon#1.45 *)
  in ... S ... out_sigexp ... end

Now the only things that I need are to check that axioms are valid, get their traces, and repair γ′′ to get the required trace. The easiest way achieve these goals is to elaborate the sigexp for the second time, with an additional parameter being the realisation. When axioms are found they are elaborated in the bases modified by the realisation:

fun elab_spec (B: Env.Basis, spec: IG.spec, A: Env.Assembly, p : pass):
 (Stat.Realisation * Env.Assembly * Env.Env * OG.spec) =
case spec of
...
(* mikon#1.4 and #1.43 *)
 (* Axiom specification *)
| IG.AXIOMspec(i, axdesc) =>
    let
      val (out_axdesc) =
        case p
          of FIRST_PASS => elab_axdesc(B, axdesc)
           | (SECOND_PASS(rea1)) => elab_axdesc(rea1 onB B, axdesc)
    in
      (Stat.Id, Env.emptyA, Env.emptyE, OG.AXIOMspec(okConv i, out_axdesc))
    end
(* end mikon#1.4 and #1.43 *)

7.3 Traces

8 An Anegdote

When I had finished coding this algorithm, for a few days I was sure, I could prove, that the algorithm was correct, but the algorithm kept producing strange and inexplicable results. I was a bit annoyed. Then what made me really angry was the discovering that the culprits were side-effects used in some places in the ML Kit for example to get fresh type names.

I solved the problem in a rather brutal way, as can be seen in the code for the function elab_psigexp above and in the offending module below:

functor Timestamp(): TIMESTAMP =
struct
type stamp = int
val r = ref 0
fun new() = (r := !r + 1; !r)
fun print i = "$" ^Int.string i
(* mikon#1.44 *)
val backup = ref 0
fun backup_state() = backup := !r
fun restore_state() = r := !backup
(* end mikon#1.44 *)

end;

22

References

[1] H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. 2nd edition, North Holland (1984).

[2] L. Birkedal, N. Rothwell, M. Tofte and D. N. Turner. The ML Kit, Version 1. (1993).

[3] L. Damas and R. Milner. Principal type schemes for functional programs. Proc. 9th ACM Symposium on Principles of Programming Languages, pp. 207–212. ACM, New York (1982).

[4] M. Jurdziński, M. Konarski, A. Schubert. The EML Kit, Version 1. Technical Report TR 96-04 (225), Institute of Informatics, Warsaw University (1996).

[5] J. Hannan. Extended natural semantics. Journal of Functional Programming, 3(2), 123–152 (1993).

[6] R. Harper. Introduction to Standard ML. Report ECS-LFCS-86-14, Univ. of Edinburgh (1986).

[7] S. Kahrs. Mistakes and ambiguities in the definition of Standard ML. Report ECS-LFCS-93-257, Univ. of Edinburgh (1993).

[8] S. Kahrs. Mistakes and ambiguities in the definition of Standard ML – Addenda. Univ. of Edinburgh (1995).

[9] S. Kahrs. On the Static Analysis of Extended ML. Univ. of Edinburgh (1994).

[10] S. Kahrs, D. Sannella and A. Tarlecki. The Definition of Extended ML. Report ECS-LFCS-94-300, Univ. of Edinburgh (1994).

[11] S. Kahrs, D. Sannella and A. Tarlecki. The Definition of Extended ML, Version 1.15 + 0.2i.

[12] S. Kahrs and D. Sannella and A. Tarlecki. The semantics of Extended ML: a gentle introduction. Proc. Workshop on Semantics of Specification Languages, Utrecht, 1993. Springer Workshops in Computing, 186–215 (1994).

[13] X. Leroy. Manifest types, modules and separate compilation. In: Proc. 21st ACM Symposium on Principles of Programming Languages, Portland. ACM (1994).

[14] X. Leroy. Polymorphic typing of an algorithmic language. Research report 1778, INRIA (1992).

[15] R. Milner and M. Tofte. Commentary on Standard ML. MIT Press (1991).

[16] R. Milner, M. Tofte and R. Harper. The Definition of Standard ML. MIT Press (1990).

[17] C. Reade. Elements of functional programming. Addison-Wesley (1989).

[18] D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Fundamental Aspects of Computing, to appear.

[19] D. Sannella and A. Tarlecki. Extended ML: past, present and future. Proc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen. Springer LNCS 534, 297–322 (1991).

[20] D. Sannella and M. Wirsing. Specification Languages. In: Algebraic Foundations of Systems Specifications (E. Astesiano, H.-J. Kreowski and B. Krieg-Brückner, editors). Chapman and Hall, to appear.

[21] M. Wirsing. Algebraic specification. In: Handbook of Theoretical Computer Science, Vol. B (J. van Leeuwen, ed.), 675-788. Elsevier and MIT Press (1990).