Medinfo 2013

Akimichi Tatsukawa August 19, 2013

Contents
1 Introduction 2 Untyped Lambda Calculus[10, p.51] 2.1 Terms[10, p.51] . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Simply Typed Lambda Calculus [10, p.99] 3.1 Terms and Types . . . . . . . . . . . . . . . . . . . 3.2 Typing judgments[4, p.10] . . . . . . . . . . . . . . 3.3 Typing rules[8, p.239] . . . . . . . . . . . . . . . . . 3.4 Type System[4, p.11] . . . . . . . . . . . . . . . . . 3.4.1 Type Soundness[4, p.12] . . . . . . . . . . . 3.5 Data Structures . . . . . . . . . . . . . . . . . . . . 3.5.1 Tuple type[10, p.126][4, p.16][2, p.132] . . . 3.5.2 Record type[10, p.129][4, p.18] . . . . . . . . 3.5.3 Variant type[10, p.132][4, p.18] . . . . . . . 3.5.4 Unit Type[4, p.15] . . . . . . . . . . . . . . 3.5.5 Reference type[4, p.19] . . . . . . . . . . . . 3.5.6 Recursive type[4, p.20][10, p.267] . . . . . . 3.5.7 List type[4, p.21][10, p.146,p.197][2, p.150][6, 2 3 3 3 4 4 5 5 5 6 7 7 7 7 11 11 11 11

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . p.42]

. . . . . . . . . . . . .

. . . . . . . . . . . . .

. . . . . . . . . . . . .

4 Subtyping[4, p.26] 11 4.1 Basic type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.2 Record type[2, p.72] . . . . . . . . . . . . . . . . . . . . . . . 15 4.3 Variant type . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 1

4.4 4.5 4.6 4.7

Function type . . . . . . . . . . . . . . Reference Type[4, p.20] . . . . . . . . . Mutable Record Type[2, p.80] . . . . . Object Type[2, p.83][5, p.10] . . . . . . 4.7.1 The recursive record model[3, ] 4.7.2 The Existential Model[5, p.13] . 4.7.3 Object Calculus[5, p.15] . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

. . . . . . .

16 17 17 17 17 18 18

5 Second-order Type System[1, p.7][4, p.20][2, p.141][6, p.31][11, p.185][7, p.116][9, p.852] 18 A Sample proofs 20 A.1 Natural deductions-style derivations . . . . . . . . . . . . . . . 20 A.2 Fitch-style deduction[6, p.12] . . . . . . . . . . . . . . . . . . . 20 B Featherweight openEHR 22 B.1 A simplyed syntax . . . . . . . . . . . . . . . . . . . . . . . . 22 B.2 A formal semantics . . . . . . . . . . . . . . . . . . . . . . . . 22 Glossary
Abstract This arcticle is a supplementary document for my presentation at Medinfo 2013. I am going to explain a brief introduction to typed lambda calculus. A word for notice: this document is far from complete for a description of typed lambda calculus.

24

Introduction

The lambda calculus is a formal system in which all computations are reduced to the basic operations of function denition and application. Its signicance arises from the fact that it can be viewed not only as a simple programming language in which computations can be described, but also as a mathematical object from which rigorous statements can be proved.

2
2.1

Untyped Lambda Calculus[10, p.51]

The set of lambda terms is dened by the following abstract syntax(Fig.1). Term variables will be denoted by x,y,z.... Terms will be denoted by M,N,P in our convention. (Term) M ::= x | x.M | M M V ariable Abstraction Application (1) (2) (3)

Figure 1: Syntax of Untyped Lambda-Calculus

2.2

Evaluation

Lambda terms are evaluated via reduction rules(Fig.2). (x.M )N M [N/x] x.(M x) M

( -reduction) ( -reduction)

(4) (5)

Figure 2: Reduction rules for Untyped Lambda-Calculus The rule (4) means that an expression can be reduced by replacing some subexpression of the form (x.M )N by substituting the argument N for the bound variable x in the body M. The subexpressions which can be reduced, are called a redex. While the equation(4) denotes a single step reduction, multi-step evaluations are denoted as . A closed term without redexes is said to be in normal form[2, p.132]. Every value is in normal form, whereas not all the normal forms are values. Such a term, which is a normal form but not a value, is said to be stuck.

