Lecture 11

​

OCaml Modules

Programming Languages

UW CSE 341 - Winter 2022

Modules

For larger programs, one “top-level” sequence of bindings is poor

• A binding can use all earlier (non-shadowed) bindings

So ML has structures to define modules

​

​

• Inside a module, can use earlier bindings as usual
• Can have any kind of binding (let, type, exception, ...)
• Outside a module, refer to earlier modules’ bindings via ModuleName.bindingName
• Like List.fold_left, etc. now can define your own modules

module MyModule = struct bindings end

​

Example

module MyMathLib = struct

let rec fact x =

if x = 0

then 1

else x * fact (x - 1)

let half_pi = Float.pi /. 2.0

let doubler x = x *. 2

end

​

Implicit modules via files

OCaml also has a built-in convenience:

​

• A file foo.ml has an implicit

module Foo = struct … end

“around it”

​

• So different files do not shadow, but need to access bindings from other files with Foo.bar syntax

Optional: Open

​

Can use open ModuleName to get “direct” access to a module’s bindings

​

• Never necessary; just a convenience; often bad style
• Often better to create local val-bindings for just the bindings you use a lot, e.g., let map = List.map
• But doesn’t work for patterns
• And open can be useful, e.g., for testing code

Namespace management

So far, this is just namespace management

​

Giving a hierarchy to names to avoid shadowing

• Yes, can have modules inside modules
• Allows different modules to reuse names, e.g., map
• Very important, but not very interesting

​

Module Types (aka Signatures)

• A signature is a type for a module
• What bindings does it have and what are their types
• Can define a signature and ascribe it to modules – example:

module type MATHLIB = sig

val fact : int -> int

val half_pi : float

val doubler : int -> int

end

module MyMathLib : MATHLIB = struct

let rec fact x = ...

let half_pi = Float.pi /. 2.0

let doubler x = x *. 2

end

​

In general

• Signatures

​

​

​

• Can include variables, types, and exceptions defined in module
• Ascribing a signature to a module

​

​

​

• Module will not type-check unless it matches the signature, meaning it has all the bindings at the right types

​

module type SIGNAME = sig

types-for-bindings

end

module ModuleName : SIGNAME = struct

bindings

end

Hiding things

Real value of signatures is to to hide bindings and type definitions

• So far, just documenting and checking the types

​

Hiding implementation details is the most important strategy for writing correct, robust, reusable software

​

So first remind ourselves that functions already do well for some forms of hiding…

​

Hiding with functions

These three functions are totally equivalent: no client can tell which we are using (so we can change our choice later):

​

Defining helper functions locally is also powerful

• Can change/remove functions later and know it affects no other code

Would be good to have “private” top-level functions too

• So two functions could share a helper function
• ML does this via signatures that omit bindings…

let double x = x*2

let double x = x+x

let y = 2

let double x = x*y

Example

Outside the module, MyMathLib.doubler is simply unbound

• So cannot be used [directly]
• Fairly powerful, very simple idea

module type MATHLIB = sig

val fact : int -> int

val half_pi : float

end

module MyMathLib : MYMATHLIB = struct

let rec fact x = ...

let half_pi = Float.pi /. 2.0

let doubler x = x *. 2

end

​

More OCaml pragmatics

• Recall file foo.ml implicitly defines the Foo module with no explicit module Foo = struct … end
• Similarly, if foo.mli is present, it is the signature for Foo with no explicit module type SOMENAME = sig … end
• foo.ml is type-checked as though it is module Foo : SOMENAME = …
• Other modules type-checked with foo.mli hiding things
• If no foo.mli present, then just “nothing hidden”

A larger example [mostly see the code]

Now consider a module that defines an Abstract Data Type (ADT)

• A type of data and operations on it

Our example: rational numbers with add and string_of_rational

​

module Rational1 = struct

type rational = Whole of int | Frac of int*int

exception BadFrac

​

(*internal functions gcd, reduce not on slide*)

​

let rec make_frac (n, d) = …

let rec add r1 r2 = …

let string_of_rational r = …

end

​

​

​

Library spec and invariants

Properties [externally visible guarantees, up to library writer]

• Disallow denominators of 0
• Return strings in reduced form (“4” not “4/1”, “3/2” not “9/6”)
• Correct math
• No infinite loops or exceptions

​

Invariants [part of the implementation, not the module’s spec]

• All denominators are greater than 0
• All rational values returned from functions are reduced

​

More on invariants

Our code guarantees the invariants and relies on them

Guarantee:

• make_frac disallows 0 denominator, removes negative denominator, and reduces result
• add calls reduce after multiplying denominators

Rely:

• gcd does not work with negative arguments, but no denominator can be negative
• add uses math properties to avoid calling reduce
• string_of_rational assumes its argument is reduced

​

A first signature

With what we know so far, this signature makes sense:

• gcd and reduce not visible outside the module

module type RATIONAL_A = sig

type rational = Whole of int | Frac of int * int

exception BadFrac

val make_frac : int * int -> rational

val add : rational -> rational -> rational

val string_of_rational : rational -> string

end

​

module Rational1 : RATIONAL_A = struct ...

​

The problem

