# Changes between Version 81 and Version 82 of TypeFunctionsSolving

Show
Ignore:
Timestamp:
09/05/08 22:51:31 (5 years ago)
Comment:

--

Unmodified
Removed
Modified
• ## TypeFunctionsSolving

v81 v82
253253
254254
255
256== Examples ==
257
258=== Unflattening locals and finalisation ===
259
260This seems ok:
261{{{
262c :: a ~ [F b] |- gamma :: alpha ~ a
263=(norm)=>
264c :: a ~ [beta], id :: F b ~ beta |- gamma :: alpha ~ a
265=(final)=>
266alpha := a, gamma := id
267}}}
268
269The problem becomes obvious when we orient the wanted equality the other way around:
270{{{
271c :: a ~ [F b] |- gamma :: a ~ alpha
272=(norm)=>
273c :: a ~ [beta], id :: F b ~ beta |- gamma :: a ~ alpha
274=(SubstVarVar)=>
275c :: a ~ [beta], id :: F b ~ beta |- gamma' :: [beta] ~ alpha
276  with gamma := c |> gamma'
277=(norm)=>
278c :: a ~ [beta], id :: F b ~ beta |- gamma'' :: alpha ~ [beta]
279  with gamma' := sym gamma''
280=(final)=>
281alpha := [beta], gamma'' := id
282}}}
283What 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).
284
285Let's assume one toplevel equality `forall x. g x :: F x = ()`:
286{{{
287c :: a ~ [F b] |- gamma :: a ~ alpha
288=(norm)=>
289c :: a ~ [beta], id :: F b ~ beta |- gamma :: a ~ alpha
290=(SubstVarVar)=>
291c :: a ~ [beta], id :: F b ~ beta |- gamma' :: [beta] ~ alpha
292  with gamma := c |> gamma'
293=(norm)=>
294c :: a ~ [beta], id :: F b ~ beta |- gamma'' :: alpha ~ [beta]
295  with gamma' := sym gamma''
296=(Top)=>
297c :: a ~ [beta], sym (g b) :: () ~ beta |- gamma'' :: alpha ~ [beta]
298=(norm)=>
299c :: a ~ [beta], g b :: beta ~ () |- gamma'' :: alpha ~ [beta]
300=(final)=>
301alpha := [beta], gamma'' := id
302}}}
303This is obviously bad, as we want to get `alpha := [()]` and not `alpha := [beta]` for a free `beta` out of finalisation.
304
255305----
256306
257 '''TODO:'''  Still need to adapt examples to new rule set!
258
259 == Examples ==
307'''TODO:'''  Still need to adapt the following examples to new rule set!
260308
261309=== Substituting wanted family equalities with !SubstFam is crucial if the right-hand side contains a flexible type variable ===