Backpack:

Retrofitting Haskell
with Interfaces
Scott Kilpatrick
MPI-SWS

Derek Dreyer
Simon Peyton Jones
Simon Marlow

MPI-SWS
Microsoft Research
Facebook

POPL ’14
22 January 2014

Strong Modularity
A
B

Typecheck B separately from A bydepending on an interface A.

A
B

A

A

B

B
2

Strong Modularity
A
B

Typecheck B separately from A bydepending on an interface A.

A
B

A

A

B

B
2

Strong Modularity
A

Typecheck B separately from A bydepending on an interface A.

B

A1

A
B

Reuse B by instantiating it withdifferent implementations of A.

A2
B

B

A

A

B

B
2

Strong Modularity
A

Typecheck B separately from A bydepending on an interface A.

B

A1

A
B

Reuse B by instantiating it withdifferent implementations of A.

A2
B

B

A

A

B

B
2

Strong Modularity
A

Typecheck B separately from A bydepending on an interface A.

B

A1

A
B

A2
B

B

Reuse B by instantiating it withdifferent implementations of A.
Typecheck mutuallydependent modules before
tying the recursive knot.

AA
B
B

2

Weak Modularity(implementations depend on implementations)• at Haskell’s

module level

SocketServer3

Weak Modularity(implementations depend on implementations)• at Haskell’s• at Haskell’s

module levelpackage level

SocketP-1.1
Server

1.4
1.3
1.2

P-1.*

Q-2

3

Weak Modularity(implementations depend on implementations)• at Haskell’s• at Haskell’s

module levelpackage level

SocketP-1.1
Serverno interfaces

1.4
1.3
1.2

P-1.*

Q-2

no strong modularity
3

Haskell has
weak modularity.
We want to extend itwith strong modularity.

4

Haskell has
weak modularity.
We want to extend itwith strong modularity.
Solution:

Retrofit4

Haskell has
weak modularity.
We want to extend itwith strong modularity.
Solution:

Retrofit

Designstrong layer
on top of
weak modules!
4

“Why not just use the ML
module system?” (i.e. functors)

5

“Why not just use the ML
module system?” (i.e. functors)
good
point

• a lot of work on the ML module system• interfaces via signatures, reuse via functors

5

“Why not just use the ML
module system?” (i.e. functors)
good
point

• a lot of work on the ML module system• interfaces via signatures, reuse via functors

but5

“Why not just use the ML
module system?” (i.e. functors)
good
point

• a lot of work on the ML module system• interfaces via signatures, reuse via functors

but• functors won’t work for us- incompatible with recursive linking- unclear how to incorporate into weak modules

5

“Why not just use the ML
module system?” (i.e. functors)
good
point

• a lot of work on the ML module system• interfaces via signatures, reuse via functors

but• functors won’t work for us- incompatible with recursive linking- unclear how to incorporate into weak modules• functors are ill-suited for separate compilation- ML langs require additional system on top
5Introducing Backpack
strongweak• Retrofits Haskell with strong modularity- Designed at package level- Employs simplified mixin design- Defined as elaboration into weak Haskell modules- Separate typechecking, not separate compilation
6

Outline• Language tour
• Semantics• Future work7

modulesin today’s
Haskell
Socketinterfaces

SocketServerSocketServer8

Modules in Today’s Haskell
Socket.hs

module Socket wheredata SocketT = ...
open = ...

SocketServerServer.hs

module Server whereimport Socket
data ServerT = ...SocketT...
9

Modules in Today’s Haskell
Socket.hs

module Socket wheredata SocketT = ...
open = ...

SocketServerServer.hs

module Server whereimport Socket
data ServerT = ...SocketT...
9

Modules in Today’s Haskell
Socket.hs

module Socket wheredata SocketT = ...
open = ...

SocketServerServer.hs

module Server whereimport Socket
data ServerT = ...SocketT...
9

Modules in Today’s Haskell
Socket.hs

module Socket wheredata SocketT = ...
open = ...

SocketServerServer.hs

module Server whereimport Socket
data ServerT = ...SocketT...
9

Modules in Today’s Haskell
Socket.hs

module Socket wheredata SocketT = ...
open = ...

SocketServerServer.hs

module Server whereimport Socket
data ServerT = ...SocketT...
9

Modules in Today’s Haskell
Socket.hs

module Socket wheredata SocketT = ...
open = ...

SocketServerServer.hs

module Server whereimport Socket
data ServerT = ...SocketT...
9

modulesin today’s
Haskell
Socketinterfaces

SocketServerSocketServer10

Boot Files: Almost Interfaces
Socket.hs-bootSocket≈module Socket wheredata SocketT
open :: Int -> SocketT• implementation mechanism in GHC compiler• used as “forward declaration” for recursive modules
11Boot Files: Almost Interfaces
Socket.hs-bootSocket≈module Socket wheredata SocketT
open :: Int -> SocketT• implementation mechanism in GHC compiler• used as “forward declaration” for recursive modules
11Boot Files: Almost Interfaces
Socket.hs-bootSocket≈module Socket wheredata SocketT
open :: Int -> SocketT• implementation mechanism in GHC compiler• used as “forward declaration” for recursive modules
11modulesin today’s
Haskell
Socketinterfaces

SocketServerSocketServer12

Packages in Backpack
Socket.hs

module Socket wheredata SocketT = ...
open = ...

SocketServerServer.hs

module Server whereimport Socket
data ServerT = ...SocketT...
13

Main =

import qualified A.Server
import qualified B.Server...

Packages in Backpack

package serverlib
where�data SocketT�Socket :: open :: Int -> SocketT��
importSocketServer =data ServerT = ...SocketT...

package complete-serverwhere�data SocketT = ...�SocketSocket = open = ...
��
ServerimportSocketServer =data ServerT = ...SocketT...
package server where
Socket = [Socket.hs]
Server = [Server.hs]

package serverimpl where
13
include socketsig

Main =

import qualified A.Server
import qualified B.Server...

Packages in Backpack

package serverlib
where�data SocketT�Socket :: open :: Int -> SocketT��
importSocketServer =data ServerT = ...SocketT...

package complete-serverwhere�data SocketT = ...�SocketSocket = open = ...
��
ServerimportSocketServer =data ServerT = ...SocketT...
package server where
Socket = [Socket.hs]
Server = [Server.hs]

package serverimpl where
13
include socketsig

Main =

import qualified A.Server
import qualified B.Server...

Packages in Backpack

package serverlib
where�data SocketT�Socket :: open :: Int -> SocketT��
importSocketServer =data ServerT = ...SocketT...

package complete-serverwhere�data SocketT = ...�SocketSocket = open = ...
��
ServerimportSocketServer =data ServerT = ...SocketT...
package server where
Socket = [Socket.hs]
Server = [Server.hs]

package serverimpl where
13
include socketsig

Main =

import qualified A.Server
import qualified B.Server...

Packages in Backpack

package serverlib
where�data SocketT�Socket :: open :: Int -> SocketT��
importSocketServer =data ServerT = ...SocketT...

package complete-serverwhere�data SocketT = ...�SocketSocket = open = ...
��
ServerimportSocketServer =data ServerT = ...SocketT...
package server where
Socket = [Socket.hs]
Server = [Server.hs]

package serverimpl where
13
include socketsig

Main =

import qualified A.Server
import qualified B.Server...

Packages in Backpack

package serverlib
where�data SocketT�Socket :: open :: Int -> SocketT��
importSocketServer =data ServerT = ...SocketT...

package complete-serverwhere�data SocketT = ...�SocketSocket = open = ...
��
ServerimportSocketServer =data ServerT = ...SocketT...
package server where
Socket = [Socket.hs]
Server = [Server.hs]

package serverimpl where
13
include socketsig

Packages in Backpack

