Changes between Version 1 and Version 2 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 5, 2006 4:15:07 AM (9 years ago)
Author:
sulzmann
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC

    v1 v2  
    11= Type Checking with Indexed Type Synonyms =
     2
     3
     4== Outline ==
     5
     6 * Background
     7 * The challenge
     8 * A first (naive) attempt
     9 * A second attempt
     10    * type checking with type functions using local completion
     11    * method can be proven correct by establishing a connection
     12      between type function and CHR derivations
     13
     14== Background ==
     15
     16GHC has now FC as its typed intermediate language.
     17In a next step, we wish to add type functions to
     18GHC's source language.  Type functions in combination
     19with type annotations and GADTs allow us to type check
     20some interesting programs.
     21
     22{{{
     23data Zero
     24data Succ n
     25data List a n where
     26  Nil :: List a Zero
     27  Cons :: a -> List a m -> List a (Succ m)
     28
     29type add :: * -> * -> *
     30     add Zero x = x
     31     add (Succ x) y = Succ (add x y)
     32
     33append :: List a l -> List a m -> List a (add l m)
     34append Nil xs = xs
     35append (Cons x xs) ys = Cons x (append xs ys)
     36}}}
     37
     38However, type checking with type functions is challenging.
     39
     40== The challenge ==
     41
     42Consider the axioms
     43
     44{{{
     45forall a. S [a] = [S a]   (R1)
     46T Int = Int               (R2)
     47}}}
     48S and T are type functions of kind *->*
     49For convenience, I drop the `redundant' forall a. on R1's lhs.
     50
     51Suppose some type annotations/pattern matchings give rise
     52to the local assumptions
     53
     54{{{
     55T [Int] = S [Int]        (R3)
     56T Int = S Int            (R4)
     57}}}
     58and under these assumptions we need to verify
     59
     60{{{
     61T Int] = [Int]
     62}}}
     63
     64
     65Logically, we can express the above as follows:
     66
     67{{{
     68(forall a. S [a] = [S a]) /\       -- axioms
     69(T Int = Int)
     70
     71 |=
     72
     73(T [Int] = S [Int]) /\             -- local assumptions
     74(T Int = S Int)
     75
     76 implies
     77
     78(T [Int] = [Int])                  -- (local) property
     79}}}
     80That is, any model (in the first-order sense) which is
     81a model of the axioms and local assumptions is also
     82a model of the property.
     83
     84NOTE: There are further axioms such as reflexitivity of = etc.
     85We'll leave them our for simplicitiy.
     86
     87The all important question:
     88How can we algorithmically check the above statement?
     89Roughly, we perform the following two steps.
     90
     91
     921. Generate the appropriate implication constraint out of the program text.  That's easy cause GHC supports now implication constraints.
     93(there are some potential subtleties, see GENERATEIMP below).
     94
     952. Solve the implication constraint by applying axioms and local assumptions until the (local) property is verified. That's the hard part.
     96
     97NOTE:
     98
     99We 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.
     100
     101In 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.
     102
     103We'll restrict ourselves to simple implication constraints of the form {{{   C implies t1=t2 }}}
     104In general, implication constraints may be nested, e.g
     105{{{ C1 implies (C2 implies C3) }}} and may contain conjunctions
     106of implications, e.g. {{{C1 implies (F1 /\ F2)}}} where F1 and F2 are arbitrary implication constraints. Implication constraints may be universally quantified, e.g.
     107{{{ forall a (S a = T a implies ...) }}}
     108These universal quantifiers arise from universal type annotations, e.g.  {{{ f :: S a = T a => ....}}}, and
     109pattern matchings over data types with abstract components, e.g. data Foo where
     110{{{ K :: S a = T a => a -> Foo}}}
     111We can operationally deal with universally quantified variables by skolemizing them (and we must ensure that skolemized/universal variables do not escape).
     112
     113End of NOTE
     114
     115
     116== A first (naive) attempt ==
     117
     118
     119To solve  {{{(C implies t1=t2)}}} with respect to Ax
     120
     1211. We interpret Ax /\ C as a rewrite system (from left to right).
     122
     1232. We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent.
     124
     125
     126Immediately, we find a problem with this solving strategy.
     127Consider our running example.
     128
     129Rewrite rules
     130{{{
     131(forall a. S [a] = [S a]) /\      (R1) -- axioms
     132(T Int = Int)                     (R2)
     133
     134 /\
     135
     136(T [Int] = S [Int]) /\            (R3) -- local assumptions
     137(T Int = S Int)                   (R4)
     138 }}}
     139
     140applied to {{{(T [Int] = [Int])}}}
     141
     142yields
     143{{{
     144T [Int] -->* [S Int]       (R3,R1)
     145
     146[Int] -->* [Int]
     147}}}
     148
     149Hence, our (naive) solver fails, but
     150clearly the (local) property  (T [Int] = [Int])
     151holds.
     152
     153The trouble here is that
     154
     155* the axiom system Ax is confluent but if we included the local assumptions C
     156
     157* the combined system Ax /\ C is non-confluent (interpreted as a rewrite system)
     158
     159
     160Possible solutions:
     161
     162Enforce syntactic conditions such that Ax /\ C is confluent.
     163It's pretty straightforward to enforce that Ax and
     164constraints appearing in type annotations and data types
     165are confluent. The tricky point is that if we combine
     166these constraints they may become non-confluent.
     167For example, imagine
     168
     169{{{
     170Ax : T Int = Int
     171
     172   a= T Int      -- from f :: a=T Int => ...
     173
     174      implies
     175
     176        (a = S Int -- from a GADT pattern
     177
     178            implies ...)
     179}}}
     180
     181The point is that only during type checking we may
     182encounter that Ax /\ C is non-confluent!
     183So, we clearly need a better type checking method.
     184
     185
     186
     187== A second attempt ==
     188
     189To solve  {{{(C implies t1=t2)}}} with respect to Ax
     190
     1911. a. We interpret Ax /\ C as a rewrite system (from left to right)       and
     192
     193   b. perform completion until the rewrite system is confluent.
     194
     1952. We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent.
     196
     197
     198Step 1b) is new and crucial. For confluent rewrite systems the
     199checking step 2) will work fine (we also need termination of course).
     200But how do we now that completion will succeed?
     201The important condition is to guarantee that Ax is confluent (and
     202terminating) then completion will be successful (i.e. terminated
     203and produce a confluent rewrite system).
     204
     205Let's take a look at our running example.
     206{{{
     207(forall a. S [a] = [S a]) /\      (R1) -- axioms
     208(T Int = Int)                     (R2)
     209
     210 /\
     211
     212(T [Int] = S [Int]) /\            (R3) -- local assumptions
     213(T Int = S Int)                   (R4)
     214}}}
     215The axioms are clearly confluent
     216but there's a critical pair between (R2,R4).
     217
     218Completion yields
     219
     220{{{
     221(S Int = Int)                     (R5)
     222}}}
     223Now, we can verify that (T [Int] = [Int])
     224
     225by executing
     226
     227{{{
     228T [Int] -->* [Int]       (R3,R1,R5)
     229
     230[Int] -->* [Int]
     231}}}
     232
     233The completion method in more detail.
     234
     235=== There are two kinds of critical pairs ===
     236
     237* Axiom vs local assumption, see (R2,R4) above
     238* Local assumption vs local assumption. For example,
     239{{{
     240  T Int = S Int  /\
     241  T Int = R Int
     242}}}
     243  Completion yields
     244{{{
     245  S Int = R Int
     246  R Int = S Int
     247}}}
     248
     249NOTE: Axiom vs axiom impossible cause axiom set is confluent
     250
     251
     252Towards establishing a connection between completion and CHR derivation steps
     253
     254
     255NOTE:
     256
     257There's a straightforward translation from type functions to constraints. For each n-ary function symbol T, we introduce a n+1-ary constraint symbol T. Thus, we can represent
     258{{{T Int = Int}}}  as
     259{{{ T Int a /\ a=Int}}}
     260For example, {{{T Int = S Int}}} is represented by
     261{{{T Int a /\ S Int b /\ a=b}}}
     262
     263
     264We can verify that the completion method success by showing that each critical pair arises in the `corresponding' CHR derivation (this derivation terminates if the axiom system is confluent and terminating, hence, we'll only encounter a finite number of critical pairs, hence, completion terminates).
     265
     266Recall the critical pair (axioms vs local assumption) from above
     267{{{
     268T Int = Int     -- axiom
     269T Int = S Int  -- local assumption
     270}}}
     271In the CHR world, we'll represent both as
     272{{{
     273T Int a <==> a=Int         -- axiom turned into CHR
     274
     275T Int b /\ S Int c /\ b=c  -- local assumption turned into CHR
     276                           -- constraints
     277}}}
     278In the CHR world, we find that
     279{{{
     280    T Int b /\ S Int c /\ b=c
     281--> b=Int /\ S Int c /\ b=c      -- apply CHR
     282<--> b=Int /\ c=Int /\ S Int Int -- equivalence transformation
     283                                 -- apply mgu
     284}}}
     285directly corresponds to
     286{{{
     287S Int = Int
     288}}}
     289generated by our completion method
     290
     291Recall the critical pair (local assumption vs local assumption)
     292{{{
     293  T Int = S Int  /\
     294  T Int = R Int
     295}}}
     296represented in the CHR world as
     297{{{
     298 T Int a /\ S Int b /\ a=b /\
     299 T Int c /\ R Int d /\ c=d
     300}}}
     301In the CHR world, we find that
     302{{{
     303    T Int a /\ S Int b /\ a=b /\
     304    T Int c /\ R Int d /\ c=d
     305-->T Int a /\ S Int b /\ a=b /\ 
     306   c=a /\ R Int d /\ c=d
     307
     308      -- apply FD rule
     309      -- T a b /\ T a c ==> b=c
     310
     311<--> T Int a /\ S Int a /\ R Int a /\
     312     a=b, c=a, d=a
     313}}}
     314  directly corresponds to
     315{{{
     316    S Int = R Int
     317    R Int = S Int
     318}}}
     319
     320The general cases are as follows.
     321
     322==== axiom vs local assumption case ====
     323
     324{{{
     325forall as. (T t1 ... tn = s)  -- axiom
     326
     327T t1' ... tn' = s'            -- local assumption
     328}}}
     329where exist phi, dom(phi)=as such that phi(ti) = ti' for i=1,...,n
     330
     331
     332completion yields
     333{{{
     334    s' = phi(s)
     335    phi(s) = s'       
     336}}}
     337
     338NOTE: We may need both orientation see above example.
     339We assume that symbol t refers to types NOT containing type functions and s refers to types which may contain type functions (can be lifted, more below)
     340
     341
     342Explaining completion in terms of CHRs.
     343Above translates to
     344{{{
     345T t1 ... tn b <==> C
     346
     347T t1' ... tn' b' /\ C'
     348}}}
     349where  s is translated to (C | b) and s' is translated to (C | b')
     350
     351(see above where each type function type is represented by
     352a variable under some CHR constraints)
     353
     354The type functions
     355{{{
     356    s' = phi(s)
     357    phi(s) = s'       
     358}}}
     359resulting from completion 'appear' in the CHR derivation
     360(i.e. the operational effect is the same)
     361{{{
     362     T t1' ... tn' b' /\ C'    -- apply CHR
     363--> b=b', phi(C) /\ C'
     364}}}
     365
     366==== local assumption vs local assumption ====
     367
     368{{{
     369T t1 ... tn = s1
     370T t1 ....tn = sn
     371}}}
     372
     373completion yields
     374{{{
     375  s1 = s2
     376  s2 = s1
     377}}}
     378In the CHR world, above represented by
     379
     380{{{
     381T t1 ... tn a /\ C1
     382T t1 ....tn b /\ C2
     383}}}
     384where s1 translated to (C1 | a)
     385      s2 translated to (C1 | n)
     386
     387Then,
     388{{{
     389    T t1 ... tn a /\ C1 /\
     390    T t1 ....tn b /\ C2
     391
     392--> FD rule step
     393
     394    T t1 ... tn a /\ C1 /\
     395    a=b /\ [a/b] C2
     396}}}
     397
     398Again, the operational effect of the type function generated
     399is also present in the CHR derivation
     400
     401
     402Lifting the restriction that t refers to types NOT containing
     403type functions (we only lift this restriction for
     404local assumptions).
     405
     406Consider
     407{{{
     408forall a. T [a] = [T a]      -- axiom
     409
     410T [S Int] = s                -- local assumption
     411}}}
     412
     413We can normalize
     414{{{
     415T [S Int] = s
     416}}}
     417to
     418{{{
     419T [b] = s
     420S Int = b
     421}}}
     422Method from above applies then.
     423
     424NOTE: Regarding generation of implication constraints.
     425GENERATEIMP
     426
     427The literate implication constraints generated out of the
     428program text may look as follows
     429{{{ a=T Int implies ( a= S Int implies ...)
     430}}}
     431
     432The above can be simplified to
     433{{{ (a=T Int /\ a = S Int) implies ...}}}
     434Before we proceed with the completion method, we first
     435need to apply some closure rules (eg. transitivity, left, right etc)
     436Hence, from the above we generatet
     437{{{a=T Int /\ a = S Int /\
     438   T Int = a /\ S Int = a /\       -- symmetry
     439   T Int = S Int /\ S Int = T Int  -- transitivity
     440}}}
     441We omit the trival (reflexive) equations
     442{{{ T Int = T Int /\ S Int = S Int }}}