Previous Up Next

Chapter 2  The core of OCaml

Many features of OCaml (and of other dialects of ML) can actually be formalized on top of core ML, either by selecting a particular choice of primitives, by encoding, or by a small extension.

2.1  Data types and pattern matching

The OCaml language contains primitive datatypes such as integers, floats, strings, arrays, etc. and operations over them. New datatypes can also be defined using a combinations of named records or variants and later be explored using pattern matching — a powerful mechanism that combines several projections and case analysis in a single construction.

2.1.1  Examples in OCaml

For instance, the type of play cards can be defined as follows:

     
type card = Card of regular | Joker and regular = { suit : card_suit; name : card_name; } and card_suit = Heart | Club | Spade | Diamond and card_name = Ace | King | Queen | Jack | Simple of int;;

This declaration actually defines four different data types. The type card of cards is a variant type with two cases. Joker is a special card. Other cards are of the form Card v where v is an element of the type regular. In turn regular is the type of records with two fields suit and name of respective types card_suit and card_name, which are themselves variant types.

Cards can be created directly, using the variant tags and labels as constructors:

     
let club_jack = Card { name = Jack; suit = Club; };;
     
val club_jack : card = Card {suit=Club; name=Jack}

Of course, cards can also be created via functions:

      
     
let card n s = Card {name = n; suit = s} let king s = card King s;;
     
val card : name -> suit -> card = <fun> val king : suit -> card = <fun>

Functions can be used to shorten notations, but also as a means of enforcing invariants.

The language OCaml, like all dialects of ML, also offers a convenient mechanism to explore and de-structure values of data-types by pattern matching, also known as case analysis. For instance, we could define the value of a card as follows:

     
let value c = match c with | Joker -> 0 | Card {name = Ace} -> 14 | Card {name = King} -> 13 | Card {name = Queen} -> 12 | Card {name = Jack} -> 11 | Card {name = Simple k} -> k;;

The function value explores the shape of the card given as argument, by doing case analysis on the outermost constructors, and whenever necessary, pursuing the analysis on the inner values of the data-structure. Cases are explored in a top-down fashion: when a branch fails, the analysis resumes with the next possible branch. However, the analysis stops as soon as the branch is successful; then, its right hand side is evaluated and returned as result.

Exercise 13 ((**) Matching Cards)   We say that a set of cards is compatible if it does not contain two regular cards of different values. The goal is to find hands with four compatible cards. Write a function find_compatible that given a hand (given as an unordered list of cards) returns a list of solutions. Each solution should be a compatible set of cards (represented as an unordered list of cards) of size greater or equal to four, and two different solutions should be incompatible.
Answer

Data types may also be parametric, that is, some of their constructors may take arguments of arbitrary types. In this case, the type of these arguments must be shown as an argument to the type (symbol) of the data-structure. For instance, OCaml pre-defines the option type as follows:

type 'a option = Some of 'a | None

The option type can be used to get inject values v of type 'a into Some(v) of type 'a option with an extra value None. (For historical reason, the type argument 'a is postfix in 'a option.)

2.1.2  Formalization of superficial pattern matching

Superficial pattern matching (ie. testing only the top constructor) can easily be formalized in core ML by the declaration of new type constructors, new constructors, and new constants. For the sake of simplicity, we assume that all datatype definitions are given beforehand. That is, we parameterize the language by a set of type definitions. We also consider the case of a single datatype definition, but the generalization to several definitions is easy.

Let us consider the following definition, prior to any expression:

type  g(α) = C1g of  τi  ∣ … Cng of  τn

where free variables of τi are all taken among α. (We use the standard prefix notation in the formalization, as opposed to OCaml postfix notation.)

This amounts to introducing a new type symbol gf of arity given by the length of α, n unary constructors C1g, …Cng, and a primitive fg of arity n+1 with the following δ-rule:

fg (Ckg  v)  v1  … vk  … vn   vk  v     (δg)

The typing environment must also be extended with the following type assumptions:

