Changes between Initial Version and Version 1 of TypeFunctionsSynTC/Challenge

Jan 27, 2007 12:33:40 PM (11 years ago)



  • TypeFunctionsSynTC/Challenge

    v1 v1  
     1== The challenge ==
     3Consider the axioms
     6forall a. S [a] = [S a]   (R1)
     7T Int = Int               (R2)
     9S and T are type functions of kind *->*
     10For convenience, I drop the `redundant' forall a. on R1's lhs.
     12Suppose some type annotations/pattern matchings give rise
     13to the local assumptions
     16T [Int] = S [Int]        (R3)
     17T Int = S Int            (R4)
     19and under these assumptions we need to verify
     22T [Int] = [Int]
     26Logically, we can express the above as follows:
     29(forall a. S [a] = [S a]) /\       -- axioms
     30(T Int = Int)
     32 |=
     36(T [Int] = S [Int]) /\             -- local assumptions
     37(T Int = S Int)
     39 implies
     41(T [Int] = [Int])                  -- (local) property
     43That is, any model (in the first-order sense) which is
     44a model of the axioms and local assumptions is also
     45a model of the property.
     47NOTE: There are further axioms such as reflexitivity of = etc.
     48We'll leave them our for simplicitiy.
     50The all important question:
     51How can we algorithmically check the above statement?
     52Roughly, we perform the following two steps.
     54 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).
     55 2. Solve the implication constraint by applying axioms and local assumptions until the (local) property is verified. That's the hard part.
     59We 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.
     61In 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.
     63We'll restrict ourselves to simple implication constraints of the form {{{   C implies t1=t2 }}}
     64In general, implication constraints may be nested, e.g
     65{{{ C1 implies (C2 implies C3) }}} and may contain conjunctions
     66of implications, e.g. {{{C1 implies (F1 /\ F2)}}} where F1 and F2 are arbitrary implication constraints. Implication constraints may be universally quantified, e.g.
     67{{{ forall a (S a = T a implies ...) }}}
     68These universal quantifiers arise from universal type annotations, e.g.  {{{ f :: S a = T a => ....}}}, and
     69pattern matchings over data types with abstract components, e.g. data Foo where
     70{{{ K :: S a = T a => a -> Foo}}}
     71We can operationally deal with universally quantified variables by skolemizing them (and we must ensure that skolemized/universal variables do not escape).
     73End of NOTE