Polymorphism

Syntax

Extend the syntax of patterns with:
 
p ::= ...
| x : type (Pat TyVar)
| x : serializable type (Pat Serial TyVar)
 
 Extend the syntax of types with:
 
T ::= ...
| x (Type TyVar)
 
 Extend the syntax of values with:
 
v ::= ...
| T (Val Type)
 

Dynamic semantics

No changes are required.

Static semantics

Add hypotheses x : type and x : serializable type to contexts, typed as:
 
(Con TyVar) [x not in ]
(x : type) : context
 
(Con TyVar) [x not in ]
(x : serializable type) : context
 
(Serializable TyVar) [x not in ]
(x : type) : serializable context
 
(Serializable TyVar) [x not in ]
(x : serializable type) : serializable context
 
 Add the type judgements:
 
(Type TyVar)
, x : type,  x: type
 
(Type Serial TyVar)
, x : serializable type,  x: type
 
(Serializable TyVar)
, x : serializable type,  x: serializable type
 
 Add new rules for pattern matching:
 
T : type
(Match TyVar)
T matches x : type
 
T : serializable type
(Match Serial TyVar)
T matches x : serializable type
 
Add new binding rules for patterns:
 
(Pat Bind TyVar) [x not in ]
(x : type) : (x : type)
 
(Pat Bind Serial TyVar) [x not in ]
(x : serializable type) : (x : serializable type)
 
Add a new side-condition to the rule (Exp Dec:
 
D : 
,  e : T
(Exp Declaration) [bv  disjoint fv T]
D e : T
 
Replace the type rule for function application by:
 
v : function p : U
w matches p
(Exp Apply function)
v w : U[w/p]
 

Subject reduction

Proposition If   N : network and N * M then   M : network.