Changes between Version 27 and Version 28 of TypeFunctionsSynTC


Ignore:
Timestamp:
Jan 27, 2007 12:34:27 PM (8 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC

    v27 v28  
    11= Type Checking with Indexed Type Synonyms = 
    2 [[PageOutline]] 
    3  
    4 == Background == 
    52 
    63GHC has now FC as its typed intermediate language. 
     
    2825However, type checking with type functions is challenging. 
    2926 
    30 == The challenge == 
    31  
    32 Consider the axioms 
    33  
    34 {{{ 
    35 forall a. S [a] = [S a]   (R1) 
    36 T Int = Int               (R2) 
    37 }}} 
    38 S and T are type functions of kind *->* 
    39 For convenience, I drop the `redundant' forall a. on R1's lhs. 
    40  
    41 Suppose some type annotations/pattern matchings give rise 
    42 to the local assumptions 
    43  
    44 {{{ 
    45 T [Int] = S [Int]        (R3) 
    46 T Int = S Int            (R4) 
    47 }}} 
    48 and under these assumptions we need to verify 
    49  
    50 {{{ 
    51 T [Int] = [Int] 
    52 }}} 
    53  
    54  
    55 Logically, we can express the above as follows: 
    56  
    57 {{{ 
    58 (forall a. S [a] = [S a]) /\       -- axioms 
    59 (T Int = Int) 
    60  
    61  |= 
    62  
    63  
    64  
    65 (T [Int] = S [Int]) /\             -- local assumptions 
    66 (T Int = S Int) 
    67  
    68  implies 
    69  
    70 (T [Int] = [Int])                  -- (local) property 
    71 }}} 
    72 That is, any model (in the first-order sense) which is 
    73 a model of the axioms and local assumptions is also 
    74 a model of the property. 
    75  
    76 NOTE: There are further axioms such as reflexitivity of = etc. 
    77 We'll leave them our for simplicitiy. 
    78  
    79 The all important question: 
    80 How can we algorithmically check the above statement? 
    81 Roughly, we perform the following two steps. 
    82  
    83  1. Generate the appropriate implication constraint out of the program text.  That's easy cause GHC supports now implication constraints. (There are some potential subtleties, see GENERATEIMP below). 
    84  2. Solve the implication constraint by applying axioms and local assumptions until the (local) property is verified. That's the hard part. 
    85  
    86 NOTE:  
    87  
    88 We assume that (implication) constraints consist of  equality constraints only. In general, we'll also find type class constraints. We ignore such constraints  for the moment. 
    89  
    90 In the following, we assume that symbols t refer to types and symbols C refer to conjunctions of equality constraints and Ax refers to an axiom set. 
    91  
    92 We'll restrict ourselves to simple implication constraints of the form {{{   C implies t1=t2 }}} 
    93 In general, implication constraints may be nested, e.g 
    94 {{{ C1 implies (C2 implies C3) }}} and may contain conjunctions 
    95 of implications, e.g. {{{C1 implies (F1 /\ F2)}}} where F1 and F2 are arbitrary implication constraints. Implication constraints may be universally quantified, e.g.  
    96 {{{ forall a (S a = T a implies ...) }}} 
    97 These universal quantifiers arise from universal type annotations, e.g.  {{{ f :: S a = T a => ....}}}, and 
    98 pattern matchings over data types with abstract components, e.g. data Foo where 
    99 {{{ K :: S a = T a => a -> Foo}}} 
    100 We can operationally deal with universally quantified variables by skolemizing them (and we must ensure that skolemized/universal variables do not escape). 
    101  
    102 End of NOTE 
    103  
    104 == Various refinements of an approach to solve the challenge == 
    105  
     27 * [wiki:TypeFunctionsSynTC/Challenge The challenge] 
    10628 * [wiki:TypeFunctionsSynTC/Naive A first (naive) attempt] 
    10729 * [wiki:TypeFunctionsSynTC/Second A second attempt]