On Axiom Type-Checking and Trace Collection in Extended ML a draft

Mikołaj Konarski ^{∗}

                    mikon@mimuw.edu.pl

February 18, 1997

Introduction

Standard ML (SML) [10] is a functional programming language, equipped with a 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

Extended ML (EML) [7] is a framework for the formal development of programs in SML. As a language EML is an extension of (a large subset of) SML. The 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

The EML Kit [3] is an implementation of the Extended ML programming language, developed by Marcin Jurdziński, Mikołaj Konarski, Sławomir Leszczyński and Aleksy Schubert. The EML Kit parses, type-checks and evaluates EML programs.

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

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.

1 Preliminaries

EML is described thoroughly in the Definition of Extended ML [7]. To dwell into the intricacies of the EML type-checking we should first introduce some of fundamental concepts of the EML Static Semantics.

1.1 Semantic objects

In the EML Static Semantics for the Core Language there appear syntactic phrases like expressions, declarations or type expressions and corresponding semantic objects like types, environments, type functions. Analogously in the EML Static Semantics for Modules there are syntactic phrases like structures or signatures and semantic objects like semantic structures, which are pairs of structure names and environments:

S or (m, E) ∈ Str = StrName × Env

or semantic signatures, which are just semantic structures with some structure and type names bound:

Σ or (N)S ∈ Sig = NameSet × Str

1.2 Judgments

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 γ”.

1.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 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 5. Elaborating EML signatures with axioms is much more complicated.

2.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 object 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.

2.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 2.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 [9], 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 2.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.

2.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.

2.4 Comforting Lemma

Fortunately the following lemma holds.

Lemma 2.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 2.4. Axioms can affect the signature elaboration only by imposing things and not by non-trivially contributing things.

2.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 2.5. The above procedure is correct.

Proof. When the check performed in step four 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 3.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 5). 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.

2.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 2.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 2.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.

3 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 2.5). There are two problems however. First, for simplicity we assumed in Section 1.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 that 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 5).

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).

3.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.

3.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

4 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.

4.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 incorrect.

4.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.

4.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 incorrect, does elaborate in the basis obtained in the final step of signature elaboration:

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

4.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 4.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 4.2. It is possible to obtain the basis B_{e} without the use of traces.

!!!!!!!!! THE REST IS NOT QUITE FINISHED, YET : ) !!!!!!!!!!!

5 Trace Collection

5.1 Traces

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

Trace = Tree(SimTrace ⊎ TraceScheme)

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

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

TraceScheme^{(k)} = TyVar^{k} × Trace

The presentation of Modules Trace found in [7] is not fully satisfactory, mainly from the implementation point of view (see [3]). 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

Traces serve to record semantic objects produces 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 3).

When adding trace collection to the existing EML type-checking algorithm there are two serious problems to solve.

5.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 the 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.

Another possibility is to refrain from correcting the trace during the elaboration, but instead apply the final substitution to the trace obtained at the end of the process. To prove that it works a lemma is needed, similar to the one proved in Section 2.4. The proof of the lemma is an induction over all the rules of the Static Semantics of EML.

5.3 Trace Schemes

The second problem is also related to the substitutions and stems from the fact, that one of the possible forms of the Core Trace is the TraceScheme.

The Clos operator is used in several places of the Static Semantics to bound type variables in traces with respect to the given context:

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

Unfortunately, a trace collected at one of the intermediate stages of a phrase elaboration cannot be closed with respect to context of this stage, because the context needn’t be principal yet. We had to design an involved algorithm to correctly organize the ongoing collection, updating and closure of traces during elaboration.

6 The Actual Implementation

6.1 Blyp

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.

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 *)

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;

References

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

[2] 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).

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

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

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

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

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

[8] 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).

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

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