Cig: ∀ α.  τig(α)
fg: ∀ α, β.  g (α) → (τ1 → β) → … (τn → β) → β

Finally, it is convenient to add the syntactic sugar

match a  with  C1g (x) ⇒ a1 … ∣ Cng (x) ⇒ an 

for

fg a  (λ xa1) … (λ xan)
Exercise 14 ((***) Type soundness for data-types)   Check that the hypotheses 1 and 2 are valid.
Exercise 15 ((**) Data-type definitions)   What happens if a free variable of τi is not one of the α's? And conversely, if one of the α's does not appear in any of the τi's?
Answer
Exercise 16 ((*) Booleans as datatype definitions)   Check that the booleans are a particular case of datatypes.
Answer
Exercise 17 ((***) Pairs as datatype definitions)   Check that pairs are a particular case of a generalization of datatypes.
Answer

2.1.3  Recursive datatype definitions

Note that, since we can assume that the type symbol g is given first, then the types τi may refer to g. This allows, recursive types definitions such as the natural numbers in unary basis (analogous to the definition of list in OCaml!):

type  IN = Zero ∣ Succ  of  IN

OCaml imposes a restriction, however, that if a datatype definition of g(α) is recursive, then all occurrences of g should appear with exactly the same parameters α. This restriction preserves the decidability of the equivalence of two type definitions. That is, the problem “Are two given datatype definitions defining isomorphic structures?” would not be decidable anymore, if the restriction was relaxed. However, this question is not so meaningful, since datatype definitions are generative, and types (of datatypes definitions) are always compared by name. Other dialects of ML do not impose this restriction. However, the gain is not significant as long as the language does not allow polymorphic recursion, since it will not be possible to write interesting function manipulating datatypes that would not follow this restriction.

As illustrated by the following exercise, the fix-point combinator, and more generally the whole lambda-calculus, can be encoded using variant datatypes. Note that this is not surprising, since the fix point can be implemented by a δ-rule, and variant datatypes have been encoded with special forms of δ-rules.

Note that the encoding uses negative recursion, that is, a recursive occurrence on the left of an arrow type. It could be shown that restricting datatypes to positive recursion would preserve termination (of course, in ML without any other form of recursion).

Exercise 18 ((**) Recursion with datatypes)   The first goal is to encode lambda-calculus. Noting that the only forms of values in the lambda calculus are functions, and that a function take a value to eventually a value, use a datatype value to define two inverse functions fold and unfold of respective types:
     
val fold : (value -> value) -> value = <fun> val unfold : value -> value -> value = <fun>
Answer
Propose a formal encoding [[·]] of lambda-calculus into ML plus the two functions fold and unfold so that for an expression of the encode of any expression of the lambda calculus are well-typed terms.
Answer
Finally, check that [[fix ]] is well-typed.
Answer

2.1.4  Type abbreviations

OCaml also allows type abbreviations declared as type g(α) = τ. These are conceptually quite different from datatypes: note that τ is not preceded by a constructor here, and that multiple cases are not allowed. Moreover, a data type definition type g(α) = Cg τ would define a new type symbol g incompatible with all others. On the opposite, the type abbreviation type g(α) = τ defines a new type symbol g that is compatible with the top type symbol of τ since g(τ') should be interchangeable with τ anywhere.

In fact, the simplest, formalization of abbreviations is to expand them in a preliminary phase. As long as recursive abbreviations are not allowed, this allows to replace all abbreviations by types without any abbreviations. However, this view of abbreviation raises several problem. As we have just mentioned, it does not work if abbreviations can be defined recursively. Furthermore, compact types may become very large after expansions. Take for example an abbreviation window that stands for a product type describing several components of windows: title, body, etc. that are themselves abbreviations for larger types.

Thus, we need another more direct presentation of abbreviations. Fortunately, our treatment of unifications with unificands is well-adapted to abbreviations: Formally, defining an abbreviation amounts to introducing a new symbol h together with an axiom h (α) = τ. (Note that this is an axiom and not a multi-equation here.) Unification can be parameterized by a set of abbreviation definitions {h (αh) = τhhA} Abbreviations are then expanded during unification, but only if they would otherwise produce a clash with another symbol. This is obtained by adding the following rewriting rule for any abbreviation h:

Abbrev   if gh
α = h (α) = g (τ) = e
α = τh [αh ← α]  = g (τ) = e

Note that sharing is kept all the way, which is represented by variable α in both the premise and the conclusion: before expansions, several parts of the type may use the same abbreviation represented by α, and all of these nodes will see the expansions simultaneously.

The rule Abbrev can be improved, so as to keep the abbreviation even after expansion:

Abbrev'   if gh
α = h (α) = g (τ) = e
∃ α'.  ( α = h (α) = e ∧ α' = τh [αh ← α] = g (τ)  )