package multi-shared whereC= {include serverimpl;
includesocketimpl(With
Holes)
D= {include
serverimpl;
includesocketimpl
��
import qualified C.Server
Main = import qualified D.Server...

package partial-serverwhere�data SocketT�SocketSocket ::open :: Int -> SocketT��
importSocketServerServer =data ServerT = ...SocketT...
package complete-serverwhere�data SocketT = ...�Socket = open = ...
��
importSocketServer =data
ServerT=...SocketT...
14

Packages in Backpack

package multi-shared whereC= {include serverimpl;
includesocketimpl(With
Holes)
D= {include
serverimpl;
includesocketimpl
��
import qualified C.Server
Main = import qualified D.Server...

package partial-serverwhere�data SocketT�SocketSocket ::open :: Int -> SocketT��
importSocketServerServer =data ServerT = ...SocketT...
package complete-serverwhere�data SocketT = ...�Socket = open = ...
��
importSocketServer =data
ServerT=...SocketT...
14

Packages in Backpack

package multi-shared whereC= {include serverimpl;
includesocketimpl(With
Holes)
D= {include
serverimpl;
includesocketimpl
��
import qualified C.Server
Main = import qualified D.Server...

package partial-serverwhere�data SocketT�SocketSocket ::open :: Int -> SocketT��
importSocketServerServer =data ServerT = ...SocketT...
package complete-serverwhere�data SocketT = ...�Socket = open = ...
��
importSocketServer =data
ServerT=...SocketT...
14

Packages in Backpack

package multi-shared whereC= {include serverimpl;
includesocketimpl(With
Holes)
D= {include
serverimpl;
includesocketimpl
��
import qualified C.Server
Main = import qualified D.Server...

package partial-serverwhere�data SocketT�SocketSocket ::open :: Int -> SocketT��
importSocketServerServer =data ServerT = ...SocketT...
package complete-serverwhere�data SocketT = ...�Socket = open = ...
��
importSocketServer =data
ServerT=...SocketT...
14

import qualified B.Server...

Package Inclusion

package serverlib
where�data SocketT�Socket :: open :: Int -> SocketT��
importSocketServer =data ServerT = ...SocketT...
package complete-serverwhere�data SocketT = ...�Socket = open = ...
��
importSocketServer =data ServerT = ...SocketT...
package server where
Socket = [Socket.hs]
Server = [Server.hs]

15
package serverimpl wherepackagecomplete-server
wherepackage partial-serverwhere�data SocketT�include socketimpl
��
Socket :: import
SocketInt -> SocketTServer = open ::�data ServerT = ...SocketT... �Server = import Socket
package serverdata
whereServerT = ...SocketT...
Socket = [Socket.hs]
package
where
Server complete-server= [Server.hs]
�data SocketT = ...�Socket = open = ...
package socketimpl
��data where�
SocketT= ...
importSocketServerSocket =open...
data =ServerT= ...SocketT...

Package Inclusion

wherewhere
package serverimpl
complete-server
include socketsig
socketimpl
��
importSocketServer=[...]Server =data ServerT = ...SocketT...
package server-linked where package server-linked-alt where
packagewhere
includeserver
serverimpl
include serverimpl
Socket= [Socket.hs]
include socketimpl
include socketimpl-alt
Server = [Server.hs]

package serverimpl where KSer15

P
M
P
P
B
T
R

M
S

packagecomplete-server
wherepackage partial-serverwhere�data SocketT�include socketimpl
��
Socket :: import
SocketInt -> SocketTServer = open ::�data ServerT = ...SocketT... �Server = import Socket
package serverdata
whereServerT = ...SocketT...
Socket = [Socket.hs]
package
where
Server complete-server= [Server.hs]
�data SocketT = ...�Socket = open = ...
package socketimpl
��data where�
SocketT= ...
importSocketServerSocket =open...
data =ServerT= ...SocketT...

P
M
P
P
B
T
R

Package Inclusion

Socketwherewhere
package serverimpl
complete-server
include socketsig
socketimpl
��
importSocketServer=[...]Server =data ServerT = ...SocketT...
package server-linked where package server-linked-alt where
packagewhere
includeserver
serverimpl
include serverimpl
Socket= [Socket.hs]
include socketimpl
include socketimpl-alt
Server = [Server.hs]

package serverimpl where KSer15

M
Spackagecomplete-server
wherepackage partial-serverwhere�data SocketT�include socketimpl
��
Socket :: import
SocketInt -> SocketTServer = open ::�data ServerT = ...SocketT... �Server = import Socket
package serverdata
whereServerT = ...SocketT...
Socket = [Socket.hs]
package
where
Server complete-server= [Server.hs]
�data SocketT = ...�Socket = open = ...
package socketimpl
��data where�
SocketT= ...
importSocketServerSocket =open...
data =ServerT= ...SocketT...

P
M
P
P
B
T
R

Package Inclusion

Socketwherewhere
package serverimpl
complete-server
include socketsig
socketimpl
��
importSocketServer=[...]Server =data ServerT = ...SocketT...
package server-linked where package server-linked-alt where
packagewhere
includeserver
serverimpl
include serverimpl
Socket= [Socket.hs]
include socketimpl
include socketimpl-alt
Server = [Server.hs]

package serverimpl where KSer15

M
Spackagecomplete-server
wherepackage partial-serverwhere�data SocketT�include socketimpl
��
Socket :: import
SocketInt -> SocketTServer = open ::�data ServerT = ...SocketT... �Server = import Socket
package serverdata
whereServerT = ...SocketT...
Socket = [Socket.hs]
package
where
Server complete-server= [Server.hs]
�data SocketT = ...�Socket = open = ...
package socketimpl
��data where�
SocketT= ...
importSocketServerSocket =open...
data =ServerT= ...SocketT...

P
M
P
P
B
T
R

Package Inclusion

Socketwherewhere
package serverimpl
complete-server
Socketinclude socketsig
socketimpl
��
importSocketServer=[...]Server =data ServerT = ...SocketT...
package server-linked where package server-linked-alt where
packagewhere
includeserver
serverimpl
include serverimpl
Socket= [Socket.hs]
include socketimpl
include socketimpl-alt
Server = [Server.hs]

package serverimpl where KSer15

M
Spackagecomplete-server
wherepackage partial-serverwhere�data SocketT�include socketimpl
��
Socket :: import
SocketInt -> SocketTServer = open ::�data ServerT = ...SocketT... �Server = import Socket
package serverdata
whereServerT = ...SocketT...
Socket = [Socket.hs]
package
where
Server complete-server= [Server.hs]
�data SocketT = ...�Socket = open = ...
package socketimpl
��data where�
SocketT= ...
importSocketServerSocket =open...
data =ServerT= ...SocketT...

P
M
P
P
B
T
R

Package Inclusion

Socketwherewhere
package serverimpl
complete-server
Socketinclude socketsig
socketimpl
��
importSocketServer=[...]Server =Serverdata ServerT = ...SocketT...
package server-linked where package server-linked-alt where
packagewhere
includeserver
serverimpl
include serverimpl
Socket= [Socket.hs]
include socketimpl
include socketimpl-alt
Server = [Server.hs]

package serverimpl where KSer15

M
Spackagecomplete-server
wherepackage partial-serverwhere�data SocketT�include socketimpl
��
Socket :: import
SocketInt -> SocketTServer = open ::�data ServerT = ...SocketT... �Server = import Socket
package serverdata
whereServerT = ...SocketT...
Socket = [Socket.hs]
package
where
Server complete-server= [Server.hs]
�data SocketT = ...�Socket = open = ...
package socketimpl
��data where�
SocketT= ...
importSocketServerSocket =open...
data =ServerT= ...SocketT...

Package Inclusion

wherewhere
package serverimpl
complete-server
include socketsig
socketimpl
��
importSocketServer=[...]Server =data ServerT = ...SocketT...
package server-linked where package server-linked-alt where
packagewhere
includeserver
serverimpl
include serverimpl
Socket= [Socket.hs]
include socketimpl
include socketimpl-alt
Server = [Server.hs]

package serverimpl where KSer16

P
M
P
P
B
T
R

M
S

package complete-server where
include socketimpl
��
importSocketServer =data ServerT = ...SocketT...

Package Inclusion

package server where
package
where
Socket multi-shared= [Socket.hs]
C=={include
serverimpl; include socketimpl}
Server[Server.hs]D= {include
serverimpl;
includesocketimpl}
��
package socketsig
wherequalified C.Server ��importdata SocketT
Main=
importqualified D.Server
Socket ::open :: Int -> SocketT...

package serverimpl
wherepartial-server
whereinclude socketsig
socketsig��Server = [...]
importSocketServer =data ServerT = ...SocketT...
package server-linked where package server-linked-alt where
packagewhere include
includecomplete-server
serverimpl
serverimpl
�data SocketT�=...
includeinclude socketimpl-alt
Socket socketimpl= open = ...
��
importSocketServer =KSer 16
data ServerT = ...SocketT...

Pa
M
Pa
Pa
Bi
Th
Re

M
Si

package complete-server where
include socketimpl
��
importSocketServer =data ServerT = ...SocketT...

Package Inclusion

package server where
package
where
Socket multi-shared= [Socket.hs]
C=={include
serverimpl; include socketimpl}
Server[Server.hs]D= {include
serverimpl;
includesocketimpl}
��
package socketsig
wherequalified C.Server ��importSocketdata
SocketT
Main=
Socket :: import qualified D.Server
open :: Int -> SocketT...

package serverimpl
wherepartial-server
whereinclude socketsig
socketsig��Server = [...]
importSocketServer =data ServerT = ...SocketT...
package server-linked where package server-linked-alt where
packagewhere include
includecomplete-server
serverimpl
serverimpl
�data SocketT�=...
includeinclude socketimpl-alt
Socket socketimpl= open = ...
��
importSocketServer =KSer 16
data ServerT = ...SocketT...

Pa
M
Pa
Pa
Bi
Th
Re

M
Si

package complete-server where
include socketimpl
��
importSocketServer =data ServerT = ...SocketT...

Package Inclusion

package server where
package
where
Socket multi-shared= [Socket.hs]
C=={include
serverimpl; include socketimpl}
Server[Server.hs]D= {include
serverimpl;
includesocketimpl}
��
package socketsig
wherequalified C.Server ��importSocketdata
SocketT
Main=
Socket :: import qualified D.Server
open :: Int -> SocketT...

package serverimpl
wherepartial-server
whereinclude socketsig
socketsig��Server = [...]
importSocketServer =data ServerT = ...SocketT...
package server-linked where package server-linked-alt where
packagewhere include
includecomplete-server
serverimpl
serverimpl
�data SocketT�=...
includeinclude socketimpl-alt
Socket socketimpl= open = ...
��
importSocketServer =KSer 16
data ServerT = ...SocketT...

Pa
M
Pa
Pa
Bi
Th
Re

M
Si

package complete-server where
include socketimpl
��
importSocketServer =data ServerT = ...SocketT...

Package Inclusion

package server where
package
where
Socket multi-shared= [Socket.hs]
C=={include
serverimpl; include socketimpl}
Server[Server.hs]D= {include
serverimpl;
includesocketimpl}
��
package socketsig
wherequalified C.Server ��importSocketdata
SocketT
Main=
Socket :: import qualified D.Server
open :: Int -> SocketT...

package serverimpl
wherepartial-server
where
Socketinclude socketsig
socketsig��Server = [...]
importSocketServer =data ServerT = ...SocketT...
package server-linked where package server-linked-alt where
packagewhere include
includecomplete-server
serverimpl
serverimpl
�data SocketT�=...
includeinclude socketimpl-alt
Socket socketimpl= open = ...
��
importSocketServer =KSer 16
data ServerT = ...SocketT...

Pa
M
Pa
Pa
Bi
Th
Re

M
Si

package complete-server where
include socketimpl
��
importSocketServer =data ServerT = ...SocketT...

Package Inclusion

package server where
package
where
Socket multi-shared= [Socket.hs]
C=={include
serverimpl; include socketimpl}
Server[Server.hs]D= {include
serverimpl;
includesocketimpl}
��
package socketsig
wherequalified C.Server ��importSocketdata
SocketT
Main=
Socket :: import qualified D.Server
open :: Int -> SocketT...

package serverimpl
wherepartial-server
where
Socketinclude socketsig
socketsig��Server = [...]
importSocketServerServer =data ServerT = ...SocketT...
package server-linked where package server-linked-alt where
packagewhere include
includecomplete-server
serverimpl
serverimpl
�data SocketT�=...
includeinclude socketimpl-alt
Socket socketimpl= open = ...
��
importSocketServer =KSer 16
data ServerT = ...SocketT...

Pa
M
Pa
Pa
Bi
Th
Re

M
Si

package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...
...open 80 ...
Package Names
P ∈ PkgNames
packageserverwhereD={includeserverimpl;
includesocketimpl}
package server where��Module Path Namesp ∈ ModPaths
Socket = [data SocketT = ...]
import qualified C.Server
Socket = [data SocketT = ...]
Package
Respositories R ::= D1 , . . .�, Dn��� Main = import qualified D.Server
importSocketServer = Package Definitions
D ::= package P
Server = import Socket
data
ServerT=...SocketT...
...
data ServerT = ...SocketT...
Bindings
B ::= p = [M ] | p
package socketimpl
Thinning
Specst� ::= (p1 , . . . , pn )package partial-server where
package socketsig
�data where�datawhere�
SocketT=...
SocketT
Renaming Specsr ::= �p1 �→ p�1 , .
includesocketsig
Socket=��
Socket :: open :: Int -> SocketT
open = λn. . . .
Server = import Socket
Modulewhere
Expressions M ::= imports; exdata ServerT = ...SocketT...
package serverimpl
package serverimpl where
Signature Expressions S ::= imports; deinclude socketimpl
include socketimpl
where
�
�
�
�package complete-server�data SocketT = ...�importSocketimportSocketServer =Server =data ServerT = ...SocketT...
data ServerT = ...SocketT... Socket = open = ...
��SocketSocketServerSocketServer = import Socket
data ServerT = ...SocketT...
package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...package multi-shared where...open 80 ...
C= {include serverimpl; include socketimpl}

Linking

package complete-server where
include socketimpl
��
importSocketServer =data ServerT = ...SocketT...

ere package main where package server where= [Socket.hs]
include partial-server Socket
Server = [Server.hs]
include socketimpl package serverimpl where
include socketsig
Server = [...]

package server-linked where package server-linked-alt where
include serverimpl
include serverimpl
include socketimpl
include socketimpl-alt
KSer

KSock
alt
KSock

KA
KB

17 α

package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...
...open 80 ...
Package Names
P ∈ PkgNames
packageserverwhereD={includeserverimpl;
includesocketimpl}
package server where��Module Path Namesp ∈ ModPaths
Socket = [data SocketT = ...]
import qualified C.Server
Socket = [data SocketT = ...]
Package
Respositories R ::= D1 , . . .�, Dn��� Main = import qualified D.Server
importSocketServer = Package Definitions
D ::= package P
Server = import Socket
data
ServerT=...SocketT...
...
data ServerT = ...SocketT...
Bindings
B ::= p = [M ] | p
package socketimpl
Thinning
Specst� ::= (p1 , . . . , pn )package partial-server where
package socketsig
�data where�datawhere�
SocketT=...
SocketT
Renaming Specsr ::= �p1 �→ p�1 , .
includesocketsig
Socket=��
Socket :: open :: Int -> SocketT
open = λn. . . .
Server = import Socket
Modulewhere
Expressions M ::= imports; exdata ServerT = ...SocketT...
package serverimpl
package serverimpl where
Signature Expressions S ::= imports; deinclude socketimpl
include socketimpl
where
�
�
�
�package complete-server�data SocketT = ...�importSocketimportSocketServer =Server =data ServerT = ...SocketT...
data ServerT = ...SocketT... Socket = open = ...
��SocketSocketServerSocketServer = import Socket
data ServerT = ...SocketT...
package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...package multi-shared where...open 80 ...
C= {include serverimpl; include socketimpl}

Linking

package complete-server where
include socketimpl
��
importSocketServer =data ServerT = ...SocketT...

ere package main where package server where= [Socket.hs]
include partial-server Socket
Server = [Server.hs]
include socketimpl package serverimpl where
include socketsig
Server = [...]

package server-linked where package server-linked-alt where
include serverimpl
include serverimpl
include socketimpl
include socketimpl-alt
KSer

KSock
alt
KSock

KA
KB

17 α

package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...
...open 80 ...
Package Names
P ∈ PkgNames
packageserverwhereD={includeserverimpl;
includesocketimpl}
package server where��Module Path Namesp ∈ ModPaths
Socket = [data SocketT = ...]
import qualified C.Server
Socket = [data SocketT = ...]
Package
Respositories R ::= D1 , . . .�, Dn��� Main = import qualified D.Server
importSocketServer = Package Definitions
D ::= package P
Server = import Socket
data
ServerT=...SocketT...
...
data ServerT = ...SocketT...
Bindings
B ::= p = [M ] | p
package socketimpl
Thinning
Specst� ::= (p1 , . . . , pn )package partial-server where
package socketsig
�data where�datawhere�
SocketT=...
SocketT
Renaming Specsr ::= �p1 �→ p�1 , .
includesocketsig
Socket=��
Socket :: open :: Int -> SocketT
open = λn. . . .
Server = import Socket
Modulewhere
Expressions M ::= imports; exdata ServerT = ...SocketT...
package serverimpl
package serverimpl where
Signature Expressions S ::= imports; deinclude socketimpl
include socketimpl
where
�
�
�
�package complete-server�data SocketT = ...�importSocketimportSocketServer =Server =data ServerT = ...SocketT...
data ServerT = ...SocketT... Socket = open = ...
��SocketSocketServerSocketServer = import Socket
data ServerT = ...SocketT...
package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...package multi-shared where...open 80 ...
C= {include serverimpl; include socketimpl}

Linking

package complete-server where
include socketimpl
��
importSocketServer =data ServerT = ...SocketT...

ere package main where package server where= [Socket.hs]
include partial-server Socket
SocketServer = [Server.hs]
include socketimpl package serverimpl where

Serverinclude socketsig
Server = [...]

package server-linked where package server-linked-alt where
include serverimpl
include serverimpl
include socketimpl
include socketimpl-alt
KSer

KSock
alt
KSock

KA
KB

17 α

package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...
...open 80 ...
Package Names
P ∈ PkgNames
packageserverwhereD={includeserverimpl;
includesocketimpl}
package server where��Module Path Namesp ∈ ModPaths
Socket = [data SocketT = ...]
import qualified C.Server
Socket = [data SocketT = ...]
Package
Respositories R ::= D1 , . . .�, Dn��� Main = import qualified D.Server
importSocketServer = Package Definitions
D ::= package P
Server = import Socket
data
ServerT=...SocketT...
...
data ServerT = ...SocketT...
Bindings
B ::= p = [M ] | p
package socketimpl
Thinning
Specst� ::= (p1 , . . . , pn )package partial-server where
package socketsig
�data where�datawhere�
SocketT=...
SocketT
Renaming Specsr ::= �p1 �→ p�1 , .
includesocketsig
Socket=��
Socket :: open :: Int -> SocketT
open = λn. . . .
Server = import Socket
Modulewhere
Expressions M ::= imports; exdata ServerT = ...SocketT...
package serverimpl
package serverimpl where
Signature Expressions S ::= imports; deinclude socketimpl
include socketimpl
where
�
�
�
�package complete-server�data SocketT = ...�importSocketimportSocketServer =Server =data ServerT = ...SocketT...
data ServerT = ...SocketT... Socket = open = ...
��SocketSocketServerSocketServer = import Socket
data ServerT = ...SocketT...
package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...package multi-shared where...open 80 ...
C= {include serverimpl; include socketimpl}

Linking

package complete-server where
include socketimpl
��
importSocketServer =data ServerT = ...SocketT...

ere package main where package server where= [Socket.hs]
include partial-server Socket
SocketServer = [Server.hs]
include socketimpl package serverimpl where

Serverinclude socketsig
Server = [...]

package server-linked where package server-linked-alt where
include serverimpl
include serverimpl
include socketimpl
include socketimpl-alt
KSer

KSock
alt
KSock

KA
KB

17 α

package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...
...open 80 ...
Package Names
P ∈ PkgNames
packageserverwhereD={includeserverimpl;
includesocketimpl}
package server where��Module Path Namesp ∈ ModPaths
Socket = [data SocketT = ...]
import qualified C.Server
Socket = [data SocketT = ...]
Package
Respositories R ::= D1 , . . .�, Dn��� Main = import qualified D.Server
importSocketServer = Package Definitions
D ::= package P
Server = import Socket
data
ServerT=...SocketT...
...
data ServerT = ...SocketT...
Bindings
B ::= p = [M ] | p
package socketimpl
Thinning
Specst� ::= (p1 , . . . , pn )package partial-server where
package socketsig
�data where�datawhere�
SocketT=...
SocketT
Renaming Specsr ::= �p1 �→ p�1 , .
includesocketsig
Socket=��
Socket :: open :: Int -> SocketT
open = λn. . . .
Server = import Socket
Modulewhere
Expressions M ::= imports; exdata ServerT = ...SocketT...
package serverimpl
package serverimpl where
Signature Expressions S ::= imports; deinclude socketimpl
include socketimpl
where
�
�
�
�package complete-server�data SocketT = ...�importSocketimportSocketServer =Server =data ServerT = ...SocketT...
data ServerT = ...SocketT... Socket = open = ...
��SocketSocketServerSocketServer = import Socket
data ServerT = ...SocketT...
package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...package multi-shared where...open 80 ...
C= {include serverimpl; include socketimpl}

Linking

package complete-server where
include socketimpl
��
importSocketServer =data ServerT = ...SocketT...

ere package main where package server where= [Socket.hs]
include partial-server Socket
SocketServer = [Server.hs]
include socketimpl package serverimpl where

Serverinclude socketsig
Server = [...]

package server-linked where package server-linked-alt where
include serverimpl
include serverimpl
include socketimpl
include socketimpl-alt
KSer

KSock
alt
KSock

KA
KB

17 α

package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...
...open 80 ...
Package Names
P ∈ PkgNames
packageserverwhereD={includeserverimpl;
includesocketimpl}
package server where��Module Path Namesp ∈ ModPaths
Socket = [data SocketT = ...]
import qualified C.Server
Socket = [data SocketT = ...]
Package
Respositories R ::= D1 , . . .�, Dn��� Main = import qualified D.Server
importSocketServer = Package Definitions
D ::= package P
Server = import Socket
data
ServerT=...SocketT...
...
data ServerT = ...SocketT...
Bindings
B ::= p = [M ] | p
package socketimpl
Thinning
Specst� ::= (p1 , . . . , pn )package partial-server where
package socketsig
�data where�datawhere�
SocketT=...
SocketT
Renaming Specsr ::= �p1 �→ p�1 , .
includesocketsig
Socket=��
Socket :: open :: Int -> SocketT
open = λn. . . .
Server = import Socket
Modulewhere
Expressions M ::= imports; exdata ServerT = ...SocketT...
package serverimpl
package serverimpl where
Signature Expressions S ::= imports; deinclude socketimpl
include socketimpl
where
�
�
�
�package complete-server�data SocketT = ...�importSocketimportSocketServer =Server =data ServerT = ...SocketT...
data ServerT = ...SocketT... Socket = open = ...
��SocketSocketServerSocketServer = import Socket
data ServerT = ...SocketT...
package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...package multi-shared where...open 80 ...
C= {include serverimpl; include socketimpl}

Linking

package serverlib
where�data SocketT�Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...
package complete-server where...open 80 ...

include socketimpl
��
importSocketServer =data ServerT = ...SocketT...

packageserverwhere
ere
packagemain
where package server where= [Socket.hs]
Socket= [data] SocketSocketT Socket=...
includepartial-server
Server = [Server.hs]�� ServerSocketpackage serverimpl where
includesocketimpl
Server= import
socketsig
data ServerT include=...SocketT...
Server = [...]

package server-linked where package server-linked-alt where
package socketimpl
where
where
include serverimplserverlib
includeserverimpl
�data SocketT package���
include socketimpl
include socketimpl-alt
= ...
data
SocketT:: K open :: Int -> SocketT
Socket = open = λn. . . . Socket ≤�K�
import Socket
Kpackage serverimpl where
Server = K data ServerT = ...SocketT...
include socketimpl
K ...open��
80 ...
importSocket17 αServer =
Ser

Sock
alt
Sock
A
B

package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...
...open 80 ...
Package Names
P ∈ PkgNames
packageserverwhereD={includeserverimpl;
includesocketimpl}
package server where��Module Path Namesp ∈ ModPaths
Socket = [data SocketT = ...]
import qualified C.Server
Socket = [data SocketT = ...]
Package
Respositories R ::= D1 , . . .�, Dn��� Main = import qualified D.Server
importSocketServer = Package Definitions
D ::= package P
Server = import Socket
data
ServerT=...SocketT...
...
data ServerT = ...SocketT...
Bindings
B ::= p = [M ] | p
package socketimpl
Thinning
Specst� ::= (p1 , . . . , pn )package partial-server where
package socketsig
�data where�datawhere�
SocketT=...
SocketT
Renaming Specsr ::= �p1 �→ p�1 , .
includesocketsig
Socket=��
Socket :: open :: Int -> SocketT
open = λn. . . .
Server = import Socket
Modulewhere
Expressions M ::= imports; exdata ServerT = ...SocketT...
package serverimpl
package serverimpl where
Signature Expressions S ::= imports; deinclude socketimpl
include socketimpl
where
�
�
�
�package complete-server�data SocketT = ...�importSocketimportSocketServer =Server =data ServerT = ...SocketT...
data ServerT = ...SocketT... Socket = open = ...
��SocketSocketServerSocketServer = import Socket
data ServerT = ...SocketT...
package serverlib
where
�data
�
SocketT
Socket :: open :: Int -> SocketT��
import Socket
Server = data ServerT = ...SocketT...package multi-shared where...open 80 ...
C= {include serverimpl; include socketimpl}

Linking

package complete-server where
include socketimpl
��
importSocketServer =data ServerT = ...SocketT...

ere package main where package server where= [Socket.hs]
include partial-server Socket
SocketServer = [Server.hs]
include socketimpl package serverimpl where

Serverinclude socketsig
Server = [...]

package server-linked where package server-linked-alt where
include serverimpl
include serverimpl
include socketimpl
include socketimpl-alt
KSer

KSock
alt
KSock

KA
KB

17 α

erT = package...SocketT...
socketsig
�datawhere�
SocketT
Socket ::open :: Int -> SocketT]]
package serverimpl where
include socketsig
Server =
[...]
�
etT

Reuse

nt -> package
SocketT server-linked-1 where package server-linked-2 where package main where
include partial-server
include partial-server
include socketimpleinclude socketimpl-1
include socketimpl-2
include partial-server

KSerwhere package server-linked-2 where package main where
KSockinclude partial-server
include socketimpl
altinclude socketimpl-2 KSockinclude partial-server

KSer

KSock
alt
KSock

KA
KB
α

KSer (α)

KAKB
αKSer (α)

KSer (KSock )alt
KSer (KSock)µα.KA (KB (α))

18erT = package...SocketT...
socketsig
�datawhere�
SocketT
Socket ::open :: Int -> SocketT]]
package serverimpl where
include socketsig
Server =
[...]
�
etT

Reuse

nt -> package
SocketT server-linked-1 where package server-linked-2 where package main where
SocketServerinclude partial-server
include partial-server
include socketimpleinclude socketimpl-1
include socketimpl-2
include partial-server
partial-server

KSerwhere package server-linked-2 where package main where
KSock
Socketinclude partial-server
include socketimpl
altinclude socketimpl-2 KSockinclude partial-server

KSer

KSock
alt
KSock

KA
KB
α

KSer (α)

KAKB
αKSer (α)

KSer (KSock )alt
KSer (KSock)µα.KA (KB (α))

18Serverpartial-server

erT = package...SocketT...
socketsig
�datawhere�
SocketT
Socket ::open :: Int -> SocketT]]
package serverimpl where
include socketsig
Server =
[...]
�
etT

Reuse

nt -> package
SocketT server-linked-1 where package server-linked-2 where package main where
SocketServerinclude partial-server
include partial-server
include socketimpleinclude socketimpl-1
include socketimpl-2
include partial-server
socketimpl-1 partial-server

KSerwhere package server-linked-2 where package main where
KSock
Socketinclude partial-server
include socketimpl
Socketalt
include socketimpl-2 KSockinclude partial-server

KSer

KSock
alt
KSock

KA
KB
α

KSer (α)

socketimpl-2

KA
KB
α

KSer (α)

KSer (KSock )alt
KSer (KSock)µα.KA (KB (α))

18Serverpartial-server

erT = package...SocketT...
socketsig
�datawhere�
SocketT
Socket ::open :: Int -> SocketT]]
package serverimpl where
include socketsig
Server =
[...]
�
etT

