Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] View of /sml/branches/primop-branch-3/compiler/DEVNOTES/ElabMod/primary-types
ViewVC logotype

View of /sml/branches/primop-branch-3/compiler/DEVNOTES/ElabMod/primary-types

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3334 - (download) (annotate)
Tue May 12 23:28:09 2009 UTC (10 years, 2 months ago) by gkuan
File size: 6891 byte(s)
*** empty log message ***
Primary & Secondary types
---------------------

Concerning the translation of signatures (functor parameter signatures in particular) into kinded type variable abstractions.

A functor parameter signature will be translated into a type abstraction (TFUN) over several type variables.  These type variables correspond to certain tycon and functor elements of the signature, and the list is flattened over the signature hierarchy.

Any nondefined functor element gets a type variable, whose kind is derived from the functor signature of that element.

A tycon element is "primary", and gets a type variable, if it is _formal_, i.e. neither defined, nor a datatype.  Datatypes are viewed has having a defined structure given by the datatype spec.  The kind of the plambda type variable for a primary tycon is computed from the arity of the tycon (PLambdaType.tkc_int).  A formal tycon is a GENtyc with kind=FORMAL.

Only one type variable is included per sharing equivalence class of tycons (& functors?).  Hence instantiation (which determines the sharing equivalence classes and their representative elements) is naturally involved in the determination of the primary tycons and their plambda type variables.

It is therefore not possible (not easy?) to compute the primary tycons from a signature without performing instantiation or an analysis of sharing equivalence that would be closely related to instantiation.

How could the primary tycons of a signature be identified.

(a) a symbolic path
(b) an entity path
(c) a flexible stamp (associated with the representative tycon in an instantiation)

(a) and (b) are intertranslatable from the signature representation.  I.e.  given a symbolic path for an element, we follow that path, extracting the entityVar for each spec along the way to form the corresponding entity path.  Starting with the entity path, we can search for the corresponding element in successive elements lists and capture the corresponding symbolic names to form a symbolic path.

Representing a primary tycon as a flexible stamp, as in (c), is clearly relative to a particular
instantiation of the signature.

Unfortunately, because elaboration introduces tycons directly into the abstract syntax of the functor body, particularly GENtycs which can only be distinguished by their stamps, neither symbolic paths nor entity paths are adequate to identify primary types throughout the abstract syntax.  
-----------------------

Translating tycons.

Primary tycons need to be translated to the corresponding plambda type variable in the TransTypes (in toTyc).

Currently tycpaths (FLINT/trans/tycpath.sml) are used as an intermediate form in the translation from (frontend) types to plambda types.  It is likely that this intermediate representation can be eliminated.  

The tycpath for a tycon is either just the tycon itself (TP_TYC tyc), or a representation of a plambda type variable, TP_VAR{tdepth,num,kind}.   Compound tycpaths (TP_FCT, TP_APP,
and TP_SEL) have to do with functors and structures.

[Q: What is the role of TP_TYC?  Shouldn't all primary tycons be represented by a TP_VAR?
If so, are the arguments of TP_TYC secondary tycons?  In that case, what do they have to
do with the plambda type or kind?]
[A: TP_TYC encodes DATATYPEs, abstract GENtycs, and all other nonformals (PRIMITIVE and TEMP (which should be impossible at this point))]. 

---------------------
Determining the tkind (plambda kind) of a functor element.

A functor element in a signature is translated into a type function and also into a lambda term.  The type function has a kind (tkind), which must be computable from the functor signature.

PLambda kinds have the following forms:

fun K ... K -> K      -- an n-ary type operator
seq K ... K              -- an n-tuple of type constructors
    0 ... n                -- a basic tycon of arity k

----------------------
External functors and primary types in closures

Because pidinfo in persistent maps contain lty information for the given pid, the lty for externally referenced functor (i.e., an occurrence of a functor name that is defined outside the compilation unit), the FLINT lty must be computed. The lty does not have to be computed before elaboration of the functor variable for local functor variables because we do not create persistent map entries for those. 
[Q: What is a pidinfo, and where is it defined?]
[A: pidinfo is defined in translate.sml as a list with ANON or NAMED id as elements.]
[Q: Where in the code is the lty for an external functor computed?]
[A: The lty for the external functor is computed by mkAccInfo using a first-class function getLty. The getLty for the mkFct invocation of mkAccInfo is defined to be fn () => fctLty(...) where fctLty is defined in transtypes.]

We translate externally defined functor variables by looking through intermediate PATH accesses until we get to an EXTERN access. Then we compute the lty for that functor variable given that functor and compInfo. 
[Q: How?  What does compinfo have to do with this?]
[A: PATH accesses contain another access inside. Alternatively, we may end up with an LVAR but this is impossible because mkAccInfo checks that the access is indeed extern before we do this step. compinfo is pass through to support EvalEnt.evalApp. evalApp only uses the mkStamp part of compinfo.]

=========================

Idea: Replace paramRlzn with list of primary flexible stamps including functor stamps 

=========================

Primary types

The following are some examples of how functor parameters translate into FLINT types. The only phenomenon not illustrated is the flattening of hierarchically nested structures in the functor parameter. 

functor F(X:
sig 
  type 'a t0 
  type t1 = int 
  functor G(Y:sig 
                type 'a u = 'a t0 
                functor H(Z:sig end):sig end 
              end): 
     sig 
       type u' = t1 
     end 
   type t2 
   val a : (int t0) * t1 * t2 end) 
= struct end;  

/\([M]=>M,M,([[]=>[]]=>[]).\v1:STR([\/([]=>[]).FCT(\/[].FCT([],[]),[]), {TCAP(TV(1,0), PRIM(I)),PRIM(I),TV(1,1)})

Formal type components such as t0 and t2 translate into type abstractions of the appropriate kind (may be a non-monokind, 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.  

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



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

/\(M,[M]=>[M]).\v1: STR(\/[M].FCT(STR[TYC{TV(1,0),TV(2,0)}],STR(STR([])))))



root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0