Changes between Version 81 and Version 82 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 6, 2008 5:51:31 AM (6 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 ===