Changes between Version 16 and Version 17 of TypeFunctionsSynTC
 Timestamp:
 Dec 12, 2006 9:15:50 PM (10 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSynTC
v16 v17 434 434  435 435 436 == Restrictions ontype equations ==437 438 We impose some syntactic restrictions on programsto ensure that type checking remains (a) deterministic, (b) a simple rewrite model is sufficient to reduce type function applications, and (c) it hopefully remains decidable.436 == Special forms of type equations == 437 438 We impose some syntactic restrictions on type instances and normalise equations arising during type checking to ensure that type checking remains (a) deterministic, (b) a simple rewrite model is sufficient to reduce type function applications, and (c) it hopefully remains decidable. 439 439 440 440 === Type variables === … … 477 477 We require that all type family instances are normal. Moreover, all equalities arising as local assumptions need to be such that they can be normalised (see below). NB: With `fundecidableindexedtypes`, we can drop left linearity and decreasingness. 478 478 479 === Seminormal type equations === 480 481 If an equation `s = t` does not contain any schema variables and is normal, except that it's lefthand side `F s1 .. sn` contains one or more type family constructors in the `si`, we call it ''seminormal''. 482 479 483 === Normalisation of equalities === 480 484 … … 482 486 483 487 1. Reduce `s` and `t` to NF, giving us `s'` and `t'`. 484 2. If `s'` and `t'` are the same variable, we succeed (with no new rule).488 2. If `s'` and `t'` are identical, we succeed (with no new rule). 485 489 3. If `s'` or `t'` is a rigid variable, we fail. (Reason: cannot instantiate rigid variables.) 486 490 4. If `s'` or `t'` is a wobbly type variables, instantiate it with the other type (after occurs check). … … 488 492 6. If `s'` = `C1 ...` and `t' = C2 ...`, where `C1` and `C2` are different data type constructors, we fail. (Reason: unfication failure.) 489 493 7. Now, at least one of `s'` and `t'` has the form `F r1 .. rn`, where F is a type family: 490 * If `s' ` = `F s1 .. sn` and is constructorbased and leftlinear, and if `s' = t'` is decreasing, yield `s' = t'`.491 * If `t' ` = `F t1 .. tn` and is constructorbased and leftlinear, and if `t' = s'` is decreasing, yield `t' = s'`.492 * If `s' ` = `F s1 .. sn` and some `si` contains a type family application of the form `G r1 .. rn`, yield the union of the equations obtained by normalising both `G r1 .. rn = a` and `F s1 .. sn = t'` with `G r1 .. rn` replaced by `a`, which is a new rigid type variable.493 * If `t' ` = `F t1 .. tn` and some `ti` contains a type family application of the form `G r1 .. rn`, yield the union of the equations obtained by normalising both `G r1 .. rn = a` and `F t1 .. tn = s'` with `G r1 .. rn` replaced by `a`, which is a new rigid type variable.494 * If `s' = t'` is normal, yield it. 495 * If `t' = s'` is normal, yield it. 496 * If `s' = t'` is seminormal, yield it. 497 * If `t' = s'` is seminormal, yield it. 494 498 * Otherwise, fail. (Reason: a wobbly type variable, lack of left linearity, or nondecreasingness prevents us from obtaining a normal equation. If it is a wobbly type variable, the user can help by adding a type annotation; otherwise, we cannot handle the program without (maybe) losing decidability.) 495 499 496 500 Rejection of local assumptions that after normalisation are either not left linear or not decreasing may lead to incompleteness. However, this should only happen for programs that are invalid or combine GADTs and type functions in ellaborate ways. 497 498 '''TODO:''' I am wondering whether we can do that pulling out type family applications from lefthand sides and turning them into extra type equations lazily.