2 of 59

Overview: Modules That Declare Types

In the next module language, OPAQUE-TYPES, we allow interfaces to declare types as well.

module m1

interface

[ opaque t

zero : t

succ : (t -> t)

pred : (t -> t)

is-zero : (t -> bool)

]

body

…

Point1: This interface declares a type t, and some operations zero, succ, pred, and is-zero that operate on values of that type.

3 of 59

Overview: Modules That Declare Types

In the next module language, OPAQUE-TYPES, we allow interfaces to declare types as well.

module m1

interface

[ opaque t

zero : t

succ : (t -> t)

pred : (t -> t)

is-zero : (t -> bool)

]

body

…

Point2: Here t is declared to be an opaque type, meaning that code outside the module boundary does not know how values of this type are represented.

All the outside code knows is that it can manipulate values of type from m1 take t with the procedures from m1 take zero, from m1 take succ, etc.

Thus from m1 take t behaves like a primitive type such as int or bool.

4 of 59

Overview: Modules That Declare Types

In the next module language, OPAQUE-TYPES, we will introduce two kinds of type declarations: transparent and opaque. Both are necessary for a good module system.

5 of 59

Overview

Examples: Transparent types as abbreviation

initial-point : (int -> pairof int * int)

increment-x : (pairof int * int -> pairof int * int)

[Alices-points]

Bob and Charlie complains about this. They don’t want to have to write pairof int * int over and over again.

6 of 59

Overview

Examples: Transparent types as abbreviation

module Alices-points

interface

[ transparent point = pairof int * int

initial-point : (int -> point)

increment-x : (point -> point)

get-x : (point -> int)

… ]

body

[ type point = pairof int * int

… ]

Alice therefore rewrites her interface to use transparent type declarations. This simplifies her task, since she has less writing to do, and

It makes her collaborators’ tasks simpler, because in their implementations they can write abbreviated definitions.

[ transparent point = from Alice-points take point

foo = proc (p1 : point)

proc (p2 : point) … ]

7 of 59

Overview

Examples: Opaque types to enforce the boundary of abstraction

- Assume the points in Alice’s project happen to represent points on a metal track with a fixed geometry, so the x- and y-coordinates are not independent.

( 가정: 트랙의 모양이 이미 정해져 있어, 그 모양에 따라 x-좌표와 y-좌표가 결정)

- Alice’s implementation of increment-x carefully updates the y-coordinate to match the change in the x-coordinate.

8 of 59

Overview

Examples: Opaque types to enforce the boundary of abstraction

- Assume the points in Alice’s project happen to represent points on a metal track with a fixed geometry, so the x- and y-coordinates are not independent.

( 가정: 트랙의 모양이 이미 정해져 있어, 그 모양에 따라 x-좌표와 y-좌표가 결정)

- But Bob doesn’t know this, and so he writes his own procedure

without changing the x-coordinate correspondingly. Alice’s code no longer works correctly.

increment-y = proc ( p : point ) (p.x, -(p.y, -1))

9 of 59

Overview

Examples: Opaque types to enforce the boundary of abstraction

- Alice can solve this problem by making point an opaque data type.

module Alices-points

interface

[ opaque point

initial-point : (int -> point)

increment-x : (point -> point)

get-x : (point -> int)

… ]

body

[ type point = pairof int * int

… ]

Now Bob can create new points and can manipulate points, but he can no longer manipulate points using any procedure other than the ones in Alice’s interface. (cf. increment-y)

10 of 59

Overview: Transparent types

Also called concrete type declarations or type abbreviations

This program has type (int -> bool).

11 of 59

Overview: Transparent types

The declaration transparent t = int in the interface binds t to the type int in the rest of the interface, so we can write z : t.

More importantly, it also binds from m1 take t to int in the rest of the program. We call this a qualified type.

The scope of a declaration is the rest of the interface and the rest of the program after the module definition.

12 of 59

Overview: Transparent types

The definition type t = int in the body binds t to the type int in the rest of the module body, so we could write s = proc (x : t) … .

The scope of a definition is the rest of the body.

13 of 59