The abbreviation can be recursive, in the sense that h may appear in τh but, as for data-types, with the tuple of arguments α as the one of its definition. The the occurrence of τh in the conclusion of rule Abbrev' must be replaced by τh [g(α) ← α].

Exercise 19 ((*) Mutually recursive definitions of abbreviations)   Explain how to model recursive definitions of type abbreviations type h1(α) = τ1 and h2(α2) = τ2 in terms of several single but recursive definitions of abbreviations.
Answer

See also Section 3.2.1 for use of abbreviations with object types.

2.1.5  Record types

Record type definitions can be formalized in a very similar way to variant type definitions. The definition

type  g(α) =  {f1g : τ1;  … f2g : τn}

amounts to the introduction of a new type symbol g of arity given by the length of α, one n-ary constructor Cg and n unary primitives fig with the following δ-rules:

fig (Cg  v1  … vi  … vn  vi     (δg)

As for variant types, we require that all free variables of τi be taken among α. The typing assumptions for these constructors and constant are:

Cg: ∀ α.  τ1 → … τnα g
fig: ∀ αg(α) → τi

The syntactic sugar is to write a.fig and { f1g = a1; … fng = an} instead of fig a and Cg a1an.

2.2  Mutable storage and side effects

The language we have described so far is purely functional. That is, several evaluations of the same expression will always produce the same answer. This prevents, for instance, the implementation of a counter whose interface is a single function next : unit -> int that increments the counter and returns its new value. Repeated invocation of this function should return a sequence of consecutive integers —a different answer each time.

Indeed, the counter needs to memorize its state in some particular location, with read/write accesses, but before all, some information must be shared between two calls to next. The solution is to use mutable storage and interact with the store by so-called side effects.

In OCaml, the counter could be defined as follows:

     
let new_count = let r = ref 0 in let next () = r := !r+1; !r in next;;

Another, maybe more concrete, example of mutable storage is a bank account. In OCaml, record fields can be declared mutable, so that new values can be assigned to them later. Hence, a bank account could be a two-field record, its number, and its balance, where the balance is mutable.

     
type account = { number : int; mutable balance : float } let retrieve account requested = let s = min account.balance requested in account.balance <- account.balance -. s; s;;

In fact, in OCaml, references are not primitive: they are special cases of mutable records. For instance, one could define:

     
type 'a ref = { mutable content : 'a } let ref x = { content = x } let deref r = r.content let assign r x = r.content <- x; x

2.2.1  Formalization of the store

We choose to model single-field store cells, ie. references. Multiple-field records with mutable fields can be modeled in a similar way, but the notations become heavier.

Certainly, the store cannot be modeled by just using δ-rules. There should necessarily be another mechanism to produce some side effects so that repeated computations of the same expression may return different values.

The solution is to model the store, rather intuitively. For that purpose, we introduce a denumerable collection of store locations lL. We also extend the syntax of programs with store locations and with constructions for manipulating the store:

a ::= … ∣ l ∣ ref a ∣ deref a ∣ assign a  a'

Following the intuition, the store is modeled as a global partial mapping s from store locations to values. Small-step reduction should have access to the store and be able to change its content. We model this by transforming pairs a/s composed of an expression and a store rather than by transforming expressions alone.