Reuse

nt -> package
SocketT server-linked-1 where package server-linked-2 where package main where
SocketServerinclude partial-server
include partial-server
include socketimpleinclude socketimpl-1
include socketimpl-2
include partial-server
socketimpl-1 partial-server

KSerwhere package server-linked-2 where package main where
KSock
Socketinclude partial-server
include socketimpl
Socketalt
include socketimpl-2 KSockinclude partial-server

KSer

KSock

KA

Serverpartial-server

socketimpl-2

KB

package multi whereαalt
KSock A= {include server-linked-1}
KSer (α)
B= {include
server-linked-2} ��KAimport qualified
A.ServerKSer (KSock)
Main = import qualifiedaltB.Server
KB
KSer (KSock )...
α
A (KB (α))
package multi-sharedµα.K
where
18
KSer (α)
C= {include serverimpl; include socketimpl}∆ � B1 ⇒ Ξ̃1∆; Ξ̃pkg � B1 : Ξ1∆∆

erT = package...SocketT...
socketsig
�datawhere�
SocketT
Socket ::open :: Int -> SocketT]]
package serverimpl where
include socketsig
Server =
[...]
�
etT

Reuse

nt -> package
SocketT server-linked-1 where package server-linked-2 where package main where
SocketServerinclude partial-server
include partial-server
include socketimpleinclude socketimpl-1
include socketimpl-2
include partial-server
socketimpl-1 partial-server

KSerwhere package server-linked-2 where package main where
KSock
Socketinclude partial-server
include socketimpl
Socketalt
include socketimpl-2 KSockinclude partial-server

KSer

KSock

partial-server

socketimpl-2

KA
KB

ServerA

package multi where
αalt
SocketKSock A= {include server-linked-1}
KSer (α)
B= {include
server-linked-2} ��KAimport qualified
A.ServerKSer (KSock)
Main = import qualifiedaltB.Server
KB
KSer (KSock )...
α
A (KB (α))
package multi-sharedµα.K
where
18
KSer (α)
C= {include serverimpl; include socketimpl}

Server∆ � B1 ⇒ Ξ̃1∆; Ξ̃pkg � B1 : Ξ1∆∆

erT = package...SocketT...
socketsig
�datawhere�
SocketT
Socket ::open :: Int -> SocketT]]
package serverimpl where
include socketsig
Server =
[...]
�
etT

Reuse

nt -> package
SocketT server-linked-1 where package server-linked-2 where package main where
SocketServerinclude partial-server
include partial-server
include socketimpleinclude socketimpl-1
include socketimpl-2
include partial-server
socketimpl-1 partial-server

KSerwhere package server-linked-2 where package main where
KSock
Socketinclude partial-server
include socketimpl
Socketalt
include socketimpl-2 KSockinclude partial-server

KSer

KSock

partial-server

socketimpl-2

KA
KB

ServerA

package multi where
αalt
SocketKSock A= {include server-linked-1}
KSer (α)
B= {include
server-linked-2} ��KABimport qualified
A.ServerKSer (KSock)
Main = import qualifiedaltB.Server
KB
SocketKSer (KSock )...
α
A (KB (α))
package multi-sharedµα.K
where
18
KSer (α)
C= {include serverimpl; include socketimpl}

Server∆ � B1 ⇒ Ξ̃1Server∆; Ξ̃pkg � B1 : Ξ1∆∆

erT = package...SocketT...
socketsig
�datawhere�
SocketT
Socket ::open :: Int -> SocketT]]
package serverimpl where
include socketsig
Server =
[...]
�
etT

Reuse

nt -> package
SocketT server-linked-1 where package server-linked-2 where package main where
SocketServerinclude partial-server
include partial-server
include socketimpleinclude socketimpl-1
include socketimpl-2
include partial-server
socketimpl-1 partial-server

KSerwhere package server-linked-2 where package main where
KSock
Socketinclude partial-server
include socketimpl
Socketalt
include socketimpl-2 KSockinclude partial-server

KSer

KSock

partial-server

socketimpl-2

KA
KB

ServerA

package multi where
αalt
SocketKSock A= {include server-linked-1}
KSer (α)
B= {include
server-linked-2} ��KABimport qualified
A.ServerKSer (KSock)
Main = import qualifiedaltB.Server
KB
SocketKSer (KSock )...
α
A (KB (α))
package multi-sharedµα.K
where
18
KSer (α)
C= {include serverimpl; include socketimpl}

Server∆ � B1 ⇒ Ξ̃1
Main

Server∆; Ξ̃pkg � B1 : Ξ1∆∆

erT = package...SocketT...
socketsig
�datawhere�
SocketT
Socket ::open :: Int -> SocketT]]
package serverimpl where
include socketsig
Server =
[...]
�
etT

Reuse

nt -> package
SocketT server-linked-1 where package server-linked-2 where package main where
SocketServerinclude partial-server
include partial-server
include socketimpleinclude socketimpl-1
include socketimpl-2
include partial-server
socketimpl-1 partial-server

KSerwhere package server-linked-2 where package main where
KSock
Socketinclude partial-server
include socketimpl
Socketalt
include socketimpl-2 KSockinclude partial-server

KSocksocketimpl-2

KA
KB

partial-serverApackage multi where
αalt
SocketKSock A= {include server-linked-1}
KSer (α)
B= {include
server-linked-2} ��KABimport qualified
A.ServerKSer (KSock)
Main = import qualifiedaltB.Server
KB
SocketKSer (KSock )...
α
A (KB (α))
package multi-sharedµα.K
where
18
KSer (α)
C= {include serverimpl; include socketimpl}

Server∆ � B1 ⇒ Ξ̃1

≠

KSer

ServerMain

Server∆; Ξ̃pkg � B1 : Ξ1∆∆

Shared Reuse

package multi whereA= {include server-linked-1}
B= {include
server-linked-2} ��import qualified A.Server
Main = import qualified B.Server...

A
SocketServer∆ � B1 ⇒ Ξ̃1
Main

B
Socketpackage multi-shared where19C= {include serverimpl; include socketimpl}

Server∆; Ξ̃pkg � B1 : Ξ1∆∆

Shared Reuse
A

package multi where
SocketA= {include server-linked-1}
B= {include
packagemulti� where server-linked-2} �Bimport server-linked-1}
qualified A.ServerA= {include= {include
import server-linked-2}
qualified B.Server
SocketBMain =
� ...
�import qualified A.Server
Main =multi-sharedimport qualified
packagewhere B.Server...
C= {include
serverimpl; include socketimpl}
D= {include
serverimpl;
include�socketimpl}
packagemulti-sharedwhere�
import partial-server;
qualified C.ServerC= {include
include socketimpl-1}
Main == {include
import partial-server;
qualified D.ServerD
include�� socketimpl-1}... qualified C.Server
importMain = import qualified D.Server
package partial-server
where
...
include socketsig��Socketpackage
Serverpartial-server= import wheredata ServerT = ...SocketT...
include socketsig��Server complete-server= �import Socket
packagewhere
data
data ServerT
SocketT==...SocketT...
...�
Socket = open = ...
19
package complete-server where

Server∆ � B1 ⇒ Ξ̃1Main∆ � B1 ⇒ Ξ̃1Server∆∆∆; Ξ∆; Ξ̃pkg � B1 : Ξ1 ∆∆; Ξ̃pkg � B1 : Ξ1

Identity Vari
Identity Con
Identities
Identity
Varia
IdentityCons
Sub
Identity
Identities
PackageIdentity
Names Subst
Module Path Names
PackageNames
Respositorie
Package
PackagePathDefinitions
ModuleNames
Bindings
Package
Respositories
Thinning
Specs
Package
Definitions

Shared Reuse
A

package multi where
SocketA= {include server-linked-1}
B= {include
packagemulti� where server-linked-2} �Bimport server-linked-1}
qualified A.ServerA= {include= {include
import server-linked-2}
qualified B.Server
SocketBMain =
� ...
�import qualified A.Server
Main =multi-sharedimport qualified
packagewhere B.Server...
C= {include
serverimpl; include socketimpl}
D= {include
serverimpl;
include�socketimpl}
packagemulti-sharedwhere�
import partial-server;
qualified C.ServerC= {include
include socketimpl-1}
Main == {include
import partial-server;
qualified D.ServerD
include�� socketimpl-1}... qualified C.Server
importMain = import qualified D.Server
package partial-server
where
Socket...
include socketsig��Socketpackage
Serverpartial-server= import wheredata ServerT = ...SocketT...
include socketsig��Server complete-server= �import Socket
packagewhere
data
data ServerT
SocketT==...SocketT...
...�
Socket = open = ...
19
package complete-server where

Server∆ � B1 ⇒ Ξ̃1Main∆ � B1 ⇒ Ξ̃1Server∆∆∆; Ξ∆; Ξ̃pkg � B1 : Ξ1 ∆∆; Ξ̃pkg � B1 : Ξ1

Identity Vari
Identity Con
Identities
Identity
Varia
IdentityCons
Sub
Identity
Identities
ServerPackageIdentity
Names Subst
Module Path Names
PackageNames
Respositorie
Package
PackagePathDefinitions
ModuleNames
Bindings
Package
Respositories
Thinning
Specs
Package
Definitions

Shared Reuse
A

package multi where
SocketA= {include server-linked-1}
B= {include
packagemulti� where server-linked-2} �Bimport server-linked-1}
qualified A.ServerA= {include= {include
import server-linked-2}
qualified B.Server
SocketBMain =
� ...
�import qualified A.Server
Main =multi-sharedimport qualified
packagewhere B.Server...
C= {include
serverimpl; include socketimpl}
D= {include
serverimpl;
include�socketimpl}
packagemulti-sharedwhere�
import partial-server;
qualified C.ServerC= {include
include socketimpl-1}
Main == {include
import partial-server;
qualified D.ServerD
include�� socketimpl-1}... qualified C.Server
importMain = import qualified D.Server
package partial-server
where
Socket...
include socketsig��Socketpackage
Serverpartial-server= import wheredata ServerT = ...SocketT...
include socketsig��Server complete-server= �import Socket
packagewhere
data
data ServerT
SocketT==...SocketT...
...�
Socket = open = ...
19
package complete-server where

Server∆ � B1 ⇒ Ξ̃1Main∆ � B1 ⇒ Ξ̃1Server∆∆∆; Ξ∆; Ξ̃pkg � B1 : Ξ1 ∆∆; Ξ̃pkg � B1 : Ξ1

Identity Vari
Identity Con
Identities
Identity
Varia
IdentityCons
Sub
Identity
Identities
ServerPackageIdentity
Names Subst
Module Path Names
PackageNames
Respositorie
Package
PackagePathDefinitions
ModuleNames
Bindings
Package
Respositories
Thinning
Specs
Package
Definitions

Shared Reuse
A

package multi where
SocketA= {include server-linked-1}
B= {include
packagemulti� where server-linked-2} �Bimport server-linked-1}
qualified A.ServerA= {include= {include
import server-linked-2}
qualified B.Server
SocketBMain =
� ...
�import qualified A.Server
Main =multi-sharedimport qualified
packagewhere B.Server...
C= {include
serverimpl; include socketimpl}
D= {include
serverimpl;
include�socketimpl}
packagemulti-sharedwhere�
import partial-server;
qualified C.ServerC= {include
include socketimpl-1}
Main == {include
import partial-server;
qualified D.ServerD
include�� socketimpl-1}... qualified C.Server
importC
Main = import qualified D.Server
package partial-server where
Socket...
include socketsig��Socketpackage
Serverpartial-server= import wheredata ServerT = ...SocketT...
include socketsig��Server complete-server= �import Socket
packagewhere
data
data ServerT
SocketT==...SocketT...
...�
Socket = open = ...
19
package complete-server where

Server∆ � B1 ⇒ Ξ̃1Main∆ � B1 ⇒ Ξ̃1Server∆∆∆; Ξ∆; Ξ̃pkg � B1 : Ξ1 ∆∆; Ξ̃pkg � B1 : Ξ1

Identity Vari
Identity Con
Identities
Identity
Varia
IdentityCons
Sub
Identity
Identities
ServerPackageIdentity
Names Subst
Module Path Names
PackageNames
Respositorie
Package
PackagePathDefinitions
ModuleNames
Bindings
Package
Respositories
Thinning
Specs
Package
Definitions

Shared Reuse
A

package multi where
SocketA= {include server-linked-1}
B= {include
packagemulti� where server-linked-2} �Bimport server-linked-1}
qualified A.ServerA= {include= {include
import server-linked-2}
qualified B.Server
SocketBMain =
� ...
�import qualified A.Server
Main =multi-sharedimport qualified
packagewhere B.Server...
C= {include
serverimpl; include socketimpl}
D= {include
serverimpl;
include�socketimpl}
packagemulti-sharedwhere�
import partial-server;
qualified C.ServerC= {include
include socketimpl-1}
Main == {include
import partial-server;
qualified D.ServerD
include�� socketimpl-1}... qualified C.Server
importC
Main = import qualified D.Server
package partial-server where
Socket...
include socketsig��Socketpackage
Serverpartial-server= import wheredata ServerT = ...SocketT...
include socketsig�� SocketServer complete-server= �import Socket
packagewhere
data
data ServerT
SocketT==...SocketT...
...�
Socket = open = ...
19
package complete-server where

Server∆ � B1 ⇒ Ξ̃1Main∆ � B1 ⇒ Ξ̃1Server∆∆∆; Ξ∆; Ξ̃pkg � B1 : Ξ1 ∆∆; Ξ̃pkg � B1 : Ξ1

Identity Vari
Identity Con
Identities
Identity
Varia
IdentityCons
Sub
Identity
Identities
ServerPackageIdentity
Names Subst
Module Path Names
PackageNames
Respositorie
Package
ServerPackagePathDefinitions
ModuleNames
Bindings
Package
Respositories
Thinning
Specs
Package
Definitions

Shared Reuse
A

package multi where
SocketA= {include server-linked-1}
B= {include
packagemulti� where server-linked-2} �Bimport server-linked-1}
qualified A.ServerA= {include= {include
import server-linked-2}
qualified B.Server
SocketBMain =
� ...
�import qualified A.Server
Main =multi-sharedimport qualified
packagewhere B.Server...
C= {include
serverimpl; include socketimpl}
D= {include
serverimpl;
include�socketimpl}
packagemulti-sharedwhere�
import partial-server;
qualified C.ServerC= {include
include socketimpl-1}
Main == {include
import partial-server;
qualified D.ServerD
include�� socketimpl-1}... qualified C.Server
importC
Main = import qualified D.Server
package partial-server where
Socket...
include socketsig��Socketpackage
Serverpartial-server= import wheredata ServerT = ...SocketT...
include socketsig�� SocketServer complete-server= �import Socket
packagewhere
data
data ServerT
SocketT==...SocketT...
...�
Socket = open = ...
19
package complete-server where

Server∆ � B1 ⇒ Ξ̃1Main∆ � B1 ⇒ Ξ̃1Server∆∆∆; Ξ∆; Ξ̃pkg � B1 : Ξ1 ∆∆; Ξ̃pkg � B1 : Ξ1

Identity Vari
Identity Con
Identities
Identity
Varia
IdentityCons
Sub
Identity
Identities
ServerPackageIdentity
Names Subst
Module Path Names
PackageNames
Respositorie
Package
ServerPackagePathDefinitions
ModuleNames
Bindings
Package
Respositories
Thinning
Specs
Package
Definitions

Shared Reuse
A

package multi where
SocketA= {include server-linked-1}
B= {include
packagemulti� where server-linked-2} �Bimport server-linked-1}
qualified A.ServerA= {include= {include
import server-linked-2}
qualified B.Server
SocketBMain =
� ...
�import qualified A.Server
Main =multi-sharedimport qualified
packagewhere B.Server...
C= {include
serverimpl; include socketimpl}
D= {include
serverimpl;
include�socketimpl}
packagemulti-sharedwhere�
import partial-server;
qualified C.ServerC= {include
include socketimpl-1}
Main == {include
import partial-server;
qualified D.ServerD
include�� socketimpl-1}... qualified C.Server
importC
Main = import qualified D.Server
package partial-server where
Socket...
include socketsig��Socketpackage
Serverpartial-server= import whereD
data
ServerT=...SocketT...
include socketsig�� SocketServer complete-server= �import Socket
packagewhere
data
data ServerT
SocketT==...SocketT...
...�
Socket = open = ...
19
package complete-server where

Server∆ � B1 ⇒ Ξ̃1Main∆ � B1 ⇒ Ξ̃1Server∆∆∆; Ξ∆; Ξ̃pkg � B1 : Ξ1 ∆∆; Ξ̃pkg � B1 : Ξ1

Identity Vari
Identity Con
Identities
Identity
Varia
IdentityCons
Sub
Identity
Identities
ServerPackageIdentity
Names Subst
Module Path Names
PackageNames
Respositorie
Package
ServerPackagePathDefinitions
ModuleNames
Bindings
Package
Respositories
Thinning
Specs
Package
Definitions

Shared Reuse
A

package multi where
SocketA= {include server-linked-1}
B= {include
packagemulti� where server-linked-2} �Bimport server-linked-1}
qualified A.ServerA= {include= {include
import server-linked-2}
qualified B.Server
SocketBMain =
� ...
�import qualified A.Server
Main =multi-sharedimport qualified
packagewhere B.Server...
C= {include
serverimpl; include socketimpl}
D= {include
serverimpl;
include�socketimpl}
packagemulti-sharedwhere�
import partial-server;
qualified C.ServerC= {include
include socketimpl-1}
Main == {include
import partial-server;
qualified D.ServerD
include�� socketimpl-1}... qualified C.Server
importC
Main = import qualified D.Server
package partial-server where
Socket...
include socketsig��Socketpackage
Serverpartial-server= import whereD
data
ServerT=...SocketT...
include socketsig�� SocketServer complete-server= �import Socket
packagewhere
data
data ServerT
SocketT==...SocketT...
...�
Socket = open = ...
19
package complete-server where

Server∆ � B1 ⇒ Ξ̃1Main∆ � B1 ⇒ Ξ̃1Server∆∆∆; Ξ∆; Ξ̃pkg � B1 : Ξ1 ∆∆; Ξ̃pkg � B1 : Ξ1

Identity Vari
Identity Con
Identities
Identity
Varia
IdentityCons
Sub
Identity
Identities
ServerPackageIdentity
Names Subst
ModuleMain
Path Names
PackageNames
Respositorie
Package
ServerPackagePathDefinitions
ModuleNames
Bindings
Package
Respositories
Thinning
Specs
Package
Definitions

Shared Reuse
A

Server∆ � B1 ⇒ Ξ̃1Main∆ � B1 ⇒ Ξ̃1Server∆∆∆; Ξ∆; Ξ̃pkg � B1 : Ξ1 ∆∆; Ξ̃pkg � B1 : Ξ1

Identity Vari
Identity Con
Identities
Identity
Varia
IdentityCons
Sub
Identity
Identities
ServerPackageIdentity
Names Subst
ModuleMain
Path Names
PackageNames
Respositorie
Package
ServerPackagePathDefinitions
ModuleNames
Bindings
Package
Respositories
Thinning
Specs
Package
Definitions=

package multi where
SocketA= {include server-linked-1}
B= {include
packagemulti� where server-linked-2} �Bimport server-linked-1}
qualified A.ServerA= {include= {include
import server-linked-2}
qualified B.Server
SocketBMain =
� ...
�import qualified A.Server
Main =multi-sharedimport qualified
packagewhere B.Server...
C= {include
serverimpl; include socketimpl}
D= {include
serverimpl;
include�socketimpl}
packagemulti-sharedwhere�
import partial-server;
qualified C.ServerC= {include
include socketimpl-1}
Main == {include
import partial-server;
qualified D.ServerD
include�� socketimpl-1}... qualified C.Server
importC
Main = import qualified D.Server
package partial-server where
Socket...
include socketsig��Socketpackage
Serverpartial-server= import whereD
data
ServerT=...SocketT...
include socketsig�� SocketServer complete-server= �import Socket
packagewhere
data
data ServerT
SocketT==...SocketT...
...�
Socket = open = ...
19
package complete-server whereShared Reuse
A

package multi where
SocketA= {include server-linked-1}
B= {include
packagemulti� where server-linked-2} �Bimport server-linked-1}
qualified A.ServerA= {include= {include
import server-linked-2}
qualified B.Server
SocketBMain =
� ...
�import qualified A.Server
Main =multi-sharedimport qualified
packagewhere B.Server...
C= {include
serverimpl; include socketimpl}
D= {include
serverimpl;
include�socketimpl}
packagemulti-sharedwhere�
import partial-server;
qualified C.ServerC= {include
include socketimpl-1}
Main == {include
import partial-server;
qualified D.ServerD
include�� socketimpl-1}... qualified C.Server
importC
Main = import qualified D.Server
package partial-server where
D Socket...
include socketsig��Socketpackage
Serverpartial-server= import wheredata ServerT = ...SocketT...
include socketsig��Server complete-server= �import Socket
packagewhere
data
data ServerT
SocketT==...SocketT...
...�
Socket = open = ...
19
package complete-server where

Server∆ � B1 ⇒ Ξ̃1Main∆ � B1 ⇒ Ξ̃1Server∆∆∆; Ξ∆; Ξ̃pkg � B1 : Ξ1 ∆∆; Ξ̃pkg � B1 : Ξ1

Identity Vari
Identity Con
Identities
Identity
Varia
IdentityCons
Sub
Identity
Identities
ServerPackageIdentity
Names Subst
ModuleMain
Path Names
PackageNames
Respositorie
Package
PackagePathDefinitions
ModuleNames
Bindings
Package
Respositories
Thinning
Specs
Package
Definitions

ursive modules follows that of MixML.
which effectively explains the macro-levelstructure of thefropa
its dependencies)
definesNormal
two modules,
and B, which
im-recursive
mixinAlinking
ties theknot, ensuring that thei.e., the modules contained in D, thenamesofallandthe stetivatetherole
ard-declaring
the
parts
of
B
that
A
depends
import B actually resolves to the B implementation
inmodules,
the end.and how they all depend on one an
definedinthosesequent subsections e
ion makesGHC
sense—i.e.,
the names
allowsit knows
recursivemodules only
withinasingle(Cabal)The second pass, called typing, augments
thestructural informandelaboration.
Fullmports package.
from B—and,naturally,thesecondBackpack, on the other hand,allowsmore
flexiblerein Ξ̃ with additional information about the micro-level str
ense after
that.
This
definitionisanalogous
cursion. Although packages
themselvesofare
notdefinedrecursively,D.
In
particular,
it fills in the types
en4
3.1of core-language
Module Identi
ould be defined in GHC today.
they may be recursively linked. Consider
the following:
forminga package type Ξ and checking that D is well-formed
5 shows
thethise
Our goal in the present section is Figure
to explainin detailpackage ab-sigs where
package b-from-a whereWeelaboration
proceed bypass typechecking algorithm, as wellcies.
as the
of
A
B
A
::
[S
]
includeab-sigsA...]
first column
pack into Haskell. Central to both passesTheof Backpack
typec
B :: [SB ]B ing= is[import
A;module...] identity. Using...]a notion ofmultinst
packagof thepackagetypes:amits dependencies)
Figure 2 as a running
example,we wipackageknot,
a-from-b
where
ab-rec-sepfrom
wheretheir names
at thelev
ies the recursive
ensuringthat the package
tivate therole and structure of module(i.e.,
identities,
and theniinclude ab-sigs
includea-from-b
the namesof th
es to the B implementationin the end.
sequentb-from-a
subsections explain the implementationof shaping,= within[importB; ...]
includeve modules A
only
a single(Cabal)The reason
for distint
and elaboration. Full details are given in Appendix §6.
the other hand, allows more flexible reidentities is simple:
4 In GHC,are
ges themselves
not definedrecursively,
insteadof explicit
bindings to a signatureand twomodules, there
3.1 Module
Identities
5 The reason for splittin
linked.would
Considerthe twofollowing:
be themodule source files and an additional “boot file” for B
Figure 5Bshowstheshapesand types ofdouble
multinst
andproblem
its depethat
looks
exactlylike
S.
Moreover,theimportwithintheA
modulevisionBrepackage b-from-a where
cies.compiler
We proceedby explaining
5 in a discussion,
left-to-rightasfasw
wouldinclude
include aab-sigs“source pragma” that tells theto import
the boot Figurefurther
The first column of Figure 5 contains
thevision
first keycompfile instead
of
the
full
module.
doublecompares
B = [import A; ...]of package types: a mapping from modules’ logical names p
here
package ab-rec-sep where
A theirA names at the level of Backpack) to their physical ident
include a-from-b(i.e., the names of the Haskell modules to which they elab
5
B The B...]
include b-from-a
reason for distinguishing between
logical names and phidentities is simple: due to aliasing (Section 2.5), there m

