Changes between Version 90 and Version 91 of TypeFunctionsSolving
 Timestamp:
 Sep 14, 2008 4:32:40 AM (8 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v90 v91 258 258 =(norm)=> 259 259 c :: a ~ [beta], id :: F b ~ beta  gamma :: alpha ~ a 260 with beta := F b 260 261 =(final)=> 261 262 alpha := a, gamma := id … … 274 275 with gamma' := sym gamma'' 275 276 =(final)=> 276 alpha := [ beta], gamma'' := id277 }}} 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).277 alpha := [F b], gamma'' := id 278 }}} 279 This result is fine, even when considering Andrew Kennedy's concerns, as we are necessarily in checking mode (following the `normalised_equation_algorithm` terminology). 279 280 280 281 Let's assume one toplevel equality `forall x. g x :: F x = ()`: … … 283 284 =(norm)=> 284 285 c :: a ~ [beta], id :: F b ~ beta  gamma :: a ~ alpha 286 with beta := F b 285 287 =(SubstVarVar)=> 286 288 c :: a ~ [beta], id :: F b ~ beta  gamma' :: [beta] ~ alpha … … 294 296 c :: a ~ [beta], g b :: beta ~ ()  gamma'' :: alpha ~ [beta] 295 297 =(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. 298 alpha := [()], 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. 301 301 302 302 