Store locations are values.

v ::= … ∣ l

The semantics of programs that do not manipulate the store is simply lifted to leave the store unchanged:

a / s  a' / s  if  a  a

Primitives operating on the store behaves as follows:

 ref v / s l / s, lvldom (s)
 deref l/ s s(l) / sldom (s)
 assign l v / s v / s, lvldom (s)

Hence, we must count store location among values: Additionally, we lift the context rule to value-store pairs:

E [a] / s  E [a'] /s  if  a/s  a' /s 
Example 3   Here is a simple example of reduction:
  let x = ref 1 in assign x (1 + deref x) / ∅
 let x = l in assign x (1 + deref x) / l ↦ 1
 assign l (1 + deref l) / l ↦ 1
 assign l (1 + 1) / l ↦ 1
 assign l (2) / l ↦ 1
 2 / l ↦ 2
Remark 5   Note that, we have not modeled garbage collection: new locations created during reduction by the Ref rule will remain in the store forever.

An attempt to model garbage collection of unreachable locations is to use an additional rule.

a / s  a / (s ∖ l)      l∉ a

However, this does not work for several reasons.

Firstly, the location l may still be accessible, indirectly: starting from the expression a one may reach a location l' whose value s(l') may still refer to l. Changing the condition to la, (sl) would solve this problem but raise another one: cycles in s will never be collected, even if not reachable from a. So, the condition should be that of the form “l is not accessible from a using store s”. Writing, this condition formally, is the beginning of a specification of garbage collection...

Secondly, it would not be correct to apply this rule locally, to a subterm, and then lift the reduction to the whole expression by an application of the context rule. There are two solutions to this last problem: one is to define a notion of toplevel reduction to prevent local applications of garbage collection; The other one is to complicate the treatment of store so that locations can be treated locally (see [77] for more details).

In order to type programs with locations, we must extend typing environment with assumptions for the type of locations:

A ::= … ∣ Al : τ

Remark that store locations are not allowed to be polymorphic (see the discussion below). Hence the typing rule for using locations is simply

Loc
l : τ ∈ A
A ⊢ l : τ

Operations on the store can be typed as the application of constants with the following type schemes in the initial environment A0:

 ref _ :∀ α.  α → ref α 
 deref _:∀ α.  ref α → α 
 assign _ _:∀ α.  ref α → α → α 

(Giving specific typing rules Ref, Deref, and Assign would unnecessarily duplicate rule App into each of them)

2.2.2  Type soundness

We first define store typing judgments: we write Aa/s : τ if there exists a store extension A' of A (ie. outside of domain of A) such that A' ⊢ a : τ and A' ⊢ s(l) : A'(l) for all ldom (A'). We then redefine ≤ to be the inclusion of store typings.

(a / s ≤ a' / s') ⇔∀ (A, τ) (A ⊢ a / s : τ ⇒ A ⊢ a' / s' : τ)
Theorem 5 (Subject reduction)   Store-reduction preserves store-typings.
Theorem 6 (Progress)   If A0a/s : τ, then either a is a value, or a/s can be further reduced.

2.2.3  Store and polymorphism

Note that store locations cannot be polymorphic. Furthermore, so as to preserve subject reduction, expressions such as ref v should not be polymorphic either, since ref v reduces to l where l is a new location of the same type as the type of v. The simplest solution to enforce this restriction is to restrict let x = a in a' to the case where a is a value v (other cases can still be seen as syntactic sugar for (λ x. a') a.) Since ref a is not a value —it is an application— it then cannot be polymorphic. Replacing a by a value v does not make any difference, since ref  is not a constructor but a primitive. Of course, this solution is not optimal, ie. there are safe cases that are rejected. All other solutions that have been explored end up to be too complicated, and also restrictive. This solution, known as “value-only polymorphism” is unambiguously the best compromise between simplicity and expressiveness.

To show how subject reduction could fail with polymorphic references, consider the following counter-example.

     
let id = ref (fun x -> x) in (id := succ; !id true);;