Recursive Linking

t bindings to a signature and two modules, there
ource files and an additional “boot file” for B
Moreover, the import B within the A moduleagma” that tells the compiler to import the boot5 The reason for splitting typechecking into two passes has to do w

double vision problem [8], as discussed in Section 2.6. See Sectio
further20discussion, as well as a detailed explanation of how our solu

The second
pass, called
typing,augments the structural iursivefrom
modulesfollows
that of MixML.
packageab-recwhere
ports
B—and,
naturally,
the second
which effectively explains the macro-levelstructure of thefropa
its
dependencies)
definesNormal
two modules,
Alinking
and B, which
im-recursive
mixin
ties
the
knot,
ensuring
that
the
in
Ξ̃
with
additional
information
about
the
micro-leve
B ::contained[SB ] in D, the names of all the ense after that. This definition is analogous
i.e.,
the
modules
tivatetherole and st
ard-declaring
the
parts
of Bresolves
that4A depends
importB
actually
totheB
implementation
in
the
end.
of
D.
In
particular,
it
fills
in
the
types
of
core-languaA=[importB;...]defined in those modules, and how they
all dependon one ane
uld
be definedin GHCittoday.
sequent
subsections
ion makes
sense—i.e.,
knows
the
names
GHC allows recursive modules only
withinapackage
single(Cabal)forming
apass,typeΞ and
D is well-fo
B= [import
A;checking...] thethatThe
secondcalledtyping,augments
structural
informandelaboration.
Fullmportsfrom
B—and,
naturally,thesecond
e
Our
goal
in
the
present
sectionistoexplainindeta
package. Backpack, on the other hand,allowsmore
flexible
rein
Ξ̃
with
additional
information
about
the
micro-level
str
Normalmixin
linkingties
therecursive
knot
ense after
that.
This
definitionisanalogous
pass
typechecking
algorithm,
aswellofascore-language
the elaboratio
cursion. Although packages
themselvesofare
notdefinedrecursively,D.
In
particular,
it
fills
in
the
types
en
4
3.1
ModuleIdentiouldbedefinedin
GHC
today.
importB
actually
resolves
totheB
implementa...] they may be recursively linked. Consider
pack
into
Haskell.
to both passes
Backpack
the following:
forminga package
typeCentral
Ξ and checking
that D ofis well-formed
GHC
recursivemodules
only thewithi...]
Figure5 showss
ing
is goala notion
ofallows
modulesection
identity.
themultinstpae
Ourin thepresent
is Using
to explainin detailthi
package ab-sigs where
packageb-from-awhere
package.
Backpack,
onwell
the
other
hand,
allow
its
dependencies)
fromFigure2asarunning
example,cies.
Weproceedbypass
typechecking
algorithm,
as
as
the
elaborationofw
es the recursive
knot,
ensuring
that
the
A
B
A :: [SA ]includeab-sigs
cursion.
Althoughpackagesthemselvesareandnott...]
tivatetherole
andstructureofmoduleidentities,
The
first
columnpack
into
Haskell.
Centraltobothpassesof
Backpack
typec
s to the B implementationin the end.
B
::
[S
]
B ing
=
[importA;module
...]
B
they
may
be
recursively
linked.
Consider
the
fom
...]
is
a
notionof
identity.
Usingthemultinst
packagsequent
subsections
explainthe
implementation
of
shap
of
packagetypes:
ae modules only within a single (Cabal)
itsanddependencies)
fromFigureas agiven
running
example,wewielaboration.
Fulldetails2whereareAppendix§6.
packagea-from-b
ab-rec-sep
wheretheirinnames
at thelev
ies
the recursive
knot,
ensuringthat thepackageab-sigs
packageb-f
he otherhand, allows
more where
flexiblere- package
tivate therole and structure of module(i.e.,
identities,
and theniincludeincludea-from-b
the names
of ab
th
es to
the B implementationin theend.
A :: [SA ]includethemselves
are notab-sigs
definedrecursively,
3.1 b-from-a
ModuleIdentities
sequent
subsections
explain the implementationof shaping,tA=[importB;...]
includeve
modules
onlywithinasingle(Cabal)The
reasonfor
distinnked. Consider the following:
B Full:: [SB §6.
= [imp
B ] are given in Appendix
andelaboration.
details
the other hand, allows more flexible reidentities
is simple:
Figure 5 shows the shapes and typesof multinst
and its
A
packagebya-from-b
where
packageabe themselvesb-from-awhere
4 Inpackage
A
ges
not
definedrecursively,cies.
We
proceedexplaining
Figure5inaleft-to-righ
GHC,areinsteadof explicit
bindings to a signatureandtwomodules,there
3.1 Module include
Identitiesab-sigs
includeab-sigs
includea5 The reason
linked.would
Considerthefollowing:
be the two module source files andanadditional
“boot
file”
for
B
for
splittinThe
firstcolumnofFigure5contains
the
first
key
B Figure 5 showsAthe=shapes
B problem
and types
ofdouble
multinst
andits depe
B=[importA;...][importB;...]
includebthat
looks
exactlylike
S.
Moreover,theimportB
withintheA
modulevisionofpackagetypes:amapping
frommodules’logicalna
Brepackage b-from-a where
cies.compiler
We proceedby explaining
Figurefurther
5 in a discussion,
left-to-rightasfasw
includea“sourcepragma”
that
tells
the
to
importtheboot
ere would
packageab-rec-sep
wheretheir names at the level of Backpack) to their physicalinclude ab-sigs
The first
columnof Figure5 contains
thevision
first
key
comp
4 In GHC,
file instead
of
the
full
module.
doublecomparesinsteadof
explicit
bindings
toasignatureaincludea-from-b(i.e.,
the
names
of
the
Haskellmodules
to
which
they
B = [import A; ...]of package
types:
athe
mappingfrom source
modules’logical
names
p
would
be
two
modulefiles
andanadditio...]includeab-rec-sep
b-from-a whereThe
reasonat for
distinguishing
betweenlogicalnames
anA nameshere
packageA their
the
level
of
Backpack)totheirphysical
identthat islooks
exactly
like
Saliasingthe importB
B . Moreover,identities
simple:due
to(Section
2.5),
theinclude a-from-b(i.e., the would
namesincludeof the aHaskell
tothat
which
they
elab
“sourcemodules
pragma”
tells
the
compi
5
bindings
signatureb-from-aand two modules, there B The B...] to a include
reasonfor
distinguishing
betweenfile instead of the full module. logical names and ph

Recursive Linking

ource files and an additional “boot file” for B
Moreover,import B
withinthe A module
t bindings tothea signature
andtwo modules,
there
gma”
compiler toimportourcethatfilestells
and thean additional“bootfile”theforboot
Be.Moreover, the import B within the A moduleagma” that tells the compiler to import the boot5 The reason for splitting typechecking into two passes has to

identities is simple: due to aliasing (Section 2.5), there mdouble vision problem [8], as discussed in Section 2.6. See S
5 The
further
discussion,as well
as a detailedof how
reasonfor splitting
typechecking
into explanation
two passes has
to doouw
doublevisioncompares
MixML’s.
doublevisionproblem[8], withas discussed
in Section 2.6. See Sectio

further20discussion, as well as a detailed explanation of how our solu

The second
pass, called
typing,augments the structural iursivefrom
modulesfollows
that of MixML.
packageab-recwhere
ports
B—and,
naturally,
the second
which effectively explains the macro-levelstructure of thefropa
its
dependencies)
definesNormal
two modules,
Alinking
and B, which
im-recursive
mixin
ties
the
knot,
ensuring
that
the
in
Ξ̃
with
additional
information
about
the
micro-leve
B ::contained[SB ] in D, the names of all the ense after that. This definition is analogous
i.e.,
the
modules
tivatetherole and st
ard-declaring
the
parts
of Bresolves
that4A depends
importB
actually
totheB
implementation
in
the
end.
of
D.
In
particular,
it
fills
in
the
types
of
core-languaA=[importB;...]defined in those modules, and how they
all dependon one ane
uld
be definedin GHCittoday.
sequent
subsections
ion makes
sense—i.e.,
knows
the
names
GHC allows recursive modules only
withinapackage
single(Cabal)forming
apass,typeΞ and
D is well-fo
B= [import
A;checking...] thethatThe
secondcalledtyping,augments
structural
informandelaboration.
Fullmportsfrom
B—and,
naturally,thesecond
e
Our
goal
in
the
present
sectionistoexplainindeta
package. Backpack, on the other hand,allowsmore
flexible
rein
Ξ̃
with
additional
information
about
the
micro-level
str
Normalmixin
linkingties
therecursive
knot
ense after
that.
This
definitionisanalogous
pass
typechecking
algorithm,
aswellofascore-language
the elaboratio
cursion. Although packages
themselvesofare
notdefinedrecursively,D.
In
particular,
it
fills
in
the
types
en
4
3.1
ModuleIdentiouldbedefinedin
GHC
today.
importB
actually
resolves
totheB
implementa...] they may be recursively linked. Consider
pack
into
Haskell.
to both passes
Backpack
the following:
forminga package
typeCentral
Ξ and checking
that D ofis well-formed
GHC
recursivemodules
only thewithi...]
Figure5 showss
ing
is goala notion
ofallows
modulesection
identity.
themultinstpae
Ourin thepresent
is Using
to explainin detailthi
package ab-sigs where
packageb-from-awhere
package.
Backpack,
onwell
the
other
hand,
allow
its
dependencies)
fromFigure2asarunning
example,cies.
Weproceedbypass
typechecking
algorithm,
as
as
the
elaborationofw
es the recursive
knot,
ensuring
that
the
A
B
A :: [SA ]includeab-sigs
cursion.
Althoughpackagesthemselvesareandnott...]
tivatetherole
andstructureofmoduleidentities,
The
first
columnpack
into
Haskell.
Centraltobothpassesof
Backpack
typec
s to the B implementationin the end.
B
::
[S
]
B ing
=
[importA;module
...]
B
they
may
be
recursively
linked.
Consider
the
fom
...]
is
a
notionof
identity.
Usingthemultinst
packagsequent
subsections
explainthe
implementation
of
shap
of
packagetypes:
ae modules only within a single (Cabal)
itsanddependencies)
fromFigureas agiven
running
example,wewielaboration.
Fulldetails2whereareAppendix§6.
packagea-from-b
ab-rec-sep
wheretheirinnames
at thelev
ies
the recursive
knot,
ensuringthat thepackageab-sigs
packageb-f
he otherhand, allows
more where
flexiblere- package
tivate therole and structure of module(i.e.,
identities,
and theniincludeincludea-from-b
the names
of ab
th
es to
the B implementationin theend.
A :: [SA ]includethemselves
are notab-sigs
definedrecursively,
3.1 b-from-a
ModuleIdentities
sequent
subsections
explain the implementationof shaping,tA=[importB;...]
includeve
modules
onlywithinasingle(Cabal)The
reasonfor
distinnked. Consider the following:
B Full:: [SB §6.
= [imp
B ] are given in Appendix
andelaboration.
details
the other hand, allows more flexible reidentities
is simple:
Figure 5 shows the shapes and typesof multinst
and its
A
packagebya-from-b
where
packageabe themselvesb-from-awhere
4 Inpackage
A
ges
not
definedrecursively,cies.
We
proceedexplaining
Figure5inaleft-to-righ
GHC,areinsteadof explicit
bindings to a signatureandtwomodules,there
3.1 Module include
Identitiesab-sigs
includeab-sigs
includea5 The reason
linked.would
Considerthefollowing:
be the two module source files andanadditional
“boot
file”
for
B
for
splittinThe
firstcolumnofFigure5contains
the
first
key
B Figure 5 showsAthe=shapes
B problem
and types
ofdouble
multinst
andits depe
B=[importA;...][importB;...]
includebthat
looks
exactlylike
S.
Moreover,theimportB
withintheA
modulevisionofpackagetypes:amapping
frommodules’logicalna
Brepackage b-from-a where
cies.compiler
We proceedby explaining
Figurefurther
5 in a discussion,
left-to-rightasfasw
includea“sourcepragma”
that
tells
the
to
importtheboot
ere would
packageab-rec-sep
wheretheir names at the level of Backpack) to their physicalinclude ab-sigs
The first
columnof Figure5 contains
thevision
first
key
comp
4 In GHC,
file instead
of
the
full
module.
doublecomparesinsteadof
explicit
bindings
toasignatureaincludea-from-b(i.e.,
the
names
of
the
Haskellmodules
to
which
they
B = [import A; ...]of package
types:
athe
mappingfrom source
modules’logical
names
p
would
be
two
modulefiles
andanadditio...]includeab-rec-sep
b-from-a whereThe
reasonat for
distinguishing
betweenlogicalnames
anA nameshere
packageA their
the
level
of
Backpack)totheirphysical
identthat islooks
exactly
like
Saliasingthe importB
B . Moreover,identities
simple:due
to(Section
2.5),
theinclude a-from-b(i.e., the would
namesincludeof the aHaskell
tothat
which
they
elab
“sourcemodules
pragma”
tells
the
compi
5
bindings
signatureb-from-aand two modules, there B The B...] to a include
reasonfor
distinguishing
betweenfile instead of the full module. logical names and ph

