| 1 | == The challenge == |
| 2 | |
| 3 | Consider the axioms |
| 4 | |
| 5 | {{{ |
| 6 | forall a. S [a] = [S a] (R1) |
| 7 | T Int = Int (R2) |
| 8 | }}} |
| 9 | S and T are type functions of kind *->* |
| 10 | For convenience, I drop the `redundant' forall a. on R1's lhs. |
| 11 | |
| 12 | Suppose some type annotations/pattern matchings give rise |
| 13 | to the local assumptions |
| 14 | |
| 15 | {{{ |
| 16 | T [Int] = S [Int] (R3) |
| 17 | T Int = S Int (R4) |
| 18 | }}} |
| 19 | and under these assumptions we need to verify |
| 20 | |
| 21 | {{{ |
| 22 | T [Int] = [Int] |
| 23 | }}} |
| 24 | |
| 25 | |
| 26 | Logically, 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 | }}} |
| 43 | That is, any model (in the first-order sense) which is |
| 44 | a model of the axioms and local assumptions is also |
| 45 | a model of the property. |
| 46 | |
| 47 | NOTE: There are further axioms such as reflexitivity of = etc. |
| 48 | We'll leave them our for simplicitiy. |
| 49 | |
| 50 | The all important question: |
| 51 | How can we algorithmically check the above statement? |
| 52 | Roughly, 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 | |
| 57 | NOTE: |
| 58 | |
| 59 | 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. |
| 60 | |
| 61 | 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. |
| 62 | |
| 63 | We'll restrict ourselves to simple implication constraints of the form {{{ C implies t1=t2 }}} |
| 64 | In general, implication constraints may be nested, e.g |
| 65 | {{{ C1 implies (C2 implies C3) }}} and may contain conjunctions |
| 66 | of 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 ...) }}} |
| 68 | These universal quantifiers arise from universal type annotations, e.g. {{{ f :: S a = T a => ....}}}, and |
| 69 | pattern matchings over data types with abstract components, e.g. data Foo where |
| 70 | {{{ K :: S a = T a => a -> Foo}}} |
| 71 | We can operationally deal with universally quantified variables by skolemizing them (and we must ensure that skolemized/universal variables do not escape). |
| 72 | |
| 73 | End of NOTE |