the sum type constructors it implements. An implementation of this type in Python is naive, and users must ensure that these classes are used correctly. We know that there are possibilities of programming dynamic type verification mechanisms in Python, which simulate strongtyping (similar to that used in OCaml) and ensure that the code is used correctly; however, these techniques lie outside of the scope of this book. The objective of all implementations shown in this book is simply to illustrate and intuitively justify the correct handling of concepts. As we have already done, we choose this approach to implement sum types.
Using Python, we define the following classes to represent the constructors of the set Exp1:
Python class Cstel: def __init__(self,cste): self.cste = cste class Var1: def __init__(self,symb): self.symb = symb class Plusl: def __init__(self,exp1,exp2): self.exp1 = exp1 self.exp2 = exp2 class Bang1: def __init__(self,symb): self.symb = symb
For example, the expression e1 = !x + y defined in example 2.1 is written as:
Python ex_expl = Plusl(Bangl(“x”),Varl(“y”))
Using OCaml, the type of arithmetic expressions is defined directly as:
OCaml type ’a exp1 = Cstel of int | Var1 of ’a | Plusl of ’a expl * ’a expl | Bangl of ’a
Values of this type are thus obtained using either the Cste1 constructor applied to an integer value, in which case they correspond to a constant expression, or using the Var1 constructor applied to a value of type ’a, corresponding to the type used to represent identifiers (the type ’a exp1 is thus polymorphic, as it depends on another type), or by applying the Plus1 constructor to two values of the type ’a expl, or by applying the Bang1 constructor to a value of type ’a. For example, the expression e1 = !x + y is written as:
OCaml let ex_exp1 = Plus1 (Bang1 (“x”), Var1 (“y”)) val ex_exp1 : string exp1
2.2.2. Values
Given a state (Env
Values in V are either relative integers or references. By defining a sum type, these two collections of values can be grouped into a single type.
Python class CInt1: def __init__(self,cst_int): self.cst_int = cst_int class CRef1: def __init__(self,cst_adr): self.cst_adr = cst_adr
Each class possesses a (object) constructor with the same name as the class: the constant k obtained from integer n (or, respectively, from reference r) is thus written as CInt1(n) (respectively, CRef1(r)), and this integer (respectively, reference) can be accessed from (the object) k by writing k.cst_int (respectively k.cst_adr). With OCaml, the type of elements in V is defined directly, as follows:
OCaml type ’a constl = CIntI of int | CRefl of ‘a
A value of this type is obtained either using the constructor CInt1 applied to an integer value or using the constructor CRef1 applied to a value of type ’a corresponding to the type used to represent references.
A type grouping the elements of
Python class VCste1: def __init__(self,cste): self.cste = cste class Erreur1: pass
An element v in VCste1(k), or an object in the class Erreur1 (pass is used here to express the fact that the (object) constructor has no argument). With OCaml, the type of the elements in 𝕧 is defined directly as follows:
OCaml type ’a valeursl = VCstel of ’a constl | Erreur1
2.2.3. Evaluation semantics
There are several formalisms that may be used to describe the evaluation of an expression. These will be introduced later. Let us construct an evaluation function:
The evaluation of the expression e in the environment Env and memory state Mem is denoted as
Table 2.2. Evaluation of the expressions of Exp1
|
|
(k ∈ ℤ) |
|
|
if x ∈ X and x ∈ dom(Env) |
|
|
if x ∈ X and x ∉ dom(Env) |
|
|
|
|
|
|
|
|
|
|
|
|
