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