Changes between Version 27 and Version 28 of TypeFunctionsSynTC


Ignore:
Timestamp:
Jan 27, 2007 12:34:27 PM (9 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]