87 


88 
[l1, l2, [a,b,c,s1,d,e], l4] 
[l1, l2, [a,b,c,s1,d,e], l4] 
89 


90 
would yield depth=2, num=4 (assuming 0based depth and 1based num indexing, 
would yield depth=2, num=4 (assuming 0based depth and 1based num indexing, which I think is being used. [NOTE: This assumes that depth is counted from the toplevel. If depth is counted outward from the current position as in conventional DeBruijn indexing, depth would be 1 instead.]. 
91 
which I think is being used. [NOTE: This assumes that depth is counted from the toplevel. 

92 
If depth is counted outward from the current position as in conventional DeBruijn 
As we enter each functor during translation, we need to determine the list of flexible stamps of the primary tycons and functors of its parameter instantiation, and we add this list to the end of the abstraction environment. [Or should it be added to the front of the environment list? This depends on whether depth is counted relative to toplevel or relative to current abstraction depth.] 

indexing, depth would be 1 instead.]. 





As we enter each functor during translation, we need to determine the 


list of flexible stamps of the primary tycons and functors of its 


parameter instantiation, and we add this list to the end of the 


abstraction environment. [Or should it be added to the front of the 


environment list? This depends on whether depth is counted relative 


to toplevel or relative to current abstraction depth.] 

93 


94 
Regardless of the method used for encoding the primary type information, the LAMBDA fctexp form must also carry that information because entity evaluation ultimately must produce a functor entity given only the LAMBDA, epc, and current entity environment. Any approach that requires modification of the functor entity form must suffer a similar shortcoming. That is to say, primary type information must be propagated through the LAMBDA fctexp because entity evaluation needs that information in order to produce a wellformed fctEntity. [DBM: Not clear what this para means  try to clarify.] 
Regardless of the method used for encoding the primary type information, the LAMBDA fctexp form must also carry that information because entity evaluation ultimately must produce a functor entity given only the LAMBDA, epc, and current entity environment. Any approach that requires modification of the functor entity form must suffer a similar shortcoming. That is to say, primary type information must be propagated through the LAMBDA fctexp because entity evaluation needs that information in order to produce a wellformed fctEntity. [DBM: Not clear what this para means  try to clarify.] 
95 


96 
Having determined the depth and num parts of the plambda type variable 
Having determined the depth and num parts of the plambda type variable for a formal/primary element with reference to the abstraction environment, we need to also determine the tkind of that element in order to construct the corresponding plambda type variable. If the item being translated is a FORMAL tycon, we have its arity and can immediately translate that into the appropriate tkind. If the item is a formal functor, it is a FCT and we therefore have its functor signature. So we need to transate its functor signature into a tkind. 
97 
for a formal/primary element with reference to the abstraction 

98 
environment, we need to also determine the tkind of that element in 
[Q: Can we translate a functor signature by itself into a tkind, or is any auxiliary information, e.g. an entityEnv, needed?] 
99 
order to construct the corresponding plambda type variable. If the 
[A: The functor signature alone is insufficient for computing tkinds mainly due to the presence and resolution mechanism of sharing constraints. Because functor signatures are instantiated and with them their respective functor parameter signatures, instantiation picks particular representatives or primary types.] 
100 
item being translated is a FORMAL tycon, we have its arity and can 
[DBM: I will assume that it is ok to use signature instantiation as a tool to translate a functor 
101 
immediately translate that into the appropriate tkind. If the item is 
signature into a tkind. Whether it is important to avoid repeated instantiation of the same signature 
102 
a formal functor, it is a FCT and we therefore have its functor 
(i.e whether we might need to memoize instantiations) is a separate issue of performance to be 
103 
signature. So we need to transate its functor signature into a tkind. 
addressed later.] 
104 
[Q: can we translate a functor signature by itself into a tkind, or is 


any auxiliary information, e.g. an entityEnv, needed?] 


[A: The functor signature alone is insufficient for computing tkinds mainly due to the presence and resolution mechanism of sharing constraints. Because functor signatures are instantiated and with them their respective functor parameter signatures, instantiation picks particular representatives or primary types. 

105 
[Q: How should transtypes tpsKnd be adapted to use this new primary type information?] 
[Q: How should transtypes tpsKnd be adapted to use this new primary type information?] 
106 
[A: tpsKnd is used by tpsTyc (for functor tycons), fctRlznLty, and the FCTfct case of mkFctexp.] 
[A: tpsKnd is used by tpsTyc (for functor tycons), fctRlznLty, and the FCTfct case of mkFctexp.] 
107 


127 
end) 
end) 
128 
= struct end; 
= struct end; 
129 


130 
/\([M]=>M, M, ([[]=>[]]=>[])).  (t0, t2, G) primary elements of X 
/\([M]=>M, M, ([[]=>[]]=>[])).  abstraction over (t0, t2, G), primary elements of X 
131 
\v1:STR([\/([]=>[]).FCT(\/[].FCT([],[]),[]), {TCAP(TV(1,0), PRIM(I)),PRIM(I),TV(1,1)}) 
\v1:STR([\/([]=>[]).FCT(\/[].FCT([],[]),[]), {TCAP(TV(1,0), PRIM(I)),PRIM(I),TV(1,1)}]). 
132 

 abstraction over the value part of X (v1), with a structure "STR" type 
133 

{ }  the empty structure body 
134 


135 

[DBM: the printing conventions here are not very clear, maybe they can be improved 
136 

to make the terms more readable. 
137 


138 

"/\" represents capital lambda, representing type variable abstraction (followed by a tuple of kinds for the abstracted type variables). 
139 

"\" represents ordinary value lambda abstraction, with a value variable (here "v1") annotated with 
140 

its type. 
141 

"STR" is presumable a valuelevel structure record. Here this would be the value part of the 
142 

parameter structure X. In this case the structure contains two value elements, G and a. 
143 

The type of a is expressed by {TCAP(TV(1,0), PRIM(I)),PRIM(I),TV(1,1)}, with TV(0,1) representing 
144 

t0, TV(1,1) representing t2 (the 0th and 1st elements of the abstracted type tuple). 
145 

The type of the G functor element must be represented by \/([]=>[]).FCT(\/[].FCT([],[]),[]). 
146 

Does "\/" represent a polymorphic quantification? I'm not sure how to parse this 
147 

type expression. 
148 

] 
149 


150 
Formal type components such as t0 and t2 translate into type abstractions of the appropriate kind (may be a nonmonokind, e.g., t0 is kind [M]=>M). They are indexed according to type abstraction depth and position in the formal argument list. For example, F has two formal type arguments, t0 and t2 which occur in the body as TV(1,0) and TV(1,1) respectively. The first index is the deBruijn index. The second is the position of that formal in the list of all formals up to sharing equivalence. 
Formal type components such as t0 and t2 translate into type abstractions of the appropriate kind (may be a nonmonokind, e.g., t0 is kind [M]=>M). They are indexed according to type abstraction depth and position in the formal argument list. For example, F has two formal type arguments, t0 and t2 which occur in the body as TV(1,0) and TV(1,1) respectively. The first index is the deBruijn index. The second is the position of that formal in the list of all formals up to sharing equivalence. 
151 


152 
The formal functor G is decomposed into a type abstraction part ([[]=>[]]=>[]) and a lambda part \/([]=>[]).FCT(\/[].FCT([],[]).[]). 
The formal functor G is decomposed into a type abstraction part of kind ([[]=>[]]=>[]) and a lambda part of type \/([]=>[]).FCT(\/[].FCT([],[]).[]). 
153 


154 


155 

 
156 

Another example: 
157 


158 
functor F(X:sig type t functor G(Y:sig type s val x : s * t end): sig type u end end) = ... 
functor F(X:sig type t functor G(Y:sig type s val x : s * t end): sig type u end end) = ... 
159 

