Changes between Version 90 and Version 91 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 14, 2008 4:32:40 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v90 v91  
    258258=(norm)=> 
    259259c :: a ~ [beta], id :: F b ~ beta |- gamma :: alpha ~ a 
     260  with beta := F b 
    260261=(final)=> 
    261262alpha := a, gamma := id 
     
    274275  with gamma' := sym gamma'' 
    275276=(final)=> 
    276 alpha := [beta], gamma'' := id 
    277 }}} 
    278 What about `F b ~ beta`?  If we just throw that away, we have an unconstrained `beta` in the environment.  However, instantiating `beta` with `F b` doesn't seem to be right, too (considering Andrew Kennedy). 
     277alpha := [F b], gamma'' := id 
     278}}} 
     279This result is fine, even when considering Andrew Kennedy's concerns, as we are necessarily in checking mode (following the `normalised_equation_algorithm` terminology). 
    279280 
    280281Let's assume one toplevel equality `forall x. g x :: F x = ()`: 
     
    283284=(norm)=> 
    284285c :: a ~ [beta], id :: F b ~ beta |- gamma :: a ~ alpha 
     286  with beta := F b 
    285287=(SubstVarVar)=> 
    286288c :: a ~ [beta], id :: F b ~ beta |- gamma' :: [beta] ~ alpha 
     
    294296c :: a ~ [beta], g b :: beta ~ () |- gamma'' :: alpha ~ [beta] 
    295297=(final)=> 
    296 alpha := [beta], gamma'' := id 
    297 }}} 
    298 This is obviously bad, as we want to get `alpha := [()]` and not `alpha := [beta]` for a free `beta` out of finalisation. 
    299  
    300 '''NB:''' The problem in the last example arises when we finalise as described in the `normalisied_equalities_algorithm` paper.  It is not a problem when using the strategy outlined on this wiki page. 
     298alpha := [()], gamma'' := id 
     299}}} 
     300'''NB:''' The algorithm in the `normalisied_equalities_algorithm` paper (as opposed to the on this wiki page) will compute `alpha := [F b]`, which is equivalent, but less normalised. 
    301301 
    302302----