Changes between Version 90 and Version 91 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 14, 2008 4:32:40 AM (7 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----