On the Static Analysis of Extended ML

Stefan Kahrs^{∗}

Abstract

This is a short note describing differences in static analysis of EML, as defined in [KST94], and SML, as defined in [MTH90] and [MT91]. It is intended for use by people who are building an EML parser/type-checker by modifying an existing SML compiler.

1 Lexical Analysis

The lexical structure of EML and SML is largely the same. There are only two differences.

The first is that EML has no imperative type variables, not even on the lexical level. Thus, the SML identifiers in ImpTyVar (those starting with ' or '' ) are excluded from EML.

The other difference is that EML has additional reserved words: exists, forall, proper, raises, terminates, ?, ==, =/=. Also *) is now reserved, but this is merely a way of avoiding unbalanced comment parentheses which is required informally for SML anyway.

2 Syntax Analysis

The syntax of Extended ML is largely an extension of SML’s syntax. These extensions can be found straightforwardly by comparing the syntax of the “full” languages of SML (in [MTH90], pages 71–73 (core) and pages 12–14 (modules)) and EML (pages 119–124 in [KST94]). I am not going into detail here, just classify the extensions:

• EML has a variety of additional constructs for expressions to have some logical connectives in the Core language, e.g. quantifiers, equality.

• A question mark ? appears at several places in the syntax, for expressions, type bindings, structure bindings, and functor bindings. At some places in the syntax question marks are banned from appearing, this is indicated by a “•”, i.e. exp^{•} is an expression in which no ?-expressions and no ?-type bindings can occur.

• Structures and signatures can both contain axioms which are included as one further alternative to strdec and spec, respectively.

• The syntax is presented with some additional non-terminals (or “syntax classes”, to stick to SML jargon), e.g. there is psigexp for principal signatures. This difference is only a matter of presentation.

Certain parts of SML are not included in EML, these are:

• References and everything that goes with them, i.e. the type constructor ref and all operations on references, the special treatment for references in matching, etc. Most of these do not affect static analysis anyway.

• Streams and everything that goes with them, but this does not affect static analysis, apart from the corresponding changes to the initial basis.

∗The research reported here was supported by SERC grant GR/J 07303.

• Imperative type variables have been removed as well, conceptually and syntactically.

• while expressions are not in EML. Their presence would be rather pointless without assignment and IO, although they formally do not depend on these. For compatibility reasons, while is kept as a reserved word.

• Compared to SML, there are a few syntactic restrictions concerning the presence of signatures. Output signatures for functors are compulsory in EML. Moreover, structure expressions in declarations of the form structure strid = strexp are required to be guarded (see page 17 of [KST94]). Intuitively, “guarded” means that the signature of strexp is clear from the context.

There are also some errors and omissions in the SML syntax we had to fill or fix for EML, see [Kah93]. Largely we have adopted solutions that confirm with existing implementations. For example, for infix patterns in the full language, we adopt the same technique as for infix expressions, i.e. EML has auxiliary syntactic classes infpat and apppat, analogously to infexp and appexp. This is exactly what all existing implementations do anyway. Remark: if an implementation wanted (desperately, I hasten to add) to confirm to the SML definition, the following should syntax-check:

infix ++
datatype tree = ++ of int*int
val z = fn x:int ++ (y:int) => x+y

Regarding the resolution of omissions in the definition of the SML syntax, there was a choice in one point: In [MTH90], the authors forgot to include the syntax of infix function value bindings in the grammar for the full language. This leaves it open whether the components of this construct are atomic patterns or infix patterns. Poly ML and New Jersey ML have different solutions; we chose to require atomic patterns (as New Jersey ML does).

SML has a notion of precedence to overcome syntactic ambiguities present in the BNF grammar. However, the SML definition requires that no program is rejected because of precedence clash. EML maintains this principle. As explained in [Kah93], SML’s notion of precedence is not sufficient to solve all syntactic disambiguities. In EML we have adopted the suggestions of [Kah93] to cope with the unresolved ambiguities, see pages 117, 118. The disambiguation principles derived from this may conflict with the choices made by SML implementations. Here is an example taken from [Kah93] (pages 14, 15):