Simply Typed Lambda Calculus [10, p.99]

In untyped lambda calculus, there are stuck terms which has no more rule to reduce and they are not values either,say x(x.x). They correspond to meaningless or erroneous programs. The main goal of typed lambda calculus is to avoid such erroneous terms by introducing a type system. In this section, we introduce First-order Type System which is a type system without type parameterization and type abstraction.

3.1

Terms and Types

The syntax of the terms and types in a simply typed lambda calculus is shown in Fig.6. The main dierence from untyped lambda calculus is the abstraction(Eq.(8)), to which a type annotation has attached. x : is an type statements and read as a term x has type , which means that x obviously evaluates to a value of the appropriate form without doing any evaluation of x. For example, 0 : Int means that 0 is a value of Int.
 

Terms: M ::= c |x | x: .M |M M Types: BasicT ype ::= Bool | Int . . . T ype ::= | 1 2 Basic type F unction type (10) (11) (12) Constant V ariable abstraction Application (6) (7) (8) (9)

Figure 3: Simply Typed Lambda-Calculus

Even though purely untyped lambda calculus dont have any types except function type, it is convenient to adopt basic types now so that later exten4

sions are easier. Basic types are indicated as BasicT ype, such as Boolean, Integer, etc.

3.2

Typing judgments[4, p.10]

A formal assertion relating entities of terms, types, and environments are called judgment. Among them, a formal assertion on types are called typing judgment. A typical typing judgment has the form in Eq.(13) and read M has type with respect to . Any given judgment is regarded as valid in a given type system. M : (13)

in Eq.(13) is a type environment. It is a set of assumptions about the types of the free variables in M . When we write {x : }, this means the type environment is extended by adding a new binding {x : }, i.e. {x : }. The empty environment is denoted by . However, we omit and use M : as shorthand for M : .

3.3

Typing rules[8, p.239]

Typing rules are implications between statements, and dened by a set of axioms and inference rules assiging types to terms. The inference rules assert the validity of certain judgments on the basis of other judgments that are already valid. Each inference rule is written as a number of premise judgments above the horizontal line, along with a single conclusion judgment below the line. The conclusion is a valid judgment according to the given type system. The typing rules without any premise are axioms. For example, the axiom (14) simply states that a variable x has whatever type it is declared to have unless it doent already appear in dom(). The typing rules for this simple typed lambda calculus are presented in Fig.4.

3.4

Type System[4, p.11]

The whole set of typing rules constituted a type system. In a given type system, we can construct a proof combining typing rules of that system. 5

{x : }

x dom() x: BasicT ype {x : } M : x : .M : M : N : (M N ) : Figure 4: Typing rules

(type var) (type const) (type arrow) (abstraction) (application)

(14) (15) (16) (17) (18)

Any proof has a shape of tree with leaves at the top and a root at the bottom, where each judgment is obtained from the ones immediately above it by applying some rules of the system. The trees are called derivation trees(type derivation).An example of type derivation is presented in Fig.5. A term M in the bottom line is said to be well-typed if there is some type such that M : can be derived from the inference rules or axioms.
 

{x : Bool} x : Bool x : Bool.x : Bool Bool true : Bool (x : Bool)true : Bool Figure 5: An example of a derivation tree

3.4.1

Type Soundness[4, p.12]

It should be noted that in a sensible type system a valid type judgment corresponds to a correct semantic behavior without errors. This is called Soundness and stated as follows in more formal way. 6

if

M : is valid, then

M holds.

(19)

Preservation of types: If M : and M M , then M : . The subject reduction theorem[2, p.131] insists that evaluation of an expression results in a value with the same type as the original expression. Progress: If M : , then either M is a value or there is some M such that M M . The combination of the progress and preservation theorem guarantees that well-typed terms never get stuck. This is one of the main advantages of typed lambda calculus over untyped one.

3.5

Data Structures

We introduce some structured data structures into our typed lambda calculus. 3.5.1 Tuple type[10, p.126][4, p.16][2, p.132]

A tuple type (M1 , M2 , . . . , Mn ) is the cartesian product of values. A component can be extracted with the projection operator(Eq.(22)). 3.5.2 Record type[10, p.129][4, p.18]

