Changes between Version 37 and Version 38 of TypeFunctions


Ignore:
Timestamp:
Aug 3, 2006 6:23:04 PM (9 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 ==