Modules and ? Types: HoPL 3/15/2004

Presented by Ryan Culpepper
Transcribed by Felix Klock

Modules for Standard ML (MacQueen '84)

So we've got some code...

type point = int * int
val origin : point = (0,0)
type circle = point * int

We'd like to decompose the lines above into seperate pieces, that can be reasoned about (and compiled) independently.

So lets put boxes around the bits we want to isolate...

type point = int * int
val origin : point = (0,0)

type circle = point * int

But, this breaks. Specifically, the second box is broken, because it doesn't know what a point is.

We'll fix this by explicitly indicating that the second box depends on some declarations that are provided elsewhere.

module Point : POINT
type point = int * int
val origin : point = (0,0)

module Circle(P : POINT) : CIRCLE
type circle = P.point * int

So we've now explicitly named our modules, and parameterized them over other modules.

POINT and CIRCLE are signatures that act to describe the modules (just as types describe values)

signature POINT
type point
val origin : point

signature CIRCLE
type circle

When you take things apart, you need to know how to put them back togther again.

Q (from Audience) : Can you have the same signature being used by distinct modules?
A: Yep.

Since anyone who deals with Circles needs to deal with Points too, we need to package the points with the Circle module too.

module Circle(P' : POINT) : CIRCLE
instance P = P'
type circle = P.point * int

Q (from Audience) : So you have a binding instance of P above, and an instance down below that references it... which P is which?
A: I'll add a prime to distinquish them

And we add instance P : POINT to the CIRCLE signature as well.

signature CIRCLE
instance P : POINT
type circle

So we've got values, types, modules, signatures, instances ...

Q (from Audience) : Which P is in the signature?
A: The prime-less P

Lets investigate further...

signature RECT
instance P : POINT
type rect

We've presumably got a Rect module somewhere (parameterized over Point as well),so we've got Circles and Rectangles.Lets add a Geometry module that uses them.

  /   \   
 C     R  

This is an instance of the diamond import problem:

  /   \   
 C     R  
  \   /   

G needs to be able to interchange data between C and R. So the P's better bed the same!

Here's something more concrete

C.mkcirc( ... ))

C.mkcirc has type C.P.point * int -> while has type R.rect -> R.P.point

So to type-check G, we need to ensure that C.P.point = R.P.point

This is known as the sharing problem

ML solves it with an explicit declaration in G that for itsimports C and R, C.P = R.P

In summary, this module system:

But, there's a downside. You have to explicit construct points using the constructors provided by the Point module; you can't just use the more convenient tuple syntax: (...,...)

Q (from Audience (Sam)) : Why is a construction function (int * int) -> Point undesirable/unacceptable?
A: Its inconvenient when you need to change your code later.
Q (from Audience (Sam)) : So what? Changes are inconvenient, but allowing the tuple syntax to directly construct points is going to make later change MORE inconvenient, not less. They're independent.
A: ...

Scribe's Note: Much discussion follows... Matthias ends the discussion saying that Sam's argument yields Mitchell and Plotkin in the limit

And on that note, we have...

Abstract Types have Existential Type (Mitchell and Plotkin, '84)

val C = rep t.<t , t -> int, ...>(int * int) <origin = <0,0>, getx, ...>
abstype t with <origin, getx, ...> is C
in getx(origin)

But, its inconvenient to always make the representation type totally opaque.

So we switch to Generalized Sums...

Using Dependent Types to Express Modular Structure (MacQueen '86)

val C = ...

To understand generalized sums (Σ), lets look at the simpler case of disjoint sums first:

A + B can be seen as a kind of special tupling: { <Left, a> } ∪ { <Right, b> } where a : A, b : B, and Left and Right are TAGS

For generalized sums, we generalize what we can put into the tag field, and we allow elements of the second tuple position can depend on what is in the first position.

So if we have the following type: Σ t : Type . <t,t->int,...>, we can construct one of its elements like so:

<int * int, <<0,0>,fst,...>>

Here, the element in the second position, <<0,0>,fst,...>, is linked to the element in the first position.

E.g. <0,0> : int * int, fst : int * int -> int, etc

So, now that we have some intuition about what Generalized Sums are, lets look at how the paper uses them for a module system.

texp ::= ...  | witness(svar)
sig  ::= Type | Σ svar : sig . texp | Σ svar : sig . sig 
Q (from Audience) : Is this to indicate "sharing" ?
A: No, this is NOT a solution to the diamond import problem.

A big idea to take away from this is that we have OPEN module instances but CLOSED signatures.

Harper + Lillibridge, Leroy

These papers opened up the signatures a bit; their systems allow the specification of types in the signature.

Harper + Lillibridge call them Translucent Sums. Their type system, however, is undecidable.