The Record Type is a product type with labels, and it has a value-level operation for extracting components by name(Fig.7). This data structure is important because it gives us a way of grouping of data items, therefore it can be a basis for encoding objects in Object-Oriented Languages[5]. 3.5.3 Variant type[10, p.132][4, p.18]

The Variant Type is a named disjoint unions of types: it express choices between alternatives.

Term: M ::= . . . | (M1 , M2 , . . . , Mn ) | M.i Type: ::= . . . | 1 2 . . . n Typing rules: M : 1 N : 1 (M, N ) : 1 2 M : 1 2 . . . n M.i : i Figure 6: Tuple type
 

(20) Tuple projection (21) (22) (23) product type (24)

(25) (26)

Types: ::= . . . | {l1 : , . . . ln : } Term: M ::= . . . | {l1 = M, . . . , ln = M } | M.li Typing rules: Mi : i (i 1..n) (32) {l1 : M1 , . . . , ln : Mn } : {l1 : 1 , . . . , ln : n } {l1 : M1 , . . . , ln : Mn } (33) M.li : i Figure 7: Record type
 

(27) (28) (29) (30) (P rojection) (31)

Types: ::= . . . | <l1 : , . . . ln : > Term: M ::= . . . | < l1 = M, . . . , ln = M > | M.li Typing rules: Mi : i (i 1..n) < l1 : M1 , . . . , ln : Mn >:< l1 : 1 , . . . , ln : n > (38) < l1 : M1 , . . . , ln : Mn > (39) M.li : i Figure 8: Variant type
 

(34) (35) (36) (37)

10

3.5.4

Unit Type[4, p.15]

A unit type is a singleton type which has only one instance unit. This is often used as a lter for uninteresting arguments and results.
 

Typing rules: U nit unit : U nit (40) (41)

Figure 9: Unit type

3.5.5

Reference type[4, p.19]

In order to represent updatable variables, we have to introduce reference type. References are mutable cells holding values, whose operations are allocation, dereferencing, and assignment. If M has type Ref ( ), then it denotes a location which can hold a value of type . Common mutable types,such as Array, can be derived from Ref type. Mutable Record type, for example, can be modeled as record types which has elds of Ref types as in Fig.(21). 3.5.6 Recursive type[4, p.20][10, p.267]

We introduce a recursion operator , and the type environments are extended to include type variables X. 3.5.7 List type[4, p.21][10, p.146,p.197][2, p.150][6, p.42]

Subtyping[4, p.26]

Subtyping captures the intuition of inclusion between types: an element of a type can be considered as an element of its supertypes. We add a new judgment 1 <: 2 meaning that 1 is a subtype of 2 . 11

Types: ::= . . . | Ref ( ) Typing rules: Ref ( ) M : ref M : Ref ( ) M : Ref ( ) deref M : M : Ref ( ) N : M := N : U nit (type ref) (44) (val ref) (45) (val deref) (46) (val assign) (47) Figure 10: Reference type
 

(42) (43)

12

Types: T ype ::= X | X. Terms: M ::= X.M |M Typing rules: {X } M : X.M : X. M : X. (M ) : [/X ] M : [X. /X ] f oldX. M : X. M : X. unf oldX. M : [X. /X ] Figure 11: Recursive type
 

(type variable) (48) (universal quantier) (49) (type abstraction) (50) (type application) (51)

(52) (53) (54) (55)

13

Types: ::= . . . | List Term: M ::= . . . | nil[T ] | cons[T ]M M Typing rules: nil[T ] : List[T ] t1 : T t2 : List T cons[T ]t1 t2 : List T (61) (62) (58) (59) (60) (56) (57)

Figure 12: List type

M : <: (subsumption rule) M : M : (reexive) <: 1 <: 2 2 <: 3 (transitive) 1 <: 3 (top type) (sub top)

(63) (64) (65) (66) (67)

T op <: T op Figure 13: Subtyping rules

14

The central theorem of subtyping is the subsumption rule(Eq.(63)) stating that if a term M has type , and is a subtype of , then the term M also has type . A single subtyping rule has to be added for each type constructor, taking care of the soundness of the subtyping rule in conjunction with subsumption.

4.1

Basic type

We can introduce subtyping rules for any Basic types as long as they are compatible with Eq.(63).

