| 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] |
