Changes between Version 37 and Version 38 of TypeFunctions


Ignore:
Timestamp:
Aug 3, 2006 6:23:04 PM (8 years ago)
Author:
chak
Comment:

Type checking indexed types (I)

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctions

    v37 v38  
    3838 * We currently don't allow associated GADTs. I cannot see any fundamental problem in supporting them, but I want to keep it simple for the moment. (When allowing this, a constructor signature in an associated GADT can of course only refine the instantiation of the type arguments specific to the instance in which the constructor is defined.) 
    3939 
     40 
    4041== Terminology == 
    4142 
     
    5253'''Associated type''': An indexed type that is declared in a type class. 
    5354 
     55'''Type family''': Indexed types can be regarded as families of types; especially in the case of indexed data types, we call each declaration at a particular type index as ''member'' or ''element'' of that family. 
     56 
    5457'''Definitions vs. declarations''': We sometimes call the kind signature of an indexed constructor its ''declaration'' and the subsequent population of the type family by type equations or indexed data/newtype declarations the constructor's ''definition''. 
     58 
    5559 
    5660== How It Works == 
     
    8387=== Representation of associated types === 
    8488 
    85 We add type declarations to class declarations and instance declarations by a new field (of type `[LTyClDecl]`) to both `TyClDecl.ClassDecl` (known by the field name `tcdATs`) and `TyClDecl.InstDecl`.  For classes, this new field contains values constructed from `TyData`, `TyFunction`, and `TySynonym`, whereas for instances, we only have `TyData` and `TySynonym`.  This is due to (a) `TyData` representing both signatures and definitions of associated data types (whereas the two are split into `TyFunction` and `TySynonym` for associated synonyms) and (b) associated synonyms having default definitions, which associated data types do not possess. 
     89We add type declarations to class declarations and instance declarations by a new field, of type `[LTyClDecl]`, to both `TyClDecl.ClassDecl` (known by the field name `tcdATs`) and `TyClDecl.InstDecl`.  For classes, this new field contains values constructed from `TyData`, `TyFunction`, and `TySynonym`, whereas for instances, we only have `TyData` and `TySynonym`.  This is due to (a) `TyData` representing both signatures and definitions of associated data types (whereas the two are split into `TyFunction` and `TySynonym` for associated synonyms) and (b) associated synonyms having default definitions, which associated data types do not possess. 
    8690 
    8791=== Phasing === 
     
    121125---- 
    122126 
    123 ---- 
    124 `Revise from here!` 
    125 ---- 
     127=== Type checking indexed data types === 
    126128 
    127 === Type checking associated data types === 
     129Type checking in the presence of only indexed data and newtypes is much simpler than in the presence of type functions as type equality remains purely syntactic (i.e., we do not need to change the unification procedure).  However, we need to check that the alternatives of a case expression inspecting an indexed data type contains only constructors of one member of the family.  (To relax this restriction, we would need a story for compiling open data types.) 
    128130 
    129 Type checking in the presence of only associated data types is much simpler than in the presence of associated type synonyms (or general type functions) as type equality remains purely syntactic (i.e., we do not need to change the unification procedure).  However, we need to check that the alternatives of a case expression inspecting an associated data type contains only constructors defined within the same instances.  (To relax this restriction, we would need a story for compiling open data types.) 
     131==== Desugaring indexed data types ==== 
    130132 
    131 Class declarations: 
    132  * As part of the knot typing exercises in `TcTyClsDecls.tcTyAndClassDecls`, we extract all AT declarations from classes and add them to the list of class and data type declarations to be processed. This ensures that AT declarations participate in kind checking and that they are entered into the global type-checker environment. 
     133The kind signature of an indexed data type 
     134{{{ 
     135data T (a1::<kind1>) .. (an::<kindn>) :: <kind> 
     136}}} 
     137turns into an F,,C,, type function declaration 
     138{{{ 
     139type T_n : <kind1> -> .. -> <kindn> -> <kind> 
     140}}} 
     141A member of an indexed data type 
     142{{{ 
     143data T t1 .. tn b1 .. bm = <constructors> 
     144}}} 
     145turns into an equality axiom and a vanilla data declaration 
     146{{{ 
     147axiom cTinst : (forall c1..cr. T_n t1 .. tn) :=: (forall c1..cr. Tinst c1 .. cn) 
     148data Tinst c1 .. cr b1 .. bm = <constructors> 
     149}}} 
     150where the `ci` are the free variables of the `tj`.  Moreover, we replace all occurences of `T` in the rest of the program by `T_n`. 
     151 
     152==== Inserting coercions ==== 
     153 
     154To ensure that the F,,C,, code generated by the above desugaring still type checks, we need to introduce cast expressions using `cTinst` to move between the indexed type `T_n` and the representation types, such as `Tinst`, of its members.  The simplicity of type checking and desugaring indexed data types - as opposed to general type functions - is due to the locations where these casts need to be added being well defined.  More precisely, there are two different kinds of locations corresponding to the introduction and elimination of indexed data types: 
     155 1. Wrappers for data constructors introduce indexed types. 
     156 2. Case expressions scrutinising indexed types eliminate them. 
     157 
     158==== Wrappers for indexed types ==== 
     159 
     160 
     161 
     162=== Type checking associated types === 
     163 
     164==== Class declarations ==== 
     165 
     166 * As part of the knot tying exercises in `TcTyClsDecls.tcTyAndClassDecls`, we extract all AT declarations from classes and add them to the list of class and data type declarations to be processed. This ensures that AT declarations participate in kind checking and that they are entered into the global type-checker environment. 
    133167 * We do ''not'' update the data declarations within class declarations (field `tcdATs` within `ClassDecl`), as the `Class.Class` structure produced by the type checker only contains the `Id`s of a classes associated types. 
    134168 * We check that we have -fglasgow-exts. 
    135169 
     170==== Instance declarations ==== 
     171 
     172We need to handle ATs in `TcInstDcls.tcInstDecls1`, which is where the type information in instances - i.e., in vanilla Haskell just the instance heads - are processed. 
     173 
     174=== Representation of type functions after type checking === 
     175 
     176Type functions have a number of properties in common with class instances; in particular, they require a machinery for matching type patterns against types, as instance heads do during context simplification.  Hence, we probably want some structure similar to `InstEnv.Instance` for type functions - for instances this is maintained in the field `iSpec` of `TcEnv.InstInfo` (for type functions we don't need anything like `iBinds` as they are pure type-level entities).  If possible, it would be ideal if we can reuse (or generalise) some of the matching machinery for instance heads. 
     177 
     178The essentials of a module after type checking are in `HscTypes.ModGuts`; in particular, we have two fields `mg_insts :: [Instance]` and `mg_binds :: [CoreRule]` containing all instance heads and all rewrite rules respectively.  Similarly, we now want something like `mg_tyequa :: [TyEqua]` to represent all type euqations.   
    136179 
    137180== Possible Extensions ==