Overview: Opaque types

Also called abstract types

This program has ill-type in -(x,0) because the main program does not know that values of types from m1 take t are actually values of type int.

Not OK

14 of 59

Overview: Opaque types

The declaration opaque t in the interface declares t to be the name of a new opaque type. An opaque type behaves like a new primitive type, such as int or bool.

The named type t is bound to this opaque type in the rest of the interface, and the qualified type, from m1 take t, is bound to the same opaque type in the rest of the program.

15 of 59

Overview: Opaque types

All the rest of the program knows about this type from m1 take t is that

- from m1 take z is bound to a value of that type, and that

- from m1 take s and from m1 take is-z? are bound to procedures that can manipulate values of that type.

This is the abstraction boundary. The type checker guarantees that the evaluation of an expression has type from m1 take t is safe, so that the value of the expression has been constructed only by these operations.

16 of 59

Overview: Opaque types

The definition type t = int in the body defines t to be a name for int inside the module body, but this information is hidden from the rest of the program, because the rest of the program gets its bindings from the module interface.

17 of 59

Overview: Opaque types

Also called abstract types

This gives a mechanism to enforce the distinction between the users of a data type and its implementation.

Now this program has type(from m1 take t -> bool).

By enforcing this abstraction boundary, the type checker guarantees that no program manipulates the values provided by the interface except through the procedures that the interface provides.

18 of 59

Overview: Opaque types

19 of 59

Overview: Opaque types

Example 8.8

There is no way the program can figure out that from colors take color is actually int, or that from colors take green is actually 1.

20 of 59

Overview: Opaque types

Example 8.9

This program has type from ints1 take t. It has value 10, but we can manipulate this value only through the procedure that are exported from ints1.

This module represents the integer k by the expressed value 5 * k.

from ints1 take succ

(from ints1 take succ

(fromt ints1 take zero))

21 of 59

Overview: Opaque types

Example 8.10

This program has type from ints2 take t. It has value -6.

22 of 59

Overview: Opaque types

Example 8.11

This program converts a value from the module back to a value of type int by a procedure to-int.

It has type int and has value 2.

The type of to-int is

( from ints1 take t -> int )

23 of 59

Overview: Opaque types

Example 8.12

Here is the same technique used with the implementation of arithmetic ints2.

It also has type int and value 2.

Later, we will show how to abstract over these two examples (8.11 and 8.12).

24 of 59

Overview: Opaque types

Example 8.13

We construct a module to encapsulate a data type of booleans. The booleans are represented as integers, but that fact is hidden from the rest of the program.

It has type from mybool take t, and has value 13.

25 of 59

OPAQUE-TYPES: Syntax (구문)

The grammar for OPAQUE-TYPES extends the grammar for SIMPLE-MODULES. (OPAQUE-TYPES 문법은 SIMPLE-MODULES 문법을 확장).

- We introduce transparent and opaque type declarations and qualified type references.

- Two new kinds of types: named types (like t) and qualified types (like from m1 take t)

Type -> identifier

Type -> from identifier take identifier

26 of 59

OPAQUE-TYPES: Syntax (구문)

- Two new kinds of declarations, for opaque and transparent types

- A new kind of definition: a type definition, which will be used to define both opaque and transparent types

Declaration -> opaque identifier

Declaration -> transparent identifier = Type

type identifier = Type

28 of 59

OPAQUE-TYPES: Abstract syntax tree (추상 구문 트리)

The AST datatype for transparent and opaque declarations

data Declaration =

ValDecl Identifier Type

| OpaqueTypeDecl Identifier

| TransparentTypeDecl Identifier Type

29 of 59

OPAQUE-TYPES: Abstract syntax tree (추상 구문 트리)

The AST datatype for type definitions

data Definition =

ValDefn Identifier Exp

| TypeDefn Identifier Type

x = 123

y = list (1,2,3)

z = bool

type t = int

type point = pairof int * int

30 of 59

OPAQUE-TYPES: Abstract syntax tree (추상 구문 트리)

The AST datatype for type names and qualified types

data Type =

TyInt

| TyBool

| TyFun Type Type

