Changes between Version 81 and Version 82 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 6, 2008 5:51:31 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

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