template.md

INV

INV (for invariant) is essentially marker for typechecking [1]. For instance, say you have a function foo declared as follows:

fun{a:t@ype} foo (xs: list0 (a)): void

Assume that mylst is of the type list0 (T) for some T. When typechecking foo(mylst), the typechecker will expand the expression as follows by picking a placeholder T1:

foo<T1>(mylst)

where T <= T1 is assumed, so that mylst can contain any subtype--in the covariant sense--of T1 [2]. Say that foo2 is declared as follows:

fun{a:t@ype} foo2 (xs: list0 (INV(a))): void

When foo2(mylst) is typechecked, the typechecker simply expands the expression to the following one:

foo2<T>(mylst)

preventing types other than precisely T to be a part of mylst.