false andalso if x then x else x orelse true

Roughly, syntactic disambiguation in EML works top-down. Thus, the above expression has a conflict at the top between andalso and orelse and the operator with lower precedence (which is orelse) is taken to be the topmost operator. In other words, the value of the above expression should be true in EML. In Poly ML and New Jersey ML, it is false.

As in Standard ML, identifiers can be value variables, value constructors, or exception constructors. The way to decide which identifier has which status was vague and flawed in the Definition of SML and still (but less) vague and still (but less) flawed in the Commentary on SML, see [Kah93]. In Extended ML, identifier status is treated more rigorously in the semantics for derived forms (Appendix B). This is again largely a formalisation of existing practice. A possible exception might be the following:

exception TARZAN
fun TARZAN _= 1

This is permitted in EML, because fun and rec retain their recursive binding nature on so-called “status environments” (see rules 373 and 387), i.e. they can be used to overwrite constructor status. The above is illegal in Poly ML but legal in New Jersey ML.

3 Type Checking, Core

Type checking for the core is only an extension of existing SML type checking. On one hand, it is an extension as we deal with an extended syntax; on the other, static analysis produces additional results in EML. In particular, the judgement form for elaborating expressions is C ⊢ exp ⇒ τ, U, γ, i.e. U and γ are additional results.

U is nothing else but the familiar set of type variables occurring unguarded in exp (see section 4.6 in [MTH90]), i.e. this result exists in SML as well but was not treated within the formalism of the type system. The only purpose of U is to direct the scoping of explicit type variables, which is the same in SML and EML (modulo language extensions/restrictions). Concerning the syntactic extensions, it should be noted that the EML constructs of equality, exp_{1}^{•} == exp_{2}^{•}, and quantification, forall match^{•} and exists match^{•}, guard variables and thus affect their scope.

A minor detail: in EML exception declarations, applicative type variables are banned syntactically, i.e. from occurring in a type expression ty, while SML bans them only semantically, i.e. from occurring in semantic types τ. The difference only shows up in pathological examples of the following kind:

type 'x dummy = bool
exception A of 'a dummy

This elaborates in SML (Poly ML rejects it illegally), but not in EML: the type variable 'a occurs in the syntactic type of the exception, but not in the semantic type.

Explanation:

We have not allowed applicative type variables in EML because of our explicit treatment of scoping of type variables: since the elaboration of core declarations in EML does not return a set of unguarded type variables, allowing them there would lead to incompatibilities to SML, for example:

     type 'x dummy = bool
     val z = let exception A of 'a dummy
                 val e:'a list = []
             in  1::e
             end

This example does not elaborate in SML, because the exception declaration makes a hole into the scope of the type variable 'a. In EML as it is defined, the example does not elaborate either, but for a different reason, i.e. because the exception declaration is rejected already. Without the syntactic side condition in rule 31.1, the above would elaborate in EML, because declarations are considered to have no unguarded type variables in EML. Of course, we could have made the corresponding adjustment of the judgement form in EML (returning unguarded type variables for declarations), but this seemed to be a bit out of place, considering that this only makes a difference for these pathological examples. End of explanation.

Corresponding to scoping, type variables are also abstracted at quantifiers (and equality expressions), i.e. type schemes are introduced here. However, this abstraction has little effect on static analysis, because quantified variables can never be used polymorphically: outside the quantifier they are simply out of scope and inside they have to be used monomorphically — the latter is similar to the treatment of polymorphic recursion in SML/EML, i.e. a recursively defined identifier cannot be used polymorphically within its own definition. The polymorphism at the quantifiers only shows up in verification, e.g. specialising forall match just means to apply the (polymorphic) function fn match to an argument.

The other new result of static elaboration in EML is the trace γ — it is essentially the parse tree of exp with type information added. Within elaboration it has only a very limited impact (see next section); its main purpose is to export type information for use in verification. In an SML implementation it would typically already exist in some form, e.g. in the form of type attributes in the abstract syntax. For verification purposes, this may not be enough: traces occur in the semantic values of signatures in the verification semantics. These traces can be modified by realisations (as any other component of a semantic signature) when a structure is matched against a signature. In practice, this means to make a copy of the trace each time a structure/signature matching has to be verified (or rather “verificated”, to use EML terminology).

