Changes between Version 90 and Version 91 of TypeFunctionsSolving

Show
Ignore:
Timestamp:
09/13/08 21:32:40 (5 years ago)
Comment:

--

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