Recursive Linking

ource files and an additional “boot file” for B
Moreover,import B
withinthe A module
t bindings tothea signature
andtwo modules,
there
gma”
compiler toimportourcethatfilestells
and thean additional“bootfile”theforboot
Be.Moreover, the import B within the A moduleagma” that tells the compiler to import the boot5 The reason for splitting typechecking into two passes has to

identities is simple: due to aliasing (Section 2.5), there mdouble vision problem [8], as discussed in Section 2.6. See S
5 The
further
discussion,as well
as a detailedof how
reasonfor splitting
typechecking
into explanation
two passes has
to doouw
doublevisioncompares
MixML’s.
doublevisionproblem[8], withas discussed
in Section 2.6. See Sectio

further20discussion, as well as a detailed explanation of how our solu

The second
pass, called
typing,augments the structural iursivefrom
modulesfollows
that of MixML.
packageab-recwhere
ports
B—and,
naturally,
the second
which effectively explains the macro-levelstructure of thefropa
its
dependencies)
definesNormal
two modules,
Alinking
and B, which
im-recursive
mixin
ties
the
knot,
ensuring
that
the
in
Ξ̃
with
additional
information
about
the
micro-leve
B ::contained[SB ] in D, the names of all the ense after that. This definition is analogous
i.e.,
the
modules
tivatetherole and st
ard-declaring
the
parts
of Bresolves
that4A depends
importB
actually
totheB
implementation
in
the
end.
of
D.
In
particular,
it
fills
in
the
types
of
core-languaA=[importB;...]defined in those modules, and how they
all dependon one ane
uld
be definedin GHCittoday.
sequent
subsections
ion makes
sense—i.e.,
knows
the
names
GHC allows recursive modules only
withinapackage
single(Cabal)forming
apass,typeΞ and
D is well-fo
B= [import
A;checking...] thethatThe
secondcalledtyping,augments
structural
informandelaboration.
Fullmportsfrom
B—and,
naturally,thesecond
e
Our
goal
in
the
present
sectionistoexplainindeta
package. Backpack, on the other hand,allowsmore
flexible
rein
Ξ̃
with
additional
information
about
the
micro-level
str
Normalmixin
linkingties
therecursive
knot
ense after
that.
This
definitionisanalogous
pass
typechecking
algorithm,
aswellofascore-language
the elaboratio
cursion. Although packages
themselvesofare
notdefinedrecursively,D.
In
particular,
it
fills
in
the
types
en
4
3.1
ModuleIdentiouldbedefinedin
GHC
today.
importB
actually
resolves
totheB
implementa...] they may be recursively linked. Consider
pack
into
Haskell.
to both passes
Backpack
the following:
forminga package
typeCentral
Ξ and checking
that D ofis well-formed
GHC
recursivemodules
only thewithi...]
Figure5 showss
ing
is goala notion
ofallows
modulesection
identity.
themultinstpae
Ourin thepresent
is Using
to explainin detailthi
package ab-sigs where
packageb-from-awhere
package.
Backpack,
onwell
the
other
hand,
allow
its
dependencies)
fromFigure2asarunning
example,cies.
Weproceedbypass
typechecking
algorithm,
as
as
the
elaborationofw
es the recursive
knot,
ensuring
that
the
A
B
A :: [SA ]includeab-sigs
cursion.
Althoughpackagesthemselvesareandnott...]
tivatetherole
andstructureofmoduleidentities,
The
first
columnpack
into
Haskell.
Centraltobothpassesof
Backpack
typec
s to the B implementationin the end.
B
::
[S
]
B ing
=
[importA;module
...]
B
they
may
be
recursively
linked.
Consider
the
fom
...]
is
a
notionof
identity.
Usingthemultinst
packagsequent
subsections
explainthe
implementation
of
shap
of
packagetypes:
ae modules only within a single (Cabal)
itsanddependencies)
fromFigureas agiven
running
example,wewielaboration.
Fulldetails2whereareAppendix§6.
packagea-from-b
ab-rec-sep
wheretheirinnames
at thelev
ies
the recursive
knot,
ensuringthat thepackageab-sigs
packageb-f
he otherhand, allows
more where
flexiblere- package
tivate therole and structure of module(i.e.,
identities,
and theniincludeincludea-from-b
the names
of ab
th
es to
the B implementationin theend.
A :: [SA ]includethemselves
are notab-sigs
definedrecursively,
3.1 b-from-a
ModuleIdentities
sequent
subsections
explain the implementationof shaping,tA=[importB;...]
includeve
modules
onlywithinasingle(Cabal)The
reasonfor
distinnked. Consider the following:
B Full:: [SB §6.
= [imp
B ] are given in Appendix
andelaboration.
details
the other hand, allows more flexible reidentities
is simple:
Figure 5 shows the shapes and typesof multinst
and its
A
packagebya-from-b
where
packageabe themselvesb-from-awhere
4 Inpackage
A
ges
not
definedrecursively,cies.
We
proceedexplaining
Figure5inaleft-to-righ
GHC,areinsteadof explicit
bindings to a signatureandtwomodules,there
3.1 Module include
Identitiesab-sigs
includeab-sigs
includea5 The reason
linked.would
Considerthefollowing:
be the two module source files andanadditional
“boot
file”
for
B
for
splittinThe
firstcolumnofFigure5contains
the
first
key
B Figure 5 showsAthe=shapes
B problem
and types
ofdouble
multinst
andits depe
B=[importA;...][importB;...]
includebthat
looks
exactlylike
S.
Moreover,theimportB
withintheA
modulevisionofpackagetypes:amapping
frommodules’logicalna
Brepackage b-from-a where
cies.compiler
We proceedby explaining
Figurefurther
5 in a discussion,
left-to-rightasfasw
includea“sourcepragma”
that
tells
the
to
importtheboot
ere would
packageab-rec-sep
wheretheir names at the level of Backpack) to their physicalinclude ab-sigs
The first
columnof Figure5 contains
thevision
first
key
comp
4 In GHC,
file instead
of
the
full
module.
doublecomparesinsteadof
explicit
bindings
toasignatureaincludea-from-b(i.e.,
the
names
of
the
Haskellmodules
to
which
they
B = [import A; ...]of package
types:
athe
mappingfrom source
modules’logical
names
p
would
be
two
modulefiles
andanadditio...]includeab-rec-sep
b-from-a where
Thenames
reasonat for
distinguishing
betweenlogical
names
an
here
package
AAtheir
the
level
of
Backpack)totheirphysical
identthat islooks
exactly
like
Saliasingthe importB
B . Moreover,identities
simple:due
to(Section
2.5),
theinclude a-from-b(i.e., the would
namesincludeof the aHaskell
tothat
which
they
elab
“sourcemodules
pragma”
tells
the
compi
5
bindings
signatureb-from-aand two modules, there
B...] to a include
Thereasonfor
distinguishing
betweenB
file instead of the full module. logical names and ph

Recursive Linking

ource files and an additional “boot file” for B
Moreover,import B
withinthe A module
t bindings tothea signature
andtwo modules,
there
gma”
compiler toimportourcethatfilestells
and thean additional“bootfile”theforboot
Be.Moreover, the import B within the A moduleagma” that tells the compiler to import the boot5 The reason for splitting typechecking into two passes has to

identities is simple: due to aliasing (Section 2.5), there mdouble vision problem [8], as discussed in Section 2.6. See S
5 The
further
discussion,as well
as a detailedof how
reasonfor splitting
typechecking
into explanation
two passes has
to doouw
doublevisioncompares
MixML’s.
doublevisionproblem[8], withas discussed
in Section 2.6. See Sectio

further20discussion, as well as a detailed explanation of how our solu

Backpack Syntax
Package Names
P ∈ PkgNames
Module Path Namesp ∈ ModPaths
Package Respositories R ::= D1 , . . . , Dn
Package Definitions D ::= package P t where B1 , . . . , Bn
Bindings
B ::= p = [M ] | p :: [S] | p = p | include P t r
Thinning Specst ::= (p1 , . . . , pn )Renaming Specsr ::= �p1 �→ p�1 , . . . , pn �→ p�n �Module Expressions M ::= imports; exports; defns
Signature Expressions S ::= imports; decls

interfaces, reuse, and recursive linking

21strong modularity

Backpack Syntax
Package Names
P ∈ PkgNames
Module Path Namesp ∈ ModPaths
Package Respositories R ::= D1 , . . . , Dn
Package Definitions D ::= package P t where B1 , . . . , Bn
Bindings
B ::= p = [M ] | p :: [S] | p = p | include P t r
Thinning Specst ::= (p1 , . . . , pn )Renaming Specsr ::= �p1 �→ p�1 , . . . , pn �→ p�n �Module Expressions M ::= imports; exports; defns
Signature Expressions S ::= imports; decls

interfaces, reuse, and recursive linking

strong modularity

Other features:
Aliasing: module name aliases•

21

Backpack Syntax
Package Names
P ∈ PkgNames
Module Path Namesp ∈ ModPaths
Package Respositories R ::= D1 , . . . , Dn
Package Definitions D ::= package P t where B1 , . . . , Bn
Bindings
B ::= p = [M ] | p :: [S] | p = p | include P t r
Thinning Specst ::= (p1 , . . . , pn )Renaming Specsr ::= �p1 �→ p�1 , . . . , pn �→ p�n �Module Expressions M ::= imports; exports; defns
Signature Expressions S ::= imports; decls

interfaces, reuse, and recursive linking

strong modularity

Other features:
Aliasing: module name aliases
Thinning: control module exposure

•
•

21

Backpack Syntax
Package Names
P ∈ PkgNames
Module Path Namesp ∈ ModPaths
Package Respositories R ::= D1 , . . . , Dn
Package Definitions D ::= package P t where B1 , . . . , Bn
Bindings
B ::= p = [M ] | p :: [S] | p = p | include P t r
Thinning Specst ::= (p1 , . . . , pn )Renaming Specsr ::= �p1 �→ p�1 , . . . , pn �→ p�n �Module Expressions M ::= imports; exports; defns
Signature Expressions S ::= imports; decls

interfaces, reuse, and recursive linking

strong modularity

Other features:
Aliasing: module name aliases
Thinning: control module exposure
Renaming: control module naming/linking

•
•
•

21

Outline• Language tour
• Semantics• Future work

22

Goal 1) Base It on MixML
Start with MixML,** [Rossberg & Dreyer, ICFP ’08]

a minimal, fully expressive core calculus of mixin modules.

23

Goal 1) Base It on MixML
Start with MixML,** [Rossberg & Dreyer, ICFP ’08]

a minimal, fully expressive core calculus of mixin modules.
but MixML
doesn’t reallywork for us:23

Goal 1) Base It on MixML
Start with MixML,** [Rossberg & Dreyer, ICFP ’08]

a minimal, fully expressive core calculus of mixin modules.
but MixML
doesn’t reallywork for us:• MixML targets “LTG”

23Goal 1) Base It on MixML
Start with MixML,** [Rossberg & Dreyer, ICFP ’08]

a minimal, fully expressive core calculus of mixin modules.
but MixML
doesn’t reallywork for us:• MixML targets “LTG”• MixML does not support shared reuse

23Goal 1) Base It on MixML
Start with MixML,** [Rossberg & Dreyer, ICFP ’08]

a minimal, fully expressive core calculus of mixin modules.
but MixML
doesn’t reallywork for us:• MixML targets “LTG”• MixML does not support shared reuse• MixML semantics is pretty complicated23Goal 2) Retrofit Haskell

Because we retrofit,
we must “compile” semantics
down to plain Haskell modules.
24

= {include server-linked-1}= {include
server-linked-2}
��
import qualified A.Server
Main = importqualified B.ServerA
ServerSocket...
A
B

Type Representation
B

Main

package multi whereSocket ServerA= {include server-linked-1}
B= {include
server-linked-2}

import qualified A.Serverimport qualified B.Server






Main = ...
A.Server.ServerT
...






...
B.Server.ServerT ...

package multi-shared where25C= {include partial-server; include socketimpl-1}

= {include server-linked-1}= {include
server-linked-2}
��
import qualified A.Server
Main = importqualified B.ServerA
ServerSocket...
A
B

Type Representation
B

Main

package multi whereSocket ServerA= {include server-linked-1}
B= {include
server-linked-2}

import qualified A.Serverimport qualified B.Server






Main = ...
A.Server.ServerT
...






...
B.Server.ServerT ...

package multi-shared where25C= {include partial-server; include socketimpl-1}

= {include server-linked-1}= {include
server-linked-2}
��
import qualified A.Server
Main = importqualified B.ServerA
ServerSocket...
A
B

Type Representation
Main

B

package multi whereSocket ServerA= {include server-linked-1}
B= {include
server-linked-2}

import qualified A.Serverimport qualified B.Server






ServerMain = Socket...
A.Server.ServerT...

socketimpl-1 partial-serverServer... Socket
B.Server.ServerT...
socketimpl-2

partial-server

package multi-shared where25C= {include partial-server; include socketimpl-1}

∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2

Module Identities∆; Ξ̃pkg � B1 , B2 : Ξ

Identity Variables
Identity Constructors
Identities
Identity SubstitutionsΞ = Ξ1 ⊕ Ξ2 defineα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}26

∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2

Module Identities∆; Ξ̃pkg � B1 , B2 : Ξ

Identity Variables
Identity Constructors
Identities
Identity SubstitutionsΞ = Ξ1 ⊕ Ξ2 defineα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}26

∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2

Module Identities∆; Ξ̃pkg � B1 , B2 : Ξ

Identity Variables
Identity Constructors
Identities
Identity Substitutions

SocketΞ = Ξ1 ⊕ Ξ2 defineα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1) Variables for holes.

Server26∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2

KSock∆; Ξ̃pkg � B1 , B2 : Ξ

ModuleIdentities
alt

K
Sock
Identity Variables

Identity Constructors
KA
Identities
Identity Substitutions
KB

Ξ = Ξ1 ⊕ Ξ2 defineα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1) Variables for holes.

αSock

SocketServerKSer (αSock )KSer (KSock )alt
KSer (KSock )26

14∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2

KSock∆; Ξ̃pkg � B1 , B2 : Ξ

ModuleIdentities
alt

K
Sock
Identity Variables

Identity Constructors
KA
Identities
Identity SubstitutionsKBα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1) Variables for holes.

αSock

SocketΞ = Ξ1 ⊕ Ξ2 define

2) Fresh token applied toimported mod idents.

ServerKSer (αSock )KSer (KSock )alt
KSer (KSock )26

14∆; Ξ̃pkg � B1 : Ξ1∆;
Ξ1 ; Ξ̃pkg � B2 : Ξ2
K
Ser

KSock∆; Ξ̃pkg � B1 , B2 : Ξ

KSock Identities
Module
alt

K
alt
Sock
K
Identity Variables

Sock

Identity Constructors
KAKA
Identities
Identity SubstitutionsK
BKB

α, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1) Variables for holes.

αSock
αSock

SocketServerΞ = Ξ1 ⊕ Ξ2 define

2) Fresh token applied toimported mod idents.

K(α)
Ser (αSock
KSer
)
Sock

KSer (KSock )KSer (KSock )alt
KSer (Kalt Sock )KSer (KSock )

14
26

14

∆; Ξ̃pkg � B1 : Ξ1∆;
Ξ1 ; Ξ̃pkg � B2 : Ξ2
K
Ser

KSock∆; Ξ̃pkg � B1 , B2 : Ξ

KSock Identities
Module
alt

K
alt
Sock
K
Identity Variables

Sock

Identity Constructors
KAKA
Identities
Identity SubstitutionsK
BKB

α, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1) Variables for holes.

αSock
αSock

SocketServerΞ = Ξ1 ⊕ Ξ2 define

2) Fresh token applied toimported mod idents.

K(α)
Ser (αSock
KSer
)
Sock

3) Linking is substitution.

KSer (KSock )KSer (KSock )alt
KSer (Kalt Sock )KSer (KSock )

14
26

14

∆; Ξ̃pkg � B1 : Ξ1 K∆;
Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ser
KSer
KSock∆; Ξ̃pkg � B1 , B2 : Ξ
KSock
KSock
alt

Module Identities

alt
KSock

KA
KB

αSock
νSocketSock
KSer (αSock )KSer (νSock )

K
alt
Sock
K
Identity Variables

Sock

Identity Constructors
KAKA
Identities
Identity SubstitutionsK
BKB

α, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1) Variables for holes.

αSock
αSock

ServerΞ = Ξ1 ⊕ Ξ2 define

2) Fresh token applied toimported mod idents.

K(α)
Ser (αSock
KSer
)
Sock

3) Linking is substitution.

KSer (KSock )KSer (KSock )alt
KSer (Kalt Sock )KSer (KSock )

14

14
26

14

KSockSock∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
KSer
altK
A Ξ̃pkg � B1 , B2 : Ξ
KSock∆;

KSock
alt
KSock

