Changes between Initial Version and Version 1 of TypeFunctionsSynTC/Challenge


Ignore:
Timestamp:
Jan 27, 2007 12:33:40 PM (7 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC/Challenge

    v1 v1  
     1== The challenge == 
     2 
     3Consider the axioms 
     4 
     5{{{ 
     6forall a. S [a] = [S a]   (R1) 
     7T Int = Int               (R2) 
     8}}} 
     9S and T are type functions of kind *->* 
     10For convenience, I drop the `redundant' forall a. on R1's lhs. 
     11 
     12Suppose some type annotations/pattern matchings give rise 
     13to the local assumptions 
     14 
     15{{{ 
     16T [Int] = S [Int]        (R3) 
     17T Int = S Int            (R4) 
     18}}} 
     19and under these assumptions we need to verify 
     20 
     21{{{ 
     22T [Int] = [Int] 
     23}}} 
     24 
     25 
     26Logically, we can express the above as follows: 
     27 
     28{{{ 
     29(forall a. S [a] = [S a]) /\       -- axioms 
     30(T Int = Int) 
     31 
     32 |= 
     33 
     34 
     35 
     36(T [Int] = S [Int]) /\             -- local assumptions 
     37(T Int = S Int) 
     38 
     39 implies 
     40 
     41(T [Int] = [Int])                  -- (local) property 
     42}}} 
     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. 
     46 
     47NOTE: There are further axioms such as reflexitivity of = etc. 
     48We'll leave them our for simplicitiy. 
     49 
     50The all important question: 
     51How can we algorithmically check the above statement? 
     52Roughly, we perform the following two steps. 
     53 
     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. 
     56 
     57NOTE:  
     58 
     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. 
     60 
     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. 
     62 
     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). 
     72 
     73End of NOTE