Concerning the correction of soundness violations in the core semantics we have adopted the solutions suggested in [Kah93] and its update. This is noticable insofar as it is more restrictive than the existing practice for SML. For example,

val x = let datatype t = C in C end;

...is legal in SML and also in most (if not all) of its implementations. The implementations avoid the soundness problem described in [Kah93] by using the state (i.e. a global counter) for creating new type names, ignoring the fact that the static semantics of SML does not have a concept of state.

To conform to the EML standard, an implementation could use the same method as most SML implementations do but needs an additional check that no local type names escape from let-expressions. To be specific: if type names are just numbers generated from a global counter, then type-checking let dec in exp end means to (i) make a copy of the counter; (ii) type-check dec and then exp; (iii) check that no type-name in the type τ of exp is “larger” than the copy we made in step i.

4 Type Checking, Modules

The major difference between SML and EML type checking is in the treatment of structure binding: EML structure bindings are opaque, SML structure bindings are transparent, see rules 62.1–62.3 in EML and rule 62 in SML. A corresponding difference applies to functor declarations. Intuitively, the user can only see what is in the output signature of a functor/structure. Here is an example:

structure S: sig type t; val x:t end =
     struct type t = int
            val  x = 41
     end;
val y = S.x+1

This type-checks in SML but not in EML, see rule 62.1. Only structure bindings without explicit signature are transparent (rule 62.3).

There are a couple of syntactic restrictions accomodating this principle: functors in EML always come equipped with an output signature (in SML these are optional), and similarly structures always have an (at least implicit) signature (see page 17 in [KST94], second bullet). The latter means that the situation in rule 62.3 only occurs in particular cases. These restrictions are merely for methodological purposes (though the omission of an output signature for functors would require a special treatment in the verification semantics, but never mind), they do not affect the static analysis as such — except, of course, that the restrictions have to be checked; there is also a useful impact on principality, see below.

Principality of declarations is imposed in EML at two places: (i) when core declarations are regarded as structure declarations (as in SML, rule 57), and (ii) for axiom declarations, see rule 57.1. In both cases it is the place where the Core language is linked up with the Modules.

Imposing principality is something that should (by nature) go unnoticed, but there are a couple of features that make fewer programs elaborate when principality is imposed: one is open in signatures, the other is overload resolution; SML has a third with its imperative type variables. Actually, the open feature does not hurt in EML because of the mentioned syntactic restrictions on structure declarations. Since no existing implementation (to my knowledge, which includes MLKit) implements the Standard anyway, I suggest not to lose sleep over this matter.

Intermission

Although in a strict sense not an adaptation problem between SML and EML, principality and the way it can be observed is a rather subtle point in the static analysis of SML and EML, and therefore I thought it to be worthwhile to explain these subtleties.

Here is an example in SML that only elaborates if principality is delayed further (say up to topdec) than the definition requires.

     structure S = struct val x=[] end;
     structure T:sig open S end = struct val x=[1] end;

In EML, the example is banned, because a signature is required in the declaration of S. The special restrictions on EML structure declarations prevent open from wrecking the beauty of principality — this achievement is solely due to overload resolution:

     structure S: sig val f: int -> int end =
         struct fun f x = x+x end;

The above declaration does not elaborate in EML, because overloading is resolved too late, i.e. after imposing principality. The technical explanation goes as follows: the declaration fun f x = x+x is parsed as a strdec, such that we have to find the principal type for f for this declaration alone. The principal type of f would be ∀ num.num → num, but this type cannot be derived, as num cannot be specialised to num: when we instantiate the type of + we have to commit to either int or real. End of intermission.

Thus, the only feature in EML which one can use to observe that principality has been imposed is overload resolution. Overloading is formalised in EML via a very modest specialisation of Haskell-style overloading [HJW92], using one distinguished type variable num — for details, see section 4.5 of [KST94] or the section on overloading in [Kah93]. The point is that overloading has to be resolved to provide a principal elaboration, since the type variable num is excluded from abstraction, i.e. there is no user-defined overloading.