If "id" had a polymorphic type ∀ α.  τ, it would be possible to assign to id a function of the less general type, eg. the type int -> int of succ, and then to read the reference with another incompatible less general type bool -> bool; however, the new content of id, which is the function succ, does not have type bool -> bool.

Another solution would be to ensure that values assigned to id have a type scheme at least as general as the type of the location. However, ML cannot force expressions to have polymorphic types.

Exercise 20 ((**) Recursion with references)   Show that the fix point combinator fix can be defined using references alone (ie. using without recursive bindings, recursive types etc.).
Answer

2.2.4  Multiple-field mutable records

In OCaml references cells are just a particular case of records with mutable fields. To model those, one should introduce locations with several fields as well. The does not raise problem in principle but makes the notations significantly heavier.

2.3  Exceptions

Exceptions are another imperative construct. As for references, the semantics of exceptions cannot be given only by introducing new primitives and δ-rules.

We extend the syntax of core ML with:

a ::= … ∣ try a  with  x ⇒ a ∣   raise  a

We extend the evaluation contexts, so as to allow evaluation of exceptions and exception handlers.

E :: … ∣ try E  with  x ⇒ a ∣ raise  E

Finally, we add the following redex rules:

 try v with xa v(Try)
 try E ' [raise v] with xa let x = v in a(Raise)

with the side condition for the Raise rule that the evaluation context E' does not contain any node of the form (try _ with _ ⇒ _). More precisely, such evaluation contexts can be defined by the grammar:

E' ::= [·] ∣ E'  a ∣ v  E' ∣ raise  E'

Informally, the Raise rule says that if the evaluation of a raises an exception with a value v, then the evaluation should continue at the first enclosing handler by applying the right hand-side of the handler value v. Conversely, is the evaluation of a returns a value, then the Try rule simply removes the handler.

The typechecking of exceptions raises similar problems to the typechecking of references: if an exception could be assigned a polymorphic type σ, then it could be raised with an instance τ1 of σ and handled with the asumption that it has type τ2 —another instance of σ. This could lead to a type error if τ1 and τ2 are incompatible. To avoid this situation, we assume given a particular closed type τ0 to be taken for the type of exceptions. The typing rules are:

Raise
A ⊢ a : τ0
A ⊢ raise  a : α
        
Try
A ⊢ a1 : τ            Ax : τ0 ⊢ a2 : τ
A ⊢ try a1  with  x ⇒ a2 : τ
Exercise 21 ((**) Type soundness of exceptions)   Show the correctness of this extension.

Exercise 22 ((**) Recursion with exceptions)   Can the fix-point combinator be defined with exceptions?
Answer

Further reading

We have only formalized a few of the ingredients of a real language. Moreover, we abstracted over many details. For instance, we assumed given the full program, so that type declaration could be moved ahead of all expressions.

Despite many superficial differences, Standard ML is actually very close to OCaml. Standard ML has also been formalized, but in much more details [51, 50]. This is a rather different task: the lower level and finer grain exposition, which is mandatory for a specification document, may unfortunately obscure the principles and the underlying simplicity behind ML.

Among many extensions that have been proposed to ML, a few of them would have deserved more attention, because there are expressive, yet simple to formalize, and in essence very close to ML.

Records as datatype definitions have the inconvenience that they must always be declared prior to their use. Worse, they do not allow to define a function that could access some particular field uniformly in any record containing at least this field. This problem, known as polymorphic record access, has been proposed several solutions [65, 57, 33, 37], all of which relying more or less directly on the powerful idea of row variables [73]. Some of these solutions simultaneously allow to extend records on a given field uniformly, ie. regardless of the other fields. This operation, known as polymorphic record extension, is quite expressive. However, extensible records cannot be typed as easily or compiled as efficiently as simple records.

Dually, variant allows building values of an open sum type by tagging with labels without any prior definition of all possible cases. Actually, OCaml was recently extended with such variants [23]

Datatypes can also be used to embed existential or universal types into ML [41, 64, 53, 24].


Previous Up Next