| TyName Identifier

| TyQualified Identifier Identifier

31 of 59

OPAQUE-TYPES: Abstract syntax tree (추상 구문 트리)

Parsing(파싱): Turn a program text(a sequence of characters) into an abstract syntax tree (프로그램 텍스트, 문자 나열을 분석해서 추상 구문 트리를 만들기)

Parsing(파싱)

32 of 59

OPAQUE-TYPES: Abstract syntax tree (추상 구문 트리)

Examples

33 of 59

OPAQUE-TYPES: Semantics (by Interpreter)

The expressed values, ExpVal, are the possible values of expressions (식을 계산해서 나올 수 있는 가능한 값, ExpVal)

- ExpVal = Int + Bool + Proc

- DenVal = ExpVal

Note: This is the same as that for CHECKED and SIMPLE-MODULES. (CHECKED언어나 SIMPLE-MODULES에서와 동일)

34 of 59

OPAQUE-TYPES: Semantics (by Interpreter)

The interpreter doesn’t look at types or declarations, so the only changes to the interpreter is to make it ignore type definitions!

- A modification of the SIMPLE-MODULE interpreter:

Just ignore the type definition.

35 of 59

OPAQUE-TYPES: Semantics (by Interpreter)

Example

36 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The changes to the checker are more substantial, since all the manipulations involving types must be extended to handle the new types.

equalType (TyName “t”) TyInt ?

equalType (TyQualified “m1” “t”)) TyInt ?

“t” should be expanded.

We should lookup “m1”, and “t” should be expanded.

37 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The changes to the checker are more substantial, since all the manipulations involving types must be extended to handle the new types. (Cont.)

equalType (TyName “t”) TyInt ?

equalType (TyQualified “m1” “t”) TyInt ?

“t” should be expanded.

We should not lookup “m1”, nor should “t” be expanded.

38 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

First, we introduce a systematic way of handling opaque and transparent types. An opaque type behaves like a primitive type while transparent types behave exactly like their definitions.

=> So, every type is equivalent to one that is given by the following grammar:

- Type ::= int | bool | from m take t | ( Type -> Type )

We call a type of this form an expanded type.

39 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

We next extend type environments to handle new types. Our type environments will bind each named type or qualified type to an expanded type.

data TyEnv =

Empty_tyenv

| Extend_tyenv Identifier Type TyEnv

| Extend_tyenv_with_module Identifier Interface TyEnv

| Extend_tyenv_with_type Identifier Type TyEnv

Invariant: type will always be made to be an expanded type.

type name

var name

module name

40 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

We next extend type environments to handle new types. Our type environments will bind each named type or qualified type to an expanded type.

We must be sure to call expand_type whenever we extend the type environment in order to maintain this invariant.

41 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

Where should we call expand_type to maintain this invariant in extending a type environment.

- In the checker: type_of

e.g., extend_tyenv x ty tenv => extend_tyenv x (expand_type ty tenv) tenv

- When processing a list of definitions: defns_to_decls

- When adding a module to the type environment: add_module_defns_to_tyenv

Later we will see how types and interfaces are expanded.

42 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The structure of the checker:

- In type_of_program, a type environment is built for the body expression, using add_module_defns_to_tyenv.

- The procedure computes an actual interface by interface_of, and compares it with the declared/expected interface by sub_iface.

- If good, the procedure adds a new type environment with the expanded interface of the declared one computed by expand_iface.

43 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The procedure add_module_defns_to_tyenv:

m has (interface) type iface’ expanded from iface.

44 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The procedure interface_of uses defns_to_decls:

ty is already expanded through type_of exp tyenv.

ty should be expanded.

TypeDefn var ty is turned into TransparentTypeDecl var ty since in the body all type bindings are transparent.

45 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The procedure expand_iface:

46 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The procedure expand_decls:

OpaqueTypeDecl x turns to TransparentTypeDecl x expanded_type !!

TransparentTypeDecl x ty turns to TransparentTypeDecl x expanded_type !!

Let* scoping: each declaration in a set of declarations is in scope in all the following declarations.

