Changes between Version 83 and Version 84 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 6, 2008 11:12:56 AM (7 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