KA
KB

Module Identities

K
B
K
A
Identity Variables
Identity Constructors
KαBSock

Identities
Identity Substitutions
νSock

αSock
νSocketSock
KSer (αSock )KSer (νSock )Server

αSock
KνSer
(α
)
Sock
Sock

Ξ = Ξ1 ⊕ Ξ2 defineα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1) Variables for holes.

2) Fresh token applied toimported mod idents.

K(α)
Ser (νSock
KSer
)
Sock

3) Linking is substitution.

KSer (νSock )

1
14

26

14

KSockSock∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
KSer
altK
A Ξ̃pkg � B1 , B2 : Ξ
KSock∆;

KSock
alt
KSock

KA
KB

Module Identities

K
B
K
A
Identity Variables
Identity Constructors
KαBSock

Identities
Identity Substitutions
νSock

αSock
νSocketSock
KSer (αSock )ServerKSer (νSock )
A
B

αSock
KνSer
(α
)
Sock
Sock

Ξ = Ξ1 ⊕ Ξ2 defineα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1) Variables for holes.

2) Fresh token applied toimported mod idents.

K(α)
Ser (νSock
KSer
)
Sock

3) Linking is substitution.

KSer (νSock )4) μ-binders for cyclic
graphs (recursion).
14

26

1

14

Sock
K
Sock
ncludeinclude∆; Ξ̃serverimpl∆; Ξ1 ; Ξ̃pkg
� B2 :serverimpl
Ξ2
Ξ = Ξ1 ⊕ Ξ2 definepkg � B1 : Ξ1
KSersocketimpl alt
ncludeincludesocketimpl-alt
K
A
KSock∆; Ξ̃pkg � B1 , B2 : Ξ

KSock
alt
KSock

KA
KB

Module Identities

K
B
K
A
Identity Variables
KSer
Identity Constructors
KαBSock

KA
Identities
Identity Substitutions
νSock

αSock
νSocketSock
KSer (αSock )ServerKSer (νSock )A
B

αSock KB
KνSer
(α
)
Sock
Sock αα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1) Variables for holes.

2) Fresh token applied toimported mod idents.

α

K(α
)
Ser (νSock
KSer
)
KSock
Ser (α)3) Linking is substitution.

KSer(νSock) B (α))µα.K
A (K4) μ-binders for cyclic
graphs (recursion).

µα.KB (KA (α))
KB (αA )KA (αB ) 26

14

1

14

Sock
K
Sock
ncludeinclude∆; Ξ̃serverimpl∆; Ξ1 ; Ξ̃pkg
� B2 :serverimpl
Ξ2
Ξ = Ξ1 ⊕ Ξ2 definepkg � B1 : Ξ1
KSersocketimpl alt
ncludeincludesocketimpl-alt
K
A
KSock∆; Ξ̃pkg � B1 , B2 : Ξ

KSock
alt
KSock

KA
KB

Module Identities

K
B
K
A
Identity Variables
KSer
Identity Constructors
KαBSock

KA
Identities
Identity Substitutions
νSock

αSock
νSocketSock
KSer (αSock )ServerKSer (νSock )A
B

αSock KB
KνSer
(α
)
Sock
Sock αα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1) Variables for holes.

2) Fresh token applied toimported mod idents.

α

K(α
)
Ser (νSock
KSer
)
KSock
Ser (α)3) Linking is substitution.

KSer(νSock) B (α))µα.K
A (K4) μ-binders for cyclic
graphs (recursion).

µα.KB (KA (α))
KB (αA )KA (αB ) 26

14

1

14

Sock
K
Sock
ncludeinclude∆; Ξ̃serverimpl∆; Ξ1 ; Ξ̃pkg
� B2 :serverimpl
Ξ2
Ξ = Ξ1 ⊕ Ξ2 definepkg � B1 : Ξ1
KSersocketimpl alt
ncludeincludesocketimpl-alt
K
A
KSock∆; Ξ̃pkg � B1 , B2 : Ξ

KSock
alt
KSock

KA

Module Identities

K
B
K
A
Identity Variables
KSer
Identity Constructors
KαBSock

KA
Identities
Identity Substitutions
νSock

KB

αSock
νSocketSock
KSer (αSock )ServerKSer (νSock )A
B

αSock KB
KνSer
(α
)
Sock
Sock αα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1) Variables for holes.

2) Fresh token applied toimported mod idents.

α

K(α
)
Ser (νSock
KSer
)
KSock
Ser (α)3) Linking is substitution.

KSer(νSock) B (α))µα.K
A (K4) μ-binders for cyclic
graphs (recursion).

µα.KB (KA (α))
14KB (αsharedA)
module identities enable
reuse and recursive linking!
KA (αB ) 26

1

14

module identity

Type System27

module identity

Type System

Elaboration

27

Type System(two passes on a package)1) Shaping• Determine

structure ofmodules and code

• Synthesize module
identities

28

Type System(two passes on a package)1) Shaping• Determine

structure ofmodules and code

2) Typing• Do Haskell• Synthesize module
identities•
28

typechecking
Augment shapes with
Haskell typing
information

µα.KA (KB (α))
KB (αA )µα.KB (KA (α))
KA (αB )KB (αA )alt
KMain (KSer (KSock ), KSer (KSock ))KA (αB )Type System: Linking∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒(SΞ̃H S EQ)(S H S EQ)∆ � B1 , B2 ⇒ Ξ̃∆ � B1 , B2 ⇒ Ξ̃∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ1 ⊕ Ξ2 = Ξ defined∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ = Ξ1 ⊕ Ξ2 defined(T Y S EQ)(T Y S EQ)∆; Ξ̃pkg � B1 , B2 : Ξ∆; Ξ̃pkg � B1 , B2 : Ξ
Identity Variables
Identity Constructors
Identities
Identity Substitutionsα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1429

µα.KA (KB (α))
KB (αA )µα.KB (KA (α))
KA (αB )KB (αA )alt
KMain (KSer (KSock ), KSer (KSock ))KA (αB )Type System: Linking∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒(SΞ̃H S EQ)(S H S EQ)∆ � B1 , B2 ⇒ Ξ̃∆ � B1 , B2 ⇒ Ξ̃∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ1 ⊕ Ξ2 = Ξ defined∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ = Ξ1 ⊕ Ξ2 defined(T Y S EQ)(T Y S EQ)∆; Ξ̃pkg � B1 , B2 : Ξ∆; Ξ̃pkg � B1 , B2 : Ξ
Identity Variables
Identity Constructors
Identities
Identity Substitutionsα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1429

µα.KA (KB (α))
KB (αA )µα.KB (KA (α))
KA (αB )KB (αA )alt
KMain (KSer (KSock ), KSer (KSock ))KA (αB )Type System: Linking∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒(SΞ̃H S EQ)(S H S EQ)∆ � B1 , B2 ⇒ Ξ̃∆ � B1 , B2 ⇒ Ξ̃∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ1 ⊕ Ξ2 = Ξ defined∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ = Ξ1 ⊕ Ξ2 defined(T Y S EQ)(T Y S EQ)∆; Ξ̃pkg � B1 , B2 : Ξ∆; Ξ̃pkg � B1 , B2 : Ξ
Identity Variables
Identity Constructors
Identities
Identity Substitutionsα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1429

µα.KA (KB (α))
KB (αA )µα.KB (KA (α))
KA (αB )KB (αA )alt
KMain (KSer (KSock ), KSer (KSock ))KA (αB )Type System: Linking∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒(SΞ̃H S EQ)(S H S EQ)∆ � B1 , B2 ⇒ Ξ̃∆ � B1 , B2 ⇒ Ξ̃∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ1 ⊕ Ξ2 = Ξ defined∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ = Ξ1 ⊕ Ξ2 defined(T Y S EQ)(T Y S EQ)∆; Ξ̃pkg � B1 , B2 : Ξ∆; Ξ̃pkg � B1 , B2 : Ξ
Identity Variables
Identity Constructors
Identities
Identity Substitutionsα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1429

µα.KA (KB (α))
KB (αA )µα.KB (KA (α))
KA (αB )KB (αA )alt
KMain (KSer (KSock ), KSer (KSock ))KA (αB )Type System: Linking
unification!

∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒(SΞ̃H S EQ)(S H S EQ)∆ � B1 , B2 ⇒ Ξ̃∆ � B1 , B2 ⇒ Ξ̃∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ1 ⊕ Ξ2 = Ξ defined∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ = Ξ1 ⊕ Ξ2 defined(T Y S EQ)(T Y S EQ)∆; Ξ̃pkg � B1 , B2 : Ξ∆; Ξ̃pkg � B1 , B2 : Ξ
Identity Variables
Identity Constructors
Identities
Identity Substitutionsα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1429

µα.KA (KB (α))
KB (αA )µα.KB (KA (α))
KA (αB )KB (αA )alt
KMain (KSer (KSock ), KSer (KSock ))KA (αB )Type System: Linking∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒(SΞ̃H S EQ)(S H S EQ)∆ � B1 , B2 ⇒ Ξ̃∆ � B1 , B2 ⇒ Ξ̃∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ1 ⊕ Ξ2 = Ξ defined∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ = Ξ1 ⊕ Ξ2 defined(T Y S EQ)(T Y S EQ)∆; Ξ̃pkg � B1 , B2 : Ξ∆; Ξ̃pkg � B1 , B2 : Ξ
Identity Variables
Identity Constructors
Identities
Identity Substitutionsα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1429

µα.KA (KB (α))
KB (αA )µα.KB (KA (α))
KA (αB )KB (αA )alt
KMain (KSer (KSock ), KSer (KSock ))KA (αB )Type System: Linking∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃∆ � B1 ⇒ Ξ̃1 ∆; Ξ̃1 � B2 ⇒ Ξ̃2
� Ξ̃1 + Ξ̃2 ⇒(SΞ̃H S EQ)(S H S EQ)∆ � B1 , B2 ⇒ Ξ̃∆ � B1 , B2 ⇒ Ξ̃∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ1 ⊕ Ξ2 = Ξ defined∆; Ξ̃pkg � B1 : Ξ1∆; Ξ1 ; Ξ̃pkg � B2 : Ξ2
Ξ = Ξ1 ⊕ Ξ2 defined(T Y S EQ)(T Y S EQ)∆; Ξ̃pkg � B1 , B2 : Ξ∆; Ξ̃pkg � B1 , B2 : Ξ
Identity Variables
Identity Constructors
Identities
Identity Substitutionsα, β ∈ IdentVars
K ∈ IdentCtors
ν ::= α | K ν | µα.νφ, θ ::= {α := ν}1429