Principality is imposed on the so-called traces, not just the resulting environments. A trace includes all the intermediate elaboration results, its general purpose is to export information about the static analysis to the verification, but within the static analysis its only impact is to require overload resolution even for dead code:

val z = let fun f x = x+x in 4 end

This does not elaborate in EML, because the trace of the declaration of z contains the type of f. Since f is not part of the resulting environment there is moreover no way to resolve overloading by surrounding declarations.

In an implementation, one should allow num to be specialised with num (or some num’), but then one needs a final check that all num have been unified with either real or int. This may involve a traversal of the attributed syntax tree (= trace), or (simpler) there could be a special table containing all generated num variables; each time principality is imposed all variables in this table should have been instantiated.

Principality of specifications differs in one respect from SML. EML signatures contain axioms which are essentially expressions of type bool. We did not want the requirement of well-typedness of these expressions to affect sharing of types and equality attributes of specified types. Recall that specified types in SML (and EML) are “guessed” and the successful elaboration of signatures requires that the right type names are guessed. An implementation would obviously perform some sort of unification here.

The problem is: what can force this unification to take place? In the semantics of SML and EML this is only implicit, apart from some noisy and ugly gnome (I call him Rumpelstiltskin, the semantics calls him “equality-principality”) who is used to prevent datatype descriptions from implicitly enforcing such unifications.

A similar problem exists for axiom descriptions. An axiom description is essentially just an expression of type bool. Thus, for a signature to elaborate, all its axiom descriptions have to type-check. This elaboration cannot equate type names or set equality attributes.

Explanation:

If we defined this straightforwardly then axiom descriptions could force the sharing of types and the setting of equality attributes. Example:

     signature S = sig
         type s
         val x:s
         axiom x=x
     end;
     signature T = sig
         type t; type u
         axiom forall x:t => exists y:u => x==y
     end;

In both cases, the axiom descriptions affect the signature elaboration: the first axiom requires s to be an equality type, the second requires the types t and u to share. We did not want this kind of interaction between core and modules; the signatures S and T are banned in EML. The main reason is that we want to be able to regard axioms as comments w.r.t. SML and obtain an executable SML program by commenting out all the axioms. Thus we have to avoid the use of axioms to specify type sharing etc. End of explanation

This is achieved as follows: rule 65 of EML imposes principality twice, once for the signature without axioms, once for the full signature.

For an implementation, the idea is to ignore the axioms for type-checking in a first run, obtain all necessary sharing/equality information from the signature, and then type-check the axioms without allowing any further sharing or setting of equality attributes. Thus, the expressions in axioms can be type-checked in the ordinary way, there is no need to empower their elaboration to impose the unification of type names.

5 Initial Basis

The definition of Standard ML does not clearly state in which environment elaboration, evaluation, etc. start. It does define a so-called “initial basis”, but this is not used in its program semantics.

This problem is also discussed in [Kah93]. In EML, the initial basis is indeed used to start everything, see rule 343. The result is that an EML system could not treat a library as part of the structure environment since the initial structure environment is fixed (and empty). Of course, there would be no harm in extending the initial structure environment in this way apart from the conflict with the “official” initial basis.

References

[HJW92] P. Hudak, S. Peyton Jones, and P. Wadler. Report on the Programming Language Haskell, a Non-strict, Purely Functional Language. Technical report, University of Glasgow, 1992. (also in SIGPLAN Notices 27(5), May 1992).

[Kah93] Stefan Kahrs. Mistakes and ambiguities in the definition of Standard ML. Technical Report ECS-LFCS-93-257, University of Edinburgh, 1993. An update listing further

errors is available in ftp://ftp.dcs.ed.ac.uk/pub/smk/SML/errors-new.ps.Z.

[KST94] Stefan Kahrs, Don Sannella, and Andrzej Tarlecki. The definition of Extended ML. Technical Report ECS-LFCS-94-300, University of Edinburgh, 1994.

[MT91] Robin Milner and Mads Tofte. Commentary on Standard ML. MIT Press, 1991.

[MTH90] Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, 1990.