By revealing the type definition, we let clients violate our invariants by directly creating values of type Rational1.rational

• At best a comment saying “must use Rational1.make_frac”

​

​

​

​

Any of these can lead to infinite loops or wrong results, which is why the module’s code would never return them:

• Rational1.Frac (3,1)
• Rational1.Frac (1,0)
• Rational1.Frac (3,-2)
• Rational1.Frac (9,6)

module type RATIONAL_A = sig

type rational = Whole of int | Frac of int * int

...

So hide more

Key idea: An ADT must hide the concrete type definition so clients cannot create invariant-violating values of the type directly

​

Alas, this attempt doesn’t work because the signature now uses a type rational that is not known to exist:

module type RATIONAL_WRONG = sig

exception BadFrac

val make_frac : int * int -> rational

val add : rational -> rational -> rational

val string_of_rational : rational -> string

end

​

module Rational1 : RATIONAL_WRONG = struct ...

​

Abstract types

So OCaml has a feature for exactly this [common!!] situation:

​

In a signature: type foo

means the type exists, but clients do not know its definition

module type RATIONAL_B = sig

type rational

exception BadFrac

val make_frac : int * int -> rational

val add : rational -> rational -> rational

val string_of_rational : rational -> string

end

​

module Rational1 : RATIONAL_B = struct ...

​

This works! (And is a Really Big Deal)

Nothing a client can do to violate invariants and properties:

• Only way to make first rational is Rational1.make_frac
• After that can use only Rational1.make_frac, Rational1.add, and Rational1.string_of_rational
• Hides constructors and patterns – don’t even know whether or not Rational1.rational is a variant type (it might not be!)
• But clients can still pass around fractions in any way

Using the module system to enforce abstractions

Two key restrictions

So we have two powerful ways to use signatures for hiding:

​

1. Deny bindings exist (variables, functions, ...)

​

• Make types abstract (so clients cannot directly create values of them nor directly access their pieces)

​

(Later we will see a signature can also make a binding’s type more specific than it is inside the module, which is cool but less important)

What about whole?

Must carefully reason about each public binding to ensure it does not break any abstractions

​

The whole function turns out to be fine

​

In fact, it would be okay to expose the Whole constructor as only Frac is a problem

• OCaml happens not to allow this; it does not treat Whole as a function, so we wrapped it with whole
• Another ML language, SML, allows exposing constructors as functions, which is cute

​

Signature matching

Have so far relied on an informal notion of, “does a module type-check given a signature?” As usual, there are precise rules…

​

module Foo : BAR is allowed if:

​

• Every non-abstract type in BAR is provided in Foo, as specified
• Every abstract type in BAR is provided in Foo in some way
• Can be a variant type or a type synonym
• Every val binding in BAR is provided in Foo, possibly with a more general and/or less abstract internal type
• Discussed “more general types” earlier in course
• Will see example soon
• Every exception in BAR is provided in Foo

Notice Foo can have more bindings (implicit in above rules)

Equivalent implementations

A key purpose of abstraction is to allow different implementations to be equivalent

• No client can tell which you are using
• So can improve/replace/choose implementations later
• Easier to do if you start with more abstract signatures (reveal only what you must)

Now: a second structure that can also have signature RATIONAL_A,

RATIONAL_B, or RATIONAL_C

• But only equivalent under RATIONAL_B or RATIONAL_C

(ignoring overflow)

​

Equivalent implementations

Example (see code file):

• structure Rational2 does not keep rationals in reduced form, instead reducing them “at last moment” in string_of_rational
• Also make gcd and reduce local functions
• Not equivalent under RATIONAL_A
• Rational1.string_of_rational(Rational1.Frac(9,6)) = "9/6"
• Rational2.string_of_rational(Rational2.Frac(9,6)) = "3/2"
• Equivalent under RATIONAL_B or RATIONAL_C
• Different invariants, but same properties
• Essential that type rational is abstract

More interesting example

Given a signature with an abstract type, different structures can:

• Have that signature
• But implement the abstract type differently

​

Such structures might or might not be equivalent

​

Example (see code):

• type rational = int * int
• Does not have signature RATIONAL_A
• Equivalent to both previous structures under RATIONAL_B or RATIONAL_C

Some interesting details for Rational3

• Internally make_frac has type int * int -> int * int, but externally int * int -> rational
• Client cannot tell if we return argument unchanged
• Could give type rational -> rational in signature, but this is awful: makes entire module unusable – why?
• Internally whole has type 'a -> 'a * int but externally int -> rational
• Matches because can specialize 'a to int and then abstract int * int to rational
• whole cannot have types 'a -> int * int or 'a -> rational (must specialize all 'a uses)
• Type-checker figures all this out for us

Can’t mix-and-match module bindings

Modules with the same signatures still define different types

​

So things like this do not type-check (good!):

• Rational1.string_of_rational(Rational2.make_frac(9,6))
• Rational3.string_of_rational(Rational2.make_frac(9,6))

​

This is a crucial behavior for type system and module properties:

• Different modules have different internal invariants!
• In fact, they have different type definitions
• Rational1.rational looks like Rational2.rational, but clients and the type-checker do not know that
• Rational3.rational is int*int not a variant type!

​

​