µα.KA (KB (α))
Modules: Γ; R; β � mod : Σ KB (αA )µα.KB (KA (α))
X : |Σ| ∈ ΓKA (αB )
(KVAR
(EMP)
B (α)A )alt
Γ; K{||}Main; ∅ (K�X: |Σ|Γ; {||}; ∅ � {} : {||}Ser (KSock ), KSer (KSock ))KA (αB )� A ⇑ knd
Γ � typ ❀ A(ITYP)� Ξ̃1 + Ξ̃2 ⇒ Ξ̃(ETYP)
∆ Γ;
�B
⇒
Ξ̃
∆;
Ξ̃
�
B
⇒
Ξ̃
1
1
1
2
2
[[=�A]];� Ξ̃[:knd] :Ξ̃[[=A]]; ∅Ξ̃�2 [typ][[=) A]]∆
B1∅⇒∆;
�Γ;Ξ̃{1||}+⇒(SΞ̃H S:EQ
1
1 � B2 ⇒ Ξ̃2(S H S EQ)∆ � B1 , B2 ⇒ Ξ̃∆ � B1 , B2 ⇒ Ξ̃Γ � exp : A� A ⇑ typeΓ � typ ❀ A
� A ⇑ type
(IVAL)(EVAL)∆;Γ;Ξ̃{pkg
�
B
∆;
Ξ
Ξ
−1 ; Ξ̃pkg � B2 : Ξ2
1 : Ξ11 ⊕ Ξ2 = Ξ defined +||};Ξ̃∅pkg
� [:typ]; ∅=� Ξ[exp]∆;� B1 : Ξ: 1[[A]] ∆; Ξ1 ; Ξ̃pkg � B2 : ΞΓ;
defined(T Y S EQ)
2 {||}Ξ
1 ⊕ Ξ2: [[A]](T Y S EQ)∆; Ξ̃pkg � B1 , B2 : Ξ∆; Ξ̃pkg � B1 , B2 : Ξ
Γ; {|� : R|}; β � mod : {|� : Σ, �� : |Σ� ||}Γ; R; β � mod : Σ
(α,
STR
(DOT)
Identity Variablesβ )∈ IdentVars
Γ; {|� : R|}; β �Identity{� = mod} : {|� : Σ|}Constructors
K ∈ IdentCtorsΓ; R; β � mod .� : Σ
Identitiesν ::= α | K ν | µα.ν
� L1 locates
α1 Substitutions
R1 # Σ2:=Rν}� R1 � L1 ; β1 � mod 1 : Σ1
Identityφ, θ ::= {αΓ;� L2 locates α2
R2 # Σ1
Γ, X : |Σ1 |; R � R2 � L2 ; β2 �stat mod 2 : Σ�2
� (L1 ; Σ1 ) � (L2 ; Σ�2 ) ❀ δΓ, X : |δΣ1 |; R � R2 � δL2 ; β2 � mod 2 : Σ2
α1 , α2 fresh� δΣ1 + Σ2 ⇒ Σ(LINK)
Γ; R � R1 � R2 ; β1 , β2 � (X = mod 1 ) with mod 2 : Σ 14

Type System: Linking

Backpack
MixML

� L1 locates α1
� L2 locates α2

Γ; L1 ; β1 � mod 1 : Σ1
Γ, 29
X : |Σ1 |; L2 ; β2 �stat mod 2 : Σ�packageserver-linked
where
packageserver-linked-alt where
Socket =[data]
SocketT=...
importSocketpackageserverwhere
KSer �
ver server
=
�
age
where
packageserverwhere
Server=[Server.hs]
includeserverimpl
includeserverimpl
data ServerT= ...SocketT...
packageserver-linked
where
packageserver-linked-alt
Socket=[importSocketdata
SocketT= ...] where
Server=cket = [data SocketT]serverimpl
Socket=socketimpl[data SocketT =� ...
]
= ...
�
includeincludesocketimpl-alt
K
includeincludeserverimpl
Sock
data
ServerT=...SocketT...
� package� serverimpl
�
importSocketwhere
ge server�importwhere Socket
Server=importSocketincludesocketimpl
includesocketimpl-alt
alt = ...SocketT...
ver=
Server=data
ServerT
includesocketsig
ket = [Socket.hs]
KpackagewhereServerT = ...SocketT...
Sockdata ServerT= server...SocketT...
data
KSer
Server=[...] wherever = [Server.hs]Socket = [Socket.hs]
package serverimpl
KA
age serverimpl
where
packagewhere KSer
A
Server serverimpl= [Server.hs]
include socketsigKSockge serverimpl
where
lude
socketsig
includesocketsig
packageserver-linked
where package server-linked-alt whe
ServerSocketKB
KSock
Server =
[...]
ver =
[...]
ude
socketsig
Server serverimpl= [...] include
include serverimpl
packagewhere serverimpl
KA
alt
Main
B
ver = [...]
includesocketimpl
includeserver-linked-alt
socketimpl-alt wheK
α package
include socketsig
Sockpackage server-linked
where
age server-linked
where
packageserver-linked-alt
packageserver-linked
where Kpackage
Bwhere server-linked-alt where
ServerSocketServer= [...]
include serverimpl
include serverimpl
K
A
K
(α)
lude
serverimpl
includeserverimpl
includeserverimpl
include serverimpl
ge server-linked where
packageserver-linked-alt whereSer
includesocketimpl
include socketimpl-alt
α
K
Ser
lude
socketimpl
includesocketimpl-alt
includesocketimpl
includeserver-linked-alt
socketimpl-alt whereude serverimpl package
includeserverimpl
server-linked
where KBpackage
KSer (KSock )ude socketimpl
socketimpl-alt
includeinclude
serverimpl
include serverimpl
KSer (α)
KSockα include K
K(KSeralt )includesocketimpl
socketimpl-alt
KSer
K
Ser
alt Sock
module KSerSer(KSock ) where KSock
KSer
KSer (α)
K
Sockmodule KSock
where
µα.K
import KSock as Socket(SockT)
A (KB (α))µα.K
(KB (α))KA
ASerK
data K
SockT
data K
ServerT
Ser (KSock=) ...SockT...
Sock = ...
A (α))µα.KBK(K
KA
KA
A
µα.K
(K
(α))
KB
B alt
A
KSock
alt
modulewhere
K(K)
module KSock where
Ser
B )
KB
KBK(α
KaltB Sock
A
K
(α
)
α
data SockT = ...
BA
importas
Socket(SockT)
Sock
µα.K
(K
(α))
A
B
K
αA
KAα
(αB )
α
data ServerT=...SockT...
KKAA(αB )KSer (α)
µα.K
(K
(α))
B
A
K
KSer (α)
BaltKSer (α)K(α)
Ser
module KMain (KSer (KSock ), KSer (KSock)) where
K
(K
)
K
Ser
Sock
B
K
(α
)
B
A
α
K
(K
) asΞ̃A.Server(ServerT)
importqualified
Ser + Ξ̃
Sock⇒
K
)
∆Ser
�(K
BSock
⇒
Ξ̃
∆;
Ξ̃
�
B
⇒
Ξ̃
�
Ξ̃
K
(K
)
1
1
1 Ser 2 Sock 2
1
alt2(S H S EQ)
αKSer (KSock ) as B.Server(ServerT)
K
importA (αqualified
B)K(α)⇒1 ,AΞ̃B∆;
� B2A (K⇒ BΞ̃(α))
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 B
12 ⇒
2
Ξ̃Ξ̃1µα.Kµα.KASer(KB (α)) ∆ �∆B�
µα.K
(K
(α))
B
(S H
...
KSer (α) ∆ �µα.K
(K
(α))
A
B
B1 , BΞ̃
2 ⇒KSer (K
)
µα.K
(K
(α))
Sock
B
A
µα.K
(K
(α))
30 (α))B2(K∆ ˜B� BA1 ⇒ Ξ̃1 ∆; Ξ̃µα.K� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 � B
˜ ⇒A Ξ̃2

Elaboration

packageserver-linked
where
packageserver-linked-alt where
Socket =[data]
SocketT=...
importSocketpackageserverwhere
KSer �
ver server
=
�
age
where
packageserverwhere
Server=[Server.hs]
includeserverimpl
includeserverimpl
data ServerT= ...SocketT...
packageserver-linked
where
packageserver-linked-alt
Socket=[importSocketdata
SocketT= ...] where
Server=cket = [data SocketT]serverimpl
Socket=socketimpl[data SocketT =� ...
]
= ...
�
includeincludesocketimpl-alt
K
includeincludeserverimpl
Sock
data
ServerT=...SocketT...
� package� serverimpl
�
importSocketwhere
ge server�importwhere Socket
Server=importSocketincludesocketimpl
includesocketimpl-alt
alt = ...SocketT...
ver=
Server=data
ServerT
includesocketsig
ket = [Socket.hs]
KpackagewhereServerT = ...SocketT...
Sockdata ServerT= server...SocketT...
data
KSer
Server=[...] wherever = [Server.hs]Socket = [Socket.hs]
package serverimpl
KA
age serverimpl
where
packagewhere KSer
A
Server serverimpl= [Server.hs]
includesocketsig
KOne
modulefile
peridentity
Sockge serverimpl
where
lude
socketsig
includesocketsig
packageserver-linked
where
packageserver-linked-alt whe
ServerSocketKB
KSock
Server =
[...]
ver =
[...]
ude
socketsig
Server serverimpl= [...] include
include serverimpl
packagewhere serverimpl
KA
alt
Main
B
ver = [...]
includesocketimpl
includeserver-linked-alt
socketimpl-alt wheK
α package
include socketsig
Sockpackage server-linked
where
age server-linked
where
packageserver-linked-alt
packageserver-linked
where Kpackage
Bwhere server-linked-alt where
ServerSocketServer= [...]
include serverimpl
include serverimpl
K
A
K
(α)
lude
serverimpl
includeserverimpl
includeserverimpl
include serverimpl
ge server-linked where
packageserver-linked-alt whereSer
includesocketimpl
include socketimpl-alt
α
K
Ser
lude
socketimpl
includesocketimpl-alt
includesocketimpl
includeserver-linked-alt
socketimpl-alt whereude serverimpl package
includeserverimpl
server-linked
where KBpackage
KSer (KSock )ude socketimpl
socketimpl-alt
includeinclude
serverimpl
include serverimpl
KSer (α)
KSockα include K
K(KSeralt )includesocketimpl
socketimpl-alt
KSer
K
Ser
alt Sock
module KSerSer(KSock ) where KSock
KSer
KSer (α)
K
Sockmodule KSock
where
µα.K
import KSock as Socket(SockT)
A (KB (α))µα.K
(KB (α))KA
ASerK
data K
SockT
data K
ServerT
Ser (KSock=) ...SockT...
Sock = ...
A (α))µα.KBK(K
KA
KA
A
µα.K
(K
(α))
KB
B alt
A
KSock
alt
modulewhere
K(K)
module KSock where
Ser
B )
KB
KBK(α
KaltB Sock
A
K
(α
)
α
data SockT = ...
BA
importas
Socket(SockT)
Sock
µα.K
(K
(α))
A
B
K
αA
KAα
(αB )
α
data ServerT=...SockT...
KKAA(αB )KSer (α)
µα.K
(K
(α))
B
A
K
KSer (α)
BaltKSer (α)K(α)
Ser
module KMain (KSer (KSock ), KSer (KSock)) where
K
(K
)
K
Ser
Sock
B
K
(α
)
B
A
α
K
(K
) asΞ̃A.Server(ServerT)
importqualified
Ser + Ξ̃
Sock⇒
K
)
∆Ser
�(K
BSock
⇒
Ξ̃
∆;
Ξ̃
�
B
⇒
Ξ̃
�
Ξ̃
K
(K
)
1
1
1 Ser 2 Sock 2
1
alt2(S H S EQ)
αKSer (KSock ) as B.Server(ServerT)
K
importA (αqualified
B)K(α)⇒1 ,AΞ̃B∆;
� B2A (K⇒ BΞ̃(α))
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 B
12 ⇒
2
Ξ̃Ξ̃1µα.Kµα.KASer(KB (α)) ∆ �∆B�
µα.K
(K
(α))
B
(S H
...
KSer (α) ∆ �µα.K
(K
(α))
A
B
B1 , BΞ̃
2 ⇒KSer (K
)
µα.K
(K
(α))
Sock
B
A
µα.K
(K
(α))
30 (α))B2(K∆ ˜B� BA1 ⇒ Ξ̃1 ∆; Ξ̃µα.K� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 � B
˜ ⇒A Ξ̃2

Elaboration•

packageserver-linked
where
packageserver-linked-alt where
Socket =[data]
SocketT=...
importSocketpackageserverwhere
KSer �
ver server
=
�
age
where
packageserverwhere
Server=[Server.hs]
includeserverimpl
includeserverimpl
data ServerT= ...SocketT...
packageserver-linked
where
packageserver-linked-alt
Socket=[importSocketdata
SocketT= ...] where
Server=cket = [data SocketT]serverimpl
Socket=socketimpl[data SocketT =� ...
]
= ...
�
includeincludesocketimpl-alt
K
includeincludeserverimpl
Sock
data
ServerT=...SocketT...
� package� serverimpl
�
importSocketwhere
ge server�importwhere Socket
Server=importSocketincludesocketimpl
includesocketimpl-alt
alt = ...SocketT...
ver=
Server=data
ServerT
includesocketsig
ket = [Socket.hs]
KpackagewhereServerT = ...SocketT...
Sockdata ServerT= server...SocketT...
data
KSer
Server=[...] wherever = [Server.hs]Socket = [Socket.hs]
package serverimpl
KA
age serverimpl
where
packagewhere KSer
A
Server serverimpl= [Server.hs]
includesocketsig
KOne
modulefile
peridentity
Sockge serverimpl
where
lude
socketsig
includesocketsig
packageserver-linked
where
packageserver-linked-alt whe
ServerSocketKB
KSock
Server =
[...]
ver =
[...]
ude
socketsig
Server serverimpl= [...] include
serverimpl
serverimpl
packagewhere
KA duplicated (ainclude
Code
la
C++
templates)
alt
Main
B
ver = [...]
includeserver-linked
socketimpl
includeserver-linked-alt
socketimpl-alt wheKSockα package
include socketsig
packagewhere
age server-linked
where
packageserver-linked-alt
packageserver-linked
where Kpackage
Bwhere server-linked-alt where
ServerSocketServer= [...]
include serverimpl
include serverimpl
K
A
K
(α)
lude
serverimpl
includeserverimpl
includeserverimpl
include serverimpl
ge server-linked where
packageserver-linked-alt whereSer
includesocketimpl
include socketimpl-alt
α
K
Ser
lude
socketimpl
includesocketimpl-alt
includesocketimpl
includeserver-linked-alt
socketimpl-alt whereude serverimpl package
includeserverimpl
server-linked
where KBpackage
KSer (KSock )ude socketimpl
socketimpl-alt
includeinclude
serverimpl
include serverimpl
KSer (α)
KSockα include K
K(KSeralt )includesocketimpl
socketimpl-alt
KSer
K
Ser
alt Sock
module KSerSer(KSock ) where KSock
KSer
KSer (α)
K
Sockmodule KSock
where
µα.K
import KSock as Socket(SockT)
A (KB (α))µα.K
(KB (α))KA
ASerK
data K
SockT
data K
ServerT
Ser (KSock=) ...SockT...
Sock = ...
A (α))µα.KBK(K
KA
KA
A
µα.K
(K
(α))
KB
B alt
A
KSock
alt
modulewhere
K(K)
module KSock where
Ser
B )
KB
KBK(α
KaltB Sock
A
K
(α
)
α
data SockT = ...
BA
importas
Socket(SockT)
Sock
µα.K
(K
(α))
A
B
K
αA
KAα
(αB )
α
data ServerT=...SockT...
KKAA(αB )KSer (α)
µα.K
(K
(α))
B
A
K
KSer (α)
BaltKSer (α)K(α)
Ser
module KMain (KSer (KSock ), KSer (KSock)) where
K
(K
)
K
Ser
Sock
B
K
(α
)
B
A
α
K
(K
) asΞ̃A.Server(ServerT)
importqualified
Ser + Ξ̃
Sock⇒
K
)
∆Ser
�(K
BSock
⇒
Ξ̃
∆;
Ξ̃
�
B
⇒
Ξ̃
�
Ξ̃
K
(K
)
1
1
1 Ser 2 Sock 2
1
alt2(S H S EQ)
αKSer (KSock ) as B.Server(ServerT)
K
importA (αqualified
B)K(α)⇒1 ,AΞ̃B∆;
� B2A (K⇒ BΞ̃(α))
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 B
12 ⇒
2
Ξ̃Ξ̃1µα.Kµα.KASer(KB (α)) ∆ �∆B�
µα.K
(K
(α))
B
(S H
...
KSer (α) ∆ �µα.K
(K
(α))
A
B
B1 , BΞ̃
2 ⇒KSer (K
)
µα.K
(K
(α))
Sock
B
A
µα.K
(K
(α))
30 (α))B2(K∆ ˜B� BA1 ⇒ Ξ̃1 ∆; Ξ̃µα.K� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 � B
˜ ⇒A Ξ̃2

Elaboration••

packageserver-linked
where
packageserver-linked-alt where
Socket =[data]
SocketT=...
importSocketpackageserverwhere
KSer �
ver server
=
�
age
where
packageserverwhere
Server=[Server.hs]
includeserverimpl
includeserverimpl
data ServerT= ...SocketT...
packageserver-linked
where
packageserver-linked-alt
Socket=[importSocketdata
SocketT= ...] where
Server=cket = [data SocketT]serverimpl
Socket=socketimpl[data SocketT =� ...
]
= ...
�
includeincludesocketimpl-alt
K
includeincludeserverimpl
Sock
data
ServerT=...SocketT...
� package� serverimpl
�
importSocketwhere
ge server�importwhere Socket
Server=importSocketincludesocketimpl
includesocketimpl-alt
alt = ...SocketT...
ver=
Server=data
ServerT
includesocketsig
ket = [Socket.hs]
KpackagewhereServerT = ...SocketT...
Sockdata ServerT= server...SocketT...
data
KSer
Server=[...] wherever = [Server.hs]Socket = [Socket.hs]
package serverimpl
KA
age serverimpl
where
packagewhere KSer
A
Server serverimpl= [Server.hs]
includesocketsig
KOne
modulefile
peridentity
Sockge serverimpl
where
lude
socketsig
includesocketsig
packageserver-linked
where
packageserver-linked-alt whe
ServerSocketKB
KSock
Server =
[...]
ver =
[...]
ude
socketsig
Server serverimpl= [...] include
serverimpl
serverimpl
packagewhere
KA duplicated (ainclude
Code
la
C++
templates)
alt
Main
B
ver = [...]
includeserver-linked
socketimpl
includeserver-linked-alt
socketimpl-alt wheKSockα package
include socketsig
package
where
Kpackage
age server-linked
where
packageserver-linked-alt
packageserver-linked
whereserver-linked-alt
where
BwhereServerCodelargelypreserved
SocketServer= [...]
includeserverimpl
includeserverimpl
K
A
K
(α)
lude
serverimpl
includeserverimpl
includeserverimpl
include serverimpl
ge server-linked where
packageserver-linked-alt whereSer
includesocketimpl
include socketimpl-alt
α
K
Ser
lude
socketimpl
includesocketimpl-alt
includesocketimpl
includeserver-linked-alt
socketimpl-alt whereude serverimpl package
includeserverimpl
server-linked
where KBpackage
KSer (KSock )ude socketimpl
socketimpl-alt
includeinclude
serverimpl
include serverimpl
KSer (α)
KSockα include K
K(KSeralt )includesocketimpl
socketimpl-alt
KSer
K
Ser
alt Sock
module KSerSer(KSock ) where KSock
KSer
KSer (α)
K
Sockmodule KSock
where
µα.K
import KSock as Socket(SockT)
A (KB (α))µα.K
(KB (α))KA
ASerK
data K
SockT
data K
ServerT
Ser (KSock=) ...SockT...
Sock = ...
A (α))µα.KBK(K
KA
KA
A
µα.K
(K
(α))
KB
B alt
A
KSock
alt
modulewhere
K(K)
module KSock where
Ser
B )
KB
KBK(α
KaltB Sock
A
K
(α
)
α
data SockT = ...
BA
importas
Socket(SockT)
Sock
µα.K
(K
(α))
A
B
K
αA
KAα
(αB )
α
data ServerT=...SockT...
KKAA(αB )KSer (α)
µα.K
(K
(α))
B
A
K
KSer (α)
BaltKSer (α)K(α)
Ser
module KMain (KSer (KSock ), KSer (KSock)) where
K
(K
)
K
Ser
Sock
B
K
(α
)
B
A
α
K
(K
) asΞ̃A.Server(ServerT)
importqualified
Ser + Ξ̃
Sock⇒
K
)
∆Ser
�(K
BSock
⇒
Ξ̃
∆;
Ξ̃
�
B
⇒
Ξ̃
�
Ξ̃
K
(K
)
1
1
1 Ser 2 Sock 2
1
alt2(S H S EQ)
αKSer (KSock ) as B.Server(ServerT)
K
importA (αqualified
B)K(α)⇒1 ,AΞ̃B∆;
� B2A (K⇒ BΞ̃(α))
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 B
12 ⇒
2
Ξ̃Ξ̃1µα.Kµα.KASer(KB (α)) ∆ �∆B�
µα.K
(K
(α))
B
(S H
...
KSer (α) ∆ �µα.K
(K
(α))
A
B
B1 , BΞ̃
2 ⇒KSer (K
)
µα.K
(K
(α))
Sock
B
A
µα.K
(K
(α))
30 (α))B2(K∆ ˜B� BA1 ⇒ Ξ̃1 ∆; Ξ̃µα.K� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 � B
˜ ⇒A Ξ̃2

Elaboration•••

packageserver-linked
where
packageserver-linked-alt where
Socket =[data]
SocketT=...
importSocketpackageserverwhere
KSer �
ver server
=
�
age
where
packageserverwhere
Server=[Server.hs]
includeserverimpl
includeserverimpl
data ServerT= ...SocketT...
packageserver-linked
where
packageserver-linked-alt
Socket=[importSocketdata
SocketT= ...] where
Server=cket = [data SocketT]serverimpl
Socket=socketimpl[data SocketT =� ...
]
= ...
�
includeincludesocketimpl-alt
K
includeincludeserverimpl
Sock
data
ServerT=...SocketT...
� package� serverimpl
�
importSocketwhere
ge server�importwhere Socket
Server=importSocketincludesocketimpl
includesocketimpl-alt
alt = ...SocketT...
ver=
Server=data
ServerT
includesocketsig
ket = [Socket.hs]
KpackagewhereServerT = ...SocketT...
Sockdata ServerT= server...SocketT...
data
KSer
Server=[...] wherever = [Server.hs]Socket = [Socket.hs]
package serverimpl
KA
age serverimpl
where
packagewhere KSer
A
Server serverimpl= [Server.hs]
includesocketsig
KOne
modulefile
peridentity
Sockge serverimpl
where
lude
socketsig
includesocketsig
packageserver-linked
where
packageserver-linked-alt whe
ServerSocketKB
KSock
Server =
[...]
ver =
[...]
ude
socketsig
Server serverimpl= [...] include
serverimpl
serverimpl
packagewhere
KA duplicated (ainclude
Code
la
C++
templates)
alt
Main
B
ver = [...]
includeserver-linked
socketimpl
includeserver-linked-alt
socketimpl-alt wheKSockα package
include socketsig
package
where
Kpackage
age server-linked
where
packageserver-linked-alt
packageserver-linked
whereserver-linked-alt
where
BwhereServerCodelargelypreserved
SocketServer= [...]
includeserverimpl
includeserverimpl
K
A
K
(α)
lude
serverimpl
includeserverimpl
includeserverimpl
include serverimpl
ge server-linked where
packageserver-linked-alt whereSer
includesocketimpl
includesocketimpl-alt
αKSer
Rewriteimports
toidentities
lude
socketimpl
includesocketimpl-alt
includesocketimpl
includeserver-linked-alt
socketimpl-alt whereude serverimpl package
includeserverimpl
server-linked
where KBpackage
KSer (KSock )ude socketimpl
socketimpl-alt
includeinclude
serverimpl
include serverimpl
KSer (α)
KSockα include K
K(KSeralt )includesocketimpl
socketimpl-alt
KSer
K
Ser
alt Sock
module KSerSer(KSock ) where KSock
KSer
KSer (α)
K
Sockmodule KSock
where
µα.K
import KSock as Socket(SockT)
A (KB (α))µα.K
(KB (α))KA
ASerK
data K
SockT
data K
ServerT
Ser (KSock=) ...SockT...
Sock = ...
A (α))µα.KBK(K
KA
KA
A
µα.K
(K
(α))
KB
B alt
A
KSock
alt
modulewhere
K(K)
module KSock where
Ser
B )
KB
KBK(α
KaltB Sock
A
K
(α
)
α
data SockT = ...
BA
importas
Socket(SockT)
Sock
µα.K
(K
(α))
A
B
K
αA
KAα
(αB )
α
data ServerT=...SockT...
KKAA(αB )KSer (α)
µα.K
(K
(α))
B
A
K
KSer (α)
BaltKSer (α)K(α)
Ser
module KMain (KSer (KSock ), KSer (KSock)) where
K
(K
)
K
Ser
Sock
B
K
(α
)
B
A
α
K
(K
) asΞ̃A.Server(ServerT)
importqualified
Ser + Ξ̃
Sock⇒
K
)
∆Ser
�(K
BSock
⇒
Ξ̃
∆;
Ξ̃
�
B
⇒
Ξ̃
�
Ξ̃
K
(K
)
1
1
1 Ser 2 Sock 2
1
alt2(S H S EQ)
αKSer (KSock ) as B.Server(ServerT)
K
importA (αqualified
B)K(α)⇒1 ,AΞ̃B∆;
� B2A (K⇒ BΞ̃(α))
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 B
12 ⇒
2
Ξ̃Ξ̃1µα.Kµα.KASer(KB (α)) ∆ �∆B�
µα.K
(K
(α))
B
(S H
...
KSer (α) ∆ �µα.K
(K
(α))
A
B
B1 , BΞ̃
2 ⇒KSer (K
)
µα.K
(K
(α))
Sock
B
A
µα.K
(K
(α))
30 (α))B2(K∆ ˜B� BA1 ⇒ Ξ̃1 ∆; Ξ̃µα.K� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 � B
˜ ⇒A Ξ̃2

Elaboration••••

packageserver-linked
where
packageserver-linked-alt where
Socket =[data]
SocketT=...
importSocketpackageserverwhere
KSer �
ver server
=
�
age
where
packageserverwhere
Server=[Server.hs]
includeserverimpl
includeserverimpl
data ServerT= ...SocketT...
packageserver-linked
where
packageserver-linked-alt
Socket=[importSocketdata
SocketT= ...] where
Server=cket = [data SocketT]serverimpl
Socket=socketimpl[data SocketT =� ...
]
= ...
�
includeincludesocketimpl-alt
K
includeincludeserverimpl
Sock
data
ServerT=...SocketT...
� package� serverimpl
�
importSocketwhere
ge server�importwhere Socket
Server=importSocketincludesocketimpl
includesocketimpl-alt
alt = ...SocketT...
ver=
Server=data
ServerT
includesocketsig
ket = [Socket.hs]
KpackagewhereServerT = ...SocketT...
Sockdata ServerT= server...SocketT...
data
KSer
Server=[...] wherever = [Server.hs]Socket = [Socket.hs]
package serverimpl
KA
age serverimpl
where
packagewhere KSer
A
Server serverimpl= [Server.hs]
includesocketsig
KOne
modulefile
peridentity
Sockge serverimpl
where
lude
socketsig
includesocketsig
packageserver-linked
where
packageserver-linked-alt whe
ServerSocketKB
KSock
Server =
[...]
ver =
[...]
ude
socketsig
Server serverimpl= [...] include
serverimpl
serverimpl
packagewhere
KA duplicated (ainclude
Code
la
C++
templates)
alt
Main
B
ver = [...]
includeserver-linked
socketimpl
includeserver-linked-alt
socketimpl-alt wheKSockα package
include socketsig
package
where
Kpackage
age server-linked
where
packageserver-linked-alt
packageserver-linked
whereserver-linked-alt
where
BwhereServerCodelargelypreserved
SocketServer= [...]
includeserverimpl
includeserverimpl
K
A
K
(α)
lude
serverimpl
includeserverimpl
includeserverimpl
include serverimpl
ge server-linked where
packageserver-linked-alt whereSer
includesocketimpl
includesocketimpl-alt
αKSer
Rewriteimports
toidentities
lude
socketimpl
includesocketimpl-alt
includesocketimpl
includeserver-linked-alt
socketimpl-alt whereude serverimpl package
includeserverimpl
server-linked
where KBpackage
KSer (KSock )ude socketimpl
socketimpl-alt
includeinclude
serverimpl
include serverimpl
KSer (α)
KSockα include K
K(KSeralt )includesocketimpl
socketimpl-alt
KSer
K
Ser
alt Sock
module KSerSer(KSock ) where KSock
KSer
KSer (α)
K
Sockmodule KSock
where
µα.K
import KSock as Socket(SockT)
A (KB (α))µα.K
(KB (α))KA
ASerK
data K
SockT
data K
ServerT
Ser (KSock=) ...SockT...
Sock = ...
A (α))µα.KBK(K
KA
KA
A
µα.K
(K
(α))
KB
B alt
A
KSock
alt
modulewhere
K(K)
module KSock where
Ser
B )
KB
KBK(α
KaltB Sock
A
K
(α
)
α
data SockT = ...
BA
importas
Socket(SockT)
Sock
µα.K
(K
(α))
A
B
K
αA
KAα
(αB )
α
data ServerT=...SockT...
KKAA(αB )KSer (α)
µα.K
(K
(α))
B
A
K
KSer (α)
BaltKSer (α)K(α)
Ser
module KMain (KSer (KSock ), KSer (KSock)) where
K
(K
)
K
Ser
Sock
B
K
(α
)
B
A
α
K
(K
) asΞ̃A.Server(ServerT)
importqualified
Ser + Ξ̃
Sock⇒
K
)
∆Ser
�(K
BSock
⇒
Ξ̃
∆;
Ξ̃
�
B
⇒
Ξ̃
�
Ξ̃
K
(K
)
1
1
1 Ser 2 Sock 2
1
alt2(S H S EQ)
αKSer (KSock ) as B.Server(ServerT)
K
importA (αqualified
B)K(α)⇒1 ,AΞ̃B∆;
� B2A (K⇒ BΞ̃(α))
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 B
12 ⇒
2
Ξ̃Ξ̃1µα.Kµα.KASer(KB (α)) ∆ �∆B�
µα.K
(K
(α))
B
(S H
...
KSer (α) ∆ �µα.K
(K
(α))
A
B
B1 , BΞ̃
2 ⇒KSer (K
)
µα.K
(K
(α))
Sock
B
A
µα.K
(K
(α))
30 (α))B2(K∆ ˜B� BA1 ⇒ Ξ̃1 ∆; Ξ̃µα.K� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 � B
˜ ⇒A Ξ̃2

Elaboration••••

packageserver-linked
where
packageserver-linked-alt where
Socket =[data]
SocketT=...
importSocketpackageserverwhere
KSer �
ver server
=
�
age
where
packageserverwhere
Server=[Server.hs]
includeserverimpl
includeserverimpl
data ServerT= ...SocketT...
packageserver-linked
where
packageserver-linked-alt
Socket=[importSocketdata
SocketT= ...] where
Server=cket = [data SocketT]serverimpl
Socket=socketimpl[data SocketT =� ...
]
= ...
�
includeincludesocketimpl-alt
K
includeincludeserverimpl
Sock
data
ServerT=...SocketT...
� package� serverimpl
�
importSocketwhere
ge server�importwhere Socket
Server=importSocketincludesocketimpl
includesocketimpl-alt
alt = ...SocketT...
ver=
Server=data
ServerT
includesocketsig
ket = [Socket.hs]
KpackagewhereServerT = ...SocketT...
Sockdata ServerT= server...SocketT...
data
KSer
Server=[...] wherever = [Server.hs]Socket = [Socket.hs]
package serverimpl
KA
age serverimpl where
packagewhere KSer
Server serverimpl= [Server.hs]
includesocketsig
KOne
modulefile package
per identity
Sock
geC
serverimpl
where
lude
socketsig
includesocketsig
packageserver-linked
whereserver-linked-alt whe
C
KB
KSock
Server =
[...]
verD=
[...]
ude
socketsig
Server= [...] include
serverimpl
serverimpl
packageserverimpl
where
K
Code
la
C++
templates)
A duplicated (ainclude
ServerSocketalt
ver = [...]
includeserver-linked
socketimpl
includeserver-linked-alt
socketimpl-alt wheKSockα package
include socketsig
package
where
Kpackage
age server-linked where
packageserver-linked-alt
packageserver-linked
whereserver-linked-alt
where
BwhereCodelargelypreserved
Server= [...]
includeserverimpl
Main include serverimpl
K
A
K
(α)
lude
serverimpl
includeserverimpl
includeserverimpl
include serverimpl
ge server-linked where
packageserver-linked-alt whereSer
includesocketimpl
includesocketimpl-alt
αKSer
Rewriteimports
toidentities
lude
socketimpl
includesocketimpl-alt
includesocketimpl
includeserver-linked-alt
socketimpl-alt whereude serverimpl package
includeserverimpl
server-linked
where KBpackage
KSer (KSock )ude socketimpl
socketimpl-alt
includeinclude
serverimpl
include serverimpl
KSer (α)
KSockα include K
K(KSeralt )includesocketimpl
socketimpl-alt
KSer
K
Ser
alt Sock
module KSerSer(KSock ) where KSock
KSer
KSer (α)
K
Sockmodule KSock
where
µα.K
import KSock as Socket(SockT)
A (KB (α))µα.K
(KB (α))KA
ASerK
data K
SockT
data K
ServerT
Ser (KSock=) ...SockT...
Sock = ...
A (α))µα.KBK(K
KA
KA
A
µα.K
(K
(α))
KB
B alt
A
KSock
alt
modulewhere
K(K)
module KSock where
Ser
B )
KB
KBK(α
KaltB Sock
A
K
(α
)
α
data SockT = ...
BA
importas
Socket(SockT)
Sock
µα.K
(K
(α))
A
B
K
αA
KAα
(αB )
α
data ServerT=...SockT...
KKAA(αB )KSer (α)
µα.K
(K
(α))
B
A
K
KSer (α)
BaltKSer (α)K(α)
Ser
module KMain (KSer (KSock ), KSer (KSock)) where
K
(K
)
K
Ser
Sock
B
K
(α
)
B
A
α
K
(K
) asΞ̃A.Server(ServerT)
importqualified
Ser + Ξ̃
Sock⇒
K
)
∆Ser
�(K
BSock
⇒
Ξ̃
∆;
Ξ̃
�
B
⇒
Ξ̃
�
Ξ̃
K
(K
)
1
1
1 Ser 2 Sock 2
1
alt2(S H S EQ)
αKSer (KSock ) as B.Server(ServerT)
K
importA (αqualified
B)K(α)⇒1 ,AΞ̃B∆;
� B2A (K⇒ BΞ̃(α))
� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 B
12 ⇒
2
Ξ̃Ξ̃1µα.Kµα.KASer(KB (α)) ∆ �∆B�
µα.K
(K
(α))
B
(S H
...
KSer (α) ∆ �µα.K
(K
(α))
A
B
B1 , BΞ̃
2 ⇒KSer (K
)
µα.K
(K
(α))
Sock
B
A
µα.K
(K
(α))
30 (α))B2(K∆ ˜B� BA1 ⇒ Ξ̃1 ∆; Ξ̃µα.K� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
1 � B
˜ ⇒A Ξ̃2

Elaboration••••

packageserver-linked
where
packageserver-linked-alt
where
Socket =[data]= [data
SocketSocketT=...
importSocketSocketT=...]packageserver
where
K
Ser
ver
=
� where�� serverimpl
�
age serverdata
whereServerT
packageserverincludeserverimpl
include=...SocketT...
package server-linked
where
packageserver-linked-alt
Socket= [data
SocketT= Socket...] whereimportSocketimportpackageserverwhere
Server=cket = [data SocketT]serverimpl
Socket=socketimpl[data SocketTServer]= serverimpl= ...
�=�= ...
includeincludesocketimpl-alt
K
Sock
includeincludedata
ServerT...SocketT...
data ServerT
Socket� = [data�
importSocketT
Socket=� ...] = ...SocketT...
ge server�importwhere Socket
Server=import Socket �data
includesocketimpl
includesocketimpl-alt
alt = ...SocketT...�
ver=
Server=ServerT
Socketket = [Socket.hs]
KSockpackagewhere
packageserverimpl
wheredata ServerT= server...SocketT...
data
ServerT...SocketT...
Server=K =importSerdata ServerT = ...SocketT...
ver = [Server.hs]Socket = [Socket.hs]
includesocketsig
package serverimpl
where KA
K
age serverimpl where
package
where
Ser
Server serverimpl= [Server.hs]
Server=[...]includesocketsig
KOne
modulepackageserverimpl
wherefile per identity
Sock
geC
serverimpl
where
lude
socketsig
includesocketsig
C
KB
Server
=
[...]
KSock
includesocketsig
verD=
[...]
ude
socketsig
Server= [...] where
packageserverimpl
KA duplicatedpackageserver-linked(awherepackageserver-linkeCodela C++
templates)
ServerSocketalt
Server=[...]ver = [...]
Kinclude
include socketsig
serverimpl
include serverimp
Sockpackage server-linked
whereα package server-linked-alt
wheK
age server-linked where
packageserver-linked-alt
where
packagewhere
packageserver-linked-alt
where
B largely
Codepreserved
Server server-linked= [...]
includesocketimpl
include socketimp
includeserverimpl
includeserverimpl
Mainpackageserver-linked
where
packageserver-linked-alt
wheK
KSer (α)
A wherelude
serverimpl where
includeserverimpl
includeserverimpl
include serverimpl
ge server-linked
packageserver-linked-alt
includesocketimpl
includesocketimpl-alt
αserverimpl
serverimpl
Rewriteimports
toidentities
lude
socketimpl
includesocketimpl-alt
includesocketimpl
includesocketimpl-alt
ude serverimpl package
includeserverimpl
server-linked where KBpackage server-linked-alt
KSer (KSockinclude) KSerwhere
includesocketimpl
socketimpl-alt
ude socketimpl
includesocketimpl-alt
include serverimpl
include serverimpl
KSer (α)
K(Kα include K
Seralt )includesocketimpl
socketimpl-alt
KSer
KSer
module KSer
(KSock ) whereSerKSerSock KSock
KSer
KSer (α)
KSockµα.K
module KSock
where
import KSock as Socket(SockT)
A (KB (α))KAµα.K(KB (α))ASer
K
KKSockK(K)
data K
SockT
=
...
data
ServerT=...SockT...
Ser
Sock
A (α))µα.KB (K
KSock
KA
A
KB
A
µα.K
(K
(α))
B alt
A
KSock
alt
KA
moduleK(K
module KSock where
Ser
Sock ) where KB
KB (αA )
KB
KaltB
α
K
(α
)
data SockT = ...
BA
importas
Socket(SockT)
KαB
Sock
µα.K
(K
(α))
A
B
K
KA (αB ) KSer (α)αAαdata ServerT=...SockT...
KKAA(αB )α(α)µα.K
B (KA (α))
K
K
B
alt
Ser
KSer (α)
KSer (α)
module))) where
KMain (KSer (KSock ), KSer (KSock
KBB(αA )
KSer
(α) )
K
α
K
(K
qualified� Ξ̃Ser + Ξ̃
A.Server(ServerT)
Sock⇒asΞ̃CK) Ξ̃1 ∆; Ξ̃1 K
∆Ser
�(K
BSock
�import
B(K
1 ⇒
2 ⇒
1
2
µα.K
(K
Ser
SockΞ̃)2A
B (α))(S H S EQ)
αKSer (KimportqualifiedDK(α)
Sock ) as B.Server(ServerT)
A
B
K
(α)
µα.K
(K
(α))
⇒1 ,Ξ̃B∆;� Ξ̃1 + Ξ̃2 ⇒ Ξ̃
BΞ̃2
1 B
12 ⇒
Ξ̃Ξ̃1 � B2A ⇒µα.Kµα.KASer(KB (α)) ∆ �∆B�
µα.K
(K
(α))
A
B
(K
B
A (α))(S H...
KSer (α) ∆ �µα.K
A (K
B (α))
B
,
B
⇒
Ξ̃
1
2
K
(K
)
µα.K
(K
(α))
Ser (KSock
B
A
µα.K
(α))
30 (α))B2(K∆ ˜B� BA1 ⇒ Ξ̃1 ∆; Ξ̃µα.K� Ξ̃1 + Ξ̃2 ⇒KΞ̃B (αA )1 � B˜ ⇒A Ξ̃2

Elaboration••••

Type Systemmodule identity
simplifies and organizes
the semantics
31

Type System

Elaboration

module identity
simplifies and organizes
the semantics
31

What else is in the paper?

• Thinning and renaming• Formalization of Haskell modules• Elaboration soundness statement & proof• Metatheory/axioms for “core language”

32What else is in the paper?

53-page appendix• Thinning and renaming• Formalization of Haskell modules• Elaboration soundness statement & proof• Metatheory/axioms for “core language”

32

Future Work

typeclasses

integration
with Cabal&
packagemanager

33

Contributions
strongweak• Retrofits Haskell with strong modularity- Designed at package level- Employs simplified mixin design- Defined as elaboration into weak Haskell modules- Separate typechecking, not separate compilation• Generic design could work for other weak langs
34

Targeting an existing, weakmodule language is not justpractical but interesting!

35

Targeting an existing, weakmodule language is not justpractical but interesting!

Thanks!
35

Bonus Materials

36

Proving soundness was hard.
• First had to formally define “plain Haskell modules”
and binary interface files- But not Haskell typechecking!
• Only formalization* of Haskell modules with:- separately checkable recursive modules- conventional metatheory, e.g. Weakening, Substitution
and metatheory are parameterized by• Definitions
axioms for “core” level of terms and types
generalize to other “weak” langs with
- Could
Haskell’s module semantics* others: [Faxén, JFP ’02] [Diatchki et al., Haskell ’02]37

Type Classes• Which instances from A
package problematic where
A :: [data T; ...]
B :: 
[data T; ...]

import qualified Aimport qualified Binstance Eq A.T whereC =  eq t1 t2 = True
instance Eq B.T where
eq t1 t2 = False
38

and B impls does C see?

- Elab. of C must specify
imported instances• Package type presumes
A.T distinct from B.T- Can’t use same impl
for A and for B

Implementation Checkpackage containers-sig-1.x where
includeprelude-sig-4.xwhere
packagecontainers-sig-1.x• Author wants to checkincludeprelude-sig-4.x
Data.Set:: [import Prelude; ...]
that she implements sig
Data.Set :: [import Prelude; ...]

But not all holes in sig•
package containers-impl-1.5 whereare implemented in impl
packagecontainers-impl-1.5
includeprelude-sig-4.x where
includeprelude-sig-4.x
HiddenImpl= [...]
�� • How exactly to define
HiddenImpl = [...]import Prelude��
implements then?
PreludeData.Set=importimportHiddenImpl
Data.Set= import... HiddenImpl...
implements containers-sig-1.x
implements containers-sig-1.x
39

Conditionals
package mylib where#ifdef __GHC__import GhcStuﬀ
...ghc-specific impl...
Foo = 
#else...default impl...
#endifwrong!
#if in program
is not typeable
at package levelright!
conditional at
the level of
package language!

branches might
introduce theirown bindings
package mylib
where


case compiler
� of
�


Mixin Impossible:
Language
Definition
import
GhcStuﬀ
Foo = ghc⇒
...ghc-specific impl... 
Scott Kilpatrick_<skilpat@mpi-sws.org>⇒ [...default impl...]v2013.10.22

1 Package Syntax

40