Changes between Version 90 and Version 91 of TypeFunctionsSolving

Timestamp:

09/13/08 21:32:40 (5 years ago)

Author:

chak

Comment:

--

TypeFunctionsSolving

@@ -258 +258 @@
 =(norm)=>
 c :: a ~ [beta], id :: F b ~ beta |- gamma :: alpha ~ a
+  with beta := F b
 =(final)=>
 alpha := a, gamma := id
@@ -274 +275 @@
   with gamma' := sym gamma''
 =(final)=>
-alpha := [beta], gamma'' := id
-}}}
-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).
+alpha := [F b], gamma'' := id
+}}}
+This result is fine, even when considering Andrew Kennedy's concerns, as we are necessarily in checking mode (following the `normalised_equation_algorithm` terminology).
 
 Let's assume one toplevel equality `forall x. g x :: F x = ()`:
@@ -283 +284 @@
 =(norm)=>
 c :: a ~ [beta], id :: F b ~ beta |- gamma :: a ~ alpha
+  with beta := F b
 =(SubstVarVar)=>
 c :: a ~ [beta], id :: F b ~ beta |- gamma' :: [beta] ~ alpha
@@ -294 +296 @@
 c :: a ~ [beta], g b :: beta ~ () |- gamma'' :: alpha ~ [beta]
 =(final)=>
-alpha := [beta], gamma'' := id
-}}}
-This is obviously bad, as we want to get `alpha := [()]` and not `alpha := [beta]` for a free `beta` out of finalisation.
-
-'''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.
+alpha := [()], gamma'' := id
+}}}
+'''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.
 
 ----