4.2


Record type[2, p.72]

i (1 i n) (width subtyping) {l1 : , . . . lm : , . . . , ln : } <: {l1 : , . . . , lm : } (68) i <: i (1 i n) {l1 : 1 , . . . ln : n , . . . } <: {l1 : 1 , . . . , ln : n } (depth subtyping) (69) Figure 14: Record subtyping rules

Figure 15: Record subtyping schema

15

i (m i n) (width subtyping) (l1 : 1 , . . . lm : m ) <: (l1 : 1 , . . . , lm : m , . . . ln : n ) (70) i <: i (1 i n) (l1 : 1 , . . . , ln : n ) <: (l1 : 1 , . . . , ln : n ) (depth subtyping) (71) Figure 16: Variant subtyping rules

4.3 4.4

Variant type Function type

As for subtyping rules for function the inclusion is inverted as covariant for function arguments, while it goes in the same direction as covariant for function results.
 

<: <: <:

(sub arrow)

(72)

Figure 17: Function Subtyping

Figure 18: Function Subtyping

16

4.5

Reference Type[4, p.20]

Reference types do not have any subtyping rule: Ref (A) <: Ref (B ) holds only if A=B (in which case Ref (A) <: Ref (B ) follows from reexivity). This strict rule is necessary because references can be both read and written, and hence behave both covariantly and contravariantly.
 

A <: B B <: A Ref (A) <: Ref (B )

(73)

Figure 19: Reference Subtyping

Figure 20: Reference subtyping

4.6

Mutable Record Type[2, p.80]

In order to model a Mutable Record Type, whose elds can be updated, each of the elds represents a reference as in Eq.(75). This means that no changes to the types of existing elds is allowed.

4.7
4.7.1

Object Type[2, p.83][5, p.10]

Objects can be represented as records whose elds are either immutable data or lambda term as method. As a result, the subtyping rule for Object Type is identical with its Record Type. There are other way of encoding for Object Type, such as the Existential Model and an axiomatic approach. 17

M : Ref ( ) N : M := N : U nit Mi : Ref (i ) (i 1..n) {li : Mi } : {li : Ref (i )}

(74)

(75)

Figure 21: Mutable Record Type

i (1 m n) and (i 1..n) {|l1 : 1 , . . . lm : m , . . . , ln : n |} <: {|l1 : 1 , . . . , lm : m |} Figure 22: Object subtyping rules

(76)

4.7.2 4.7.3

The Existential Model[5, p.13] Object Calculus[5, p.15]

Second-order Type System[1, p.7][4, p.20][2, p.141][6, p.31][11, p.185][7, p.116][9, p.852]

Second-order type systems extend rst-order systems with type parameters, which is written as X.M indicating that a term M is parameterized with respect to a type variable X. The type parameteric functions are instantiated by type instantiation according to the Eq.(84).

[X := ] = X [X := ] = (1 2 )[X := ] = (1 [X := ] 2 [X := ]) (Y.M )[X := ] = Y.(M [X := ]) 18

(85) (86) (87) (88)

Types: ::= | . Terms: M ::= .M |M Typing rules: {X } {X } X {X } X. {X } M : X.M : X. M : X. M : [/X ]. (81) (82) (83) type instantiation (84) Figure 23: second-order type system
 

type variable (77) universal quantication (78) type abstraction (79) type instantiation (80)

19

A
A.1


Sample proofs
Natural deductions-style derivations


A <: A N :A N :A x : A.M : A B (x : A.M )(N ) : B Figure 24: Proof 1

 

 

A <: A N :A

x : A .M : A B (x : A .M )(N ) : B

N :A

Figure 25: Proof 2

{y : T } x : T (y : T.x) : T T {x : T } x : T {x : T } (y : T.x) : T T x : T.(y : T.x) : T T T T.(x : T.(y : T.x)) : T.T T T Figure 26: Proof 3
 

A.2

Fitch-style deduction[6, p.12]

In a tch-style, a hypothesis is introduced by raising a ag, that is, the x : in Fig.30. The hypothesis is discharged by withdrawing the ag. 20

A <: A N :A

N :A

(subsumption)

{x : A} M : B x : A.M : A B (x : A.M )(N ) : B