e.g., expand_decls … new_itnernal_env

47 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The procedure expand_decls : Let* scoping: each declaration in a set of declarations is in scope in all the following declarations.

module m1

interface

[ opaque t

transparent u = int

transparent uu = (t -> u)

f : uu

… ]

body

[ … ]

module m1

interface

[ transparent t = from m1 take t

transparent u = int

transparent uu = (from m1 take t -> int)

f : (from m1 take t -> int)

… ]

body

[ … ]

expand_decls : [Declaration] ==> [Declaration]

48 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The procedure expand_decls : Let* scoping: each declaration in a set of declarations is in scope in all the following declarations.

module m1

interface

[ opaque t

transparent u = int

transparent uu = (t -> u)

f : uu

… ]

body

[ … ]

module m1

interface

[ transparent t = from m1 take t

transparent u = int

transparent uu = (from m1 take t -> int)

f : (from m1 take t -> int)

… ]

body

[ … ]

expand_decls : [Declaration] ==> [Declaration]

In (A), the type environment should bind

t to from m1 take t,

u to int,

uu to (from m1 take t -> int).

(We call it the internal type environment.)

NB. this procedure creates only transparent declarations, since its purpose is to create a data structure in which qualified types can be looked up.

49 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The procedure sub_iface:

50 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The procedure sub_decls to handle the two new kinds of declarations.

- We must deal with the scoping relations inside a set of declarations.

- extend_tyenv_with_decl will do the job.

[ transparent t = int

x : bool

y : t ]

[ y : int ]

We need to know that t refers to type int when we get to the declaration of y.

51 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The procedure sub_decls:

extend_tyenv_with_decl translates a declaration decl1 to an appropriate extension of the type environment.

52 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The procedure sub_decl:

- How do we compare declarations?

- NB. equalExpandedType

They are both value declarations, and their types match.

They are both opaque type declarations.

They are both transparent type declarations, and their definitions match.

decl1 is a transparent type declaration, and decl2 is an opaque type declaration.

transparent t=int <: opaque t (O)

opaque t <: transparent t=int (X)

53 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The procedure extend_tyenv_with_decl:

This creates a fresh module name!

It maintains the invariant that all types in the type environment are expanded.

54 of 59

OPAQUE-TYPES: Semantics (by Type Checker)

The procedure equalExpandedType:

- E.g.,

[ transparent t = int x : bool y : t ] <: [ y : int ]

55 of 59

OPAQUE-TYPES: Projects

Tokens.hs	Declare tokens (구문의 최소 단위 선언)
Lexer.hs	Turn a text (char seq.) into a token sequences( 텍스트를 토큰으로 분리)
Expr.hs	Declare abstract syntax trees (구문 트리 선언)
Env.hs	Declare the environment types with modules (모듈을 포함한 환경 선언)
Parser.hs	Turn the token seq. into an abstract syntrax tree (토큰들을 구문 트리로)
TyEnv.hs	Declare environments with module types (모듈 타입/인터페이스를 포함한 환경 타입 선언),
TypeCheck.hs	Type checker (타입 검사)
Interp.hs	An interpreter (해석기)
EitherState.hs	The combination of Either and State (Either와 State 혼합 타입 유틸리티)

1 of 59

2 of 59

3 of 59

4 of 59

5 of 59

6 of 59

7 of 59

8 of 59

9 of 59

10 of 59

11 of 59

12 of 59

13 of 59

14 of 59

15 of 59

16 of 59

17 of 59

18 of 59

19 of 59

20 of 59

21 of 59

22 of 59

23 of 59

24 of 59

25 of 59

26 of 59

27 of 59

28 of 59

29 of 59

30 of 59

31 of 59

32 of 59

33 of 59

34 of 59

35 of 59

36 of 59

37 of 59

38 of 59

39 of 59

40 of 59

41 of 59

42 of 59

43 of 59

44 of 59

45 of 59

46 of 59

47 of 59

48 of 59

49 of 59

50 of 59

51 of 59

52 of 59

53 of 59

54 of 59

55 of 59

56 of 59

57 of 59

58 of 59

59 of 59