Changes between Version 83 and Version 84 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 6, 2008 11:12:56 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v83 v84  
    239239== Finalisation == 
    240240 
    241 '''!!!TODO:''' complete the following. 
    242  
    243 The finalisation step instantiates as many flexible type variables as possible, but it takes care to not to affect variables occurring in the global environment.  The latter is important to obtain principle types (c.f., Andrew Kennedy's thesis).  Hence, we perform finalisation in two phases: 
    244  1. '''Instantiation:''' For any variable equality of the form `co :: alpha ~ t` or `co :: a ~ alpha`, where `co` is wanted or `alpha` is a variable introduced by flattening, we instantiate `alpha` with `t` or `a`, respectively, and set `co := id`. 
    245  2. '''Substitution:''' For any family equality... 
    246  
    247 '''!!!TODO:''' What about unflattening the locals? 
    248  
    249 {{{ 
    250 alpha in environ, beta in skolems: 
    251   gamma1 :: alpha ~ [beta], id :: G a ~ beta   -- , gamma2 :: F a ~ beta 
    252 }}} 
    253  
     241The finalisation step instantiates as many flexible type variables as possible, but it takes care not to instantiate variables occurring in the global environment with types containing synonym family applications.  This is important to obtain principle types (c.f., Andrew Kennedy's thesis).  Hence, we perform finalisation in two phases: 
     242 1.  '''Substitution:''' For any variable equality of the form `co :: x ~ t` (both local and wanted), we apply the substitution `[t/x]` to all equalities. 
     243 2. '''Instantiation:''' For any variable equality of the form `co :: alpha ~ t` or `co :: a ~ alpha`, where `co` is wanted, we instantiate `alpha` with `t` or `a`, respectively, and set `co := id`. 
    254244 
    255245