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