(abstraction)

Figure 27: Proof 4

<: <: (7) Ref ( ) <: Ref ( ) {l1 : Ref ( )} <: {l1 : Ref ( )} Figure 28: Proof 5
 

(3)

 

Arc <: Arc [Arc ] <: [Arc] N : [Arc]

N : [Arc ] x : Arc xs : [Arc].M : [Arc] [Arc] (x : Arc xs : [Arc].M ) N : [Arc]

Figure 29: Proof 6

1. x : 2. . . . 3. . . . 4. M : 5. x : .M :

abs, 1,4 Figure 30: abs-rule 21

1. . . . 2. . . . 3. M : 4. . . . 5. . . . 6. N : 7. . . . 8. M N :

app, 3,6 Figure 31: app-rule

B
B.1

Featherweight openEHR
A simplyed syntax

Archetype[OBSERVATION] BloodPressure specialize Base { data : HISTORY protocol : ITEM_TREE }

Syntax: AT ::= Archetype A specialize A {f : A} K ::= A(f = f ) archetype declaration (89) constructor (90)

B.2

A formal semantics
types */ Character Boolean Interger 22

/* Primitive BasicType := | |

Term: t::= x | t.f | new C (t) Values: v ::= new A(v ) Type: ::= RM T ype | AOM T ype T ype ::= | 1 2 (95) (96) (97) instance (94) variable eld instantiation (91) (92) (93)

Subtyping: C <: C C <: D D <: E C <: E Archetype C specialize D C <: D Typing rules: i (1 i m n) Archetype{l1 : , . . . , ln : } <: Archetype{l1 : , . . . , lm : } (101) i <: i (1 i n) Archetype{l1 : 1 , . . . ln : n } <: Archetype{l1 : 1 , . . . , ln : n } (102) (98) (99) (100)

23

| | | | |

Real Double ISO8601_DATE ISO8601_TIME ... */ List[T] Set[T] Array[T] Hash[U,T] Interval[T]

/* Complex types AggregateType := | | | | DV := | | | |

DV_BOOLEAN DV_TEXT DV_CODED_TEXT DV_QUANTITY DV_IDENTIFIER

Glossary
judgment A formal assertion relating entities such as terms, types, and environments. 5 normal form An expression to which none of the reduction rules can be applied. 3 type derivation A tree of judgments obtained by applying the rules of a type system.. 6 type environment A sequence of variables and their types. 5 type system A collection of typing rules for a typed programming language. Same as static type system.. 5 typing rule typing rules are implications between judgments, whole set of which constitutes a type system. typing rules assert the validity of 24

certain judgments on the basis of other judgments that are already known to be valid.. 5 valid judgment A judgment obtained from a derivation in a given type system. 5

References
[1] Erik Barendsen. Introduction to Type Theory. http://www.cs.ru.nl/ erikb/onderwijs/sl2/materiaal/tt-sl2.pdf, 2005. [2] Kim B. Bruce. Foundations of Object-Oriented Languages. MIT press, 2002. [3] William R. Cook Walter L. Hill Peter S. Canning. Inheritance Is Not Subtyping. Technical report, Hewlett-Packard Laboratories, 1990. [4] Luca Cardelli. Type Systems. In Handbook of Computer Science and Engineering, chapter 97. CRC Press, 2004. [5] Kathleen Fisher and John C. Mitchell. The Development of Type Systems for Object-Oriented Languages. Theory and Practice of Object Systems, Vol. 1, pp. 189220, 1996. [6] Herman Geuvers. Introduction to Type Theory. Technical report, Radboud University Nijmegen and Technical University Eindhoven,The Netherlands, 2008. [7] Chris Hankin. An Introduction to Lambda Calculi for Computer Scientists. No. 2 in Texts in Computing. Kings College, 1 edition, 2004. [8] John C. Mitchell. Foundations for Programming Languages. MIT Press, 1 edition, 2000. [9] Atsushi Ohori. A Polymorphic Record Calculus and Its Compilation. ACM Transactions on Programming Languages and Systems, Vol. 17, No. 6, pp. 844895, 1995. [10] Benjamin C. Pierce. Types and Programming Languages. MIT press, 1 edition, 2002. 25

[11] . . , No. 9. , 1 , 1997.

26