Changes between Version 5 and Version 6 of TypeFunctions/TotalFamilies


Ignore:
Timestamp:
Apr 6, 2008 11:01:59 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctions/TotalFamilies

    v5 v6  
    8181 * `TypeEq a b` where `a` and `b` are two rigid type variables, can't be rewritten without further information about `a` and `b`. 
    8282 
    83 === Critical examples from the paper === 
     83=== Critical examples concerning termination === 
    8484 
     85Example 1 of the paper: 
     86{{{ 
     87Et: {F Bool ~ F (G Int); F _ ~ VOID} 
     88    {G _ ~ VOID} 
    8589 
     90Eg: G Int ~ Bool 
     91}}} 
     92Completion gives: 
     93{{{ 
     94  Eg 
     95=> (TOP) 
     96  VOID ~ Bool 
     97=> FAIL 
     98}}} 
     99 
     100We can be a bit more tricky and use 
     101{{{ 
     102Et: {F [a] ~ F (G a); F _ ~ VOID} 
     103    {G _ ~ VOID} 
     104 
     105Eg: G x ~ [x] 
     106}}} 
     107Here the idea is to use a new symbol in the local given, namely a rigid type variable.  Nevertheless, the only equality of `G` matches `G x` and completion of `Eg` leads to an inconsistency. 
     108 
     109However, if we add another equality to `G`, the situation changes: 
     110{{{ 
     111Et: {F [a] ~ F (G a); F _ ~ VOID} 
     112    {G Int ~ Bool; G _ ~ VOID} 
     113 
     114Eg: G x ~ [x] 
     115}}} 
     116Here completion can't rewrite `G x`, as the outcome depends on getting more information about `x`.  However, we have the following infinite derivation: 
     117{{{ 
     118F [x]  -->  F (G x)  -->  F [x]  -->  ... 
     119}}} 
     120This is although `Eg` is inconsistent (and hence shouldn't be used for rewriting at all). 
     121 
     122Can we fix this???