# 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.

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

 ```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)

 ```type point val origin : point ```

 ```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.

 ```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.

 ```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...

 ```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.

```    G
/   \
C     R
...
```

This is an instance of the diamond import problem:

```    G
/   \
C     R
\   /
P
```

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( R.center( ... ))
```

C.mkcirc has type C.P.point * int -> C.circle while R.center 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:

• Seperates signatures from implementation
• Uses only dependent signatures for type-checking, not the actual implementations
• Every instance you create is new and distinct from all the others (to support generativity and local state)

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)
```
• The body of open cannot contain t free.
• There is no way to find out what the representation type is!
• Modules are first class values.

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 = ...
Σt.<